\documentclass[japanese]{jnlp_3.6}
\usepackage{jnlpbbl_2.2}
\usepackage[dvipdfmx]{graphicx}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{url}
\usepackage{hangcaption_jnlp}
\usepackage{array}
%%%%\usepackage{udline}
%%%%\setulminsep{1.2ex}{0.2ex}
%%%%\let\underline=\ul
\allowdisplaybreaks


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% author's definition
\usepackage{amsthm}
\usepackage{latexsym}
\theoremstyle{definition}
\newtheorem{thm}{\emph{定理}}
\newtheorem{lem}[thm]{\emph{補助定理}}
\theoremstyle{definition}
\newtheorem{dfn}{\emph{定義}}
\renewcommand{\proofname}{\textbf{証明}}
%%%%\usepackage{here}
%%%%\newcommand\blfootnote[1]{%
%%%%  \begingroup
%%%%  \renewcommand\thefootnote{}\footnote{#1}%
%%%%  \addtocounter{footnote}{-1}%
%%%%  \endgroup
%%%%}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\Volume{30}
\Number{2}
\Month{June}
\Year{2023}
%%%%\Issuetitle{「　　　　」特集号}

\received{2022}{9}{1}
\revised{2023}{1}{26}
\accepted{2023}{3}{3}

\setcounter{page}{632}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\jsubject{一般論文}
\jtitle{ニューラルモデルとタブロー法を用いた自然言語推論}
\jauthor{佐治　礼仁\affiref{Author_1}\affiref{Author_2} \and 高尾　大樹\affiref{Author_1} \and 加藤　芳秀\affiref{Author_3} \and 松原　茂樹\affiref{Author_1}\affiref{Author_3}}
\jabstract{%
自然言語推論 (NLI) は，2 つのテキストの間に成り立つ推論的関係を同定するタスクである．近年，ニューラルモデルに基づくアプローチが高い正答率を達成している．しかし，このアプローチに基づくNLIは，判定結果に至る過程や理由を説明する能力を有していないという問題がある．一方，NLI では以前より，記号操作に基づくアプローチが提案されてきた．このアプローチは，推論の論理的な過程を明示でき，推論の根拠を示すことができるものの，語の意味的知識や常識的な知識を十分に備えることは容易でなく，高い推論性能の達成は難しいという問題がある．そこで本論文では，タブロー法とニューラルモデルを組み合わせた手法を提案する．タブロー法は，推論規則の適用に基づく論理式の分解，及び，論理式への真偽値割り当てが存在するか否かの検査から構成される．本手法ではこのうち，真偽値割り当ての検査にニューラルモデルを用いる．なお，タブロー法では通常，論理式を操作対象とするのに対し，本手法では依存構造を対象とする．依存構造を用いることにより，ニューラル NLI モデルをタブロー法アルゴリズムに組み込むことが可能となる．提案手法の論理的整合性を検証するために，手法をモデル理論的に定式化し，その理論的性質を明らかにした．また，SNLI コーパスを用いて推論実験を行い，本手法による推論過程の明示可能性を検証した．
\renewcommand{\thefootnote}{}
\protect\footnote[0]{本論文の内容の一部は，The 35th Pacific Asia Conference on Language, Information and Computation \cite{saji-etal-2021-natural}，および，The 36th Pacific Asia Conference on Language, Information and Computationで報告したものである．}
\renewcommand{\thefootnote}{\arabic{footnote}}
}
\jkeywords{自然言語推論，含意関係認識，依存構造，形式論理，タブロー法，ニューラルネットワーク，SNLI コーパス}


\etitle{Natural Language Inference Using Neural Network and Tableau Method}
\eauthor{Ayahito Saji\affiref{Author_1}\affiref{Author_2} \and Daiki Takao\affiref{Author_1} \and Yoshihide Kato\affiref{Author_3} \and Shigeki Matsubara\affiref{Author_1}\affiref{Author_3}}
\eabstract{%
Natural language inference (NLI) is the task of identifying the inferential relation between a text pair. In recent times, neural-based approaches have achieved high performance in NLI. However, they are unable to explain their reasoning processes. On the other hand, symbolic approaches have the advantage that their reasoning process is understandable to humans. This paper proposes a method for integrating a neural NLI model and the tableau proof system, with the latter explaining the reasoning processes. The standard tableau method decomposes logical formulas by applying inferential rules and checks for a valuation that satisfies the given constraints. Unlike the standard tableau method, the proposed method uses dependency structures as its components rather than logical formulas and employs a neural NLI model for the latter process. To analyze the behavior of our method, we conducted an experiment on the neural NLI model and the proposed method using SNLI corpus. In addition, we formalize our method model-theoretically and clarify the theoretical limitations of this method based on the formalization.
}
\ekeywords{Natural Language Inference, Recognizing Textual Entailment, Dependency Structure, Formal Logic, Tableau Method, Neural Network, SNLI corpus}

\headauthor{佐治，高尾，加藤，松原}
\headtitle{ニューラルモデルとタブロー法を用いた自然言語推論}

\affilabel{Author_1}{名古屋大学大学院情報学研究科}{Graduate School of Informatics, Nagoya University}
\affilabel{Author_2}{現所属：ヤフー株式会社}{Currently: Yahoo Japan Corporation}
\affilabel{Author_3}{名古屋大学情報連携推進本部}{Information and Communications, Nagoya University}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\maketitle


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{はじめに}

自然言語推論(NLI) \cite{series/synthesis/2013Dagan}とは，2つのテキスト（一方を\emph{前提}，他方を\emph{仮説}と呼ぶ）の間に成り立つ推論的関係を同定するタスクである．
前提から仮説が，論理的知識や常識的知識を用いて導出可能である場合は\emph{含意}，前提と仮説が両立しえない場合は\emph{矛盾}，そのいずれでもない場合は\emph{中立}と判定する．
質問応答，情報検索，テキスト要約などの幅広い分野での応用が期待されている．

近年，ニューラルモデルに基づくアプローチ\cite{parikh-etal-2016-decomposable,chen-etal-2017-enhanced,devlin-etal-2019-bert,DBLP:journals/corr/abs-1909-11942,tai-etal-2020-exbert,Wang2021EntailmentAF}が提案され，SNLI コーパス\cite{bowman-etal-2015-large}，MultiNLI (MNLI) コーパス\cite{williams-etal-2018-broad}，Adversarial NLI (ANLI) データセット\cite{nie-etal-2020-adversarial}，QNLI データセット\cite{wang-etal-2018-glue}などのNLIデータセットを用いた実験で高い正答率を達成している．
しかし，このアプローチに基づくNLIは，判定結果に至る過程や理由を説明する能力を有していないという問題がある．
ニューラルモデルの内部はブラックボックスであり，どのような推論を経て判定に至ったのかを人間が推察することは容易ではない\footnote{Kumarら\cite{kumar-talukdar-2020-nile}は説明文を生成するNLIシステムを提案している．しかし，説明文はニューラルモデルにより生成されるため，説明文の生成過程はブラックボックス化しており，内部の処理を知ることは困難であるといえる．}．
このような問題に対して，近年，機械学習モデルの判定の過程を明らかにするための技術，いわゆる説明可能なAI (XAI) \cite{BARREDOARRIETA202082}の研究が進められており，自然言語処理の分野においても同様の問題意識を共有している\cite{danilevsky-etal-2020-survey}．
また，ニューラルモデルによる推論の正当性についても問題が指摘されている．例えば，Yanakaら\shortcite{yanaka-etal-2020-neural}は，ニューラルモデルが自然言語における推論の体系性を学習するかについてmonotonicityの観点から評価する手法を提案し，現状のニューラルモデルの汎化性能には限界があることを示している．
\pagebreak
また，Gururanganら\shortcite{gururangan-etal-2018-annotation}やTsuchiya \shortcite{tsuchiya-2018-performance}は，SNLIコーパスやMNLIコーパスなどのNLIデータセットには，本来2つのテキストに対して定まるはずの推論的関係が，一方のテキストのみから推測できてしまうバイアスがあることを示し，ニューラルモデルが単にバイアスに基づいて推論的関係を同定しているという危険性を指摘している．

一方，NLIでは従来より，記号操作に基づくアプローチが提案されてきた \cite{bar2007semantic,maccartney-manning-2007-natural,maccartney-manning-2008-modeling,maccartney-manning-2009-extended,mineshima-etal-2015-higher,abzianidze-2015-tableau,abzianidze-2017-langpro,hu-etal-2020-monalog}．
このアプローチには，ニューラルモデルによるものと異なり，推論の論理的な過程を明示できるという利点がある．
また，推論における記号操作は，論理学や言語学による裏付けが与えられているため，推論の根拠を示すことができる．
しかし，このアプローチでは，推論規則を人手で作成する必要があり，語の同義・対義関係や上位・下位関係を網羅的に扱うことが難しいという問題がある．
加えて，「雨が降ると地面が濡れる」といった常識的知識を推論規則として表現しなければならず，それを人手で網羅することは困難である．
実際，記号操作に基づくアプローチは，FraCaS test suite \cite{Consortium96usingthe}やSICKデータセット\cite{marelli-etal-2014-sick}など，論理的知識に基づき推論的関係が導出できるように統制をかけて作成されたNLIデータセット（以下，統制NLIデータと呼ぶ）に対して優位性が示されている．
一方，上述したSNLIコーパスやMNLIコーパスなどは，統制NLIデータで課されたような統制をかけず比較的自由に作成されている（以下，非統制NLIデータと呼ぶ）．
語の意味的知識や常識的な知識を十分に備えていない記号操作に基づくアプローチでは，非統制NLIデータに対して高い正答率を達成することは難しい．

そこで本論文では，ニューラルモデルに基づくアプローチが備える，非統制NLIデータへの適用可能性を維持しつつ，論理的な推論過程を明示可能な自然言語推論システムを実現するための一手法を提案する．
本手法では，形式論理の証明手法の一つであるタブロー法のアルゴリズムとニューラルNLIモデルを組み合わせる．
タブロー法は，推論規則の適用に基づく論理式の分解，並びに論理式への真偽値割り当てが存在するか否かの検査から構成される．
提案手法ではこのうち，真偽値割り当ての検査にニューラルNLIモデルを用いる．
タブロー法は通常，論理式を操作対象とするのに対し，本手法では，依存構造を操作対象とする．
依存構造を用いることにより，ニューラルNLIモデルをタブロー法アルゴリズムに組み込むことが可能となる．
本手法で導入するニューラルNLIモデルには，入力として前提文と仮説文を受け取ること，及び，それらの推論的関係を出力することのみを課し，その内部処理に関する制約はない\footnote{すなわち，本手法は任意のニューラルNLIモデルに適用可能である．}．

本論文の構成は以下の通りである．
まず2章で，提案手法のベースとなるタブロー法について概説する．
3章では，タブロー法とニューラルNLIモデルを組み合わせた推論手法を提案する．
続く4章では，提案手法の意味論をモデル理論的に定式化し，手法の理論的性質を明らかにする．
5章では，SLNIコーパスを用いて，提案手法の推論能力を定量的及び定性的に評価する．
6章では，関連研究を整理し，提案手法との違いを示す．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{タブロー法}

本章では，提案手法のベースとなるタブロー法について説明する．
タブロー法は，論理式と真偽値の対の集合が与えられたとき，集合中のすべての論理式にその対となる真偽値を割り当てることが可能か否かを証明する手続きである．
タブロー法では，与えられた集合をもとに，タブローと呼ばれる木構造を構成する．
タブローのノードのラベルは，3つ組$(f, v, a)$であり，\emph{エントリ}と呼ばれる．
これは，論理式$f$が真偽値として$v$を取らなければならないという制約を表しており，$a$はこのエントリに対して後述するタブロー規則が適用されたか否かを表すフラグである．
真偽値は，\texttt{T}か\texttt{F}のいずれかであり，それぞれ真と偽を表す．
フラグは，0か1のいずれかであり，0はタブロー規則が未適用，1は適用済みであることを表す．
\emph{初期タブロー}は，与えられた集合の要素である論理式と真偽値の対に対して，フラグとして値0を付加したエントリから構成される．
タブローのエントリに\emph{タブロー規則}と呼ばれる推論規則を適用することにより新たなタブローが導出される．
タブロー規則の適用により，エントリが表現する制約，すなわち，論理式が与えられた真偽値を取らなければならないという制約は，部分論理式に関する制約に分解され，新たなエントリとしてタブローに付け加えられる．
この分解により，推論の過程が明示化される．
以下では，タブロー$t$に対して，タブロー規則集合$R$中のタブロー規則を適用して，タブロー$t'$が導出されるとき，$t \stackrel{R}{\rhd} t'$と表記する．
また，$\stackrel{R}{\rhd}$の反射推移閉包を$\stackrel{R}{\rhd^{*}}$と表記し，$t \stackrel{R}{\rhd} t'$であるような$t'$が存在しないタブロー$t$を\emph{完成したタブロー}と呼ぶことにする．

タブロー規則の適用は，適用元のエントリが表現する制約を，それと等価な制約へと変換する操作と位置づけられる\footnote{弱い制約を導出するタブロー規則も考えられるが，本論文ではそのような規則は対象としない．}．
したがって，タブロー規則が適用されたエントリの制約は，新たに導出されたエントリにより表現されているため，それ以上規則の適用，および後述する閉鎖性判定の対象にする必要はない．
エントリ$(f,v,a)$の$a$はこれらの操作の適用の制御に利用でき，タブロー規則が適用されたときにこれを1に変更する．
フラグが1のエントリは以後，規則の適用，および閉鎖性判定の対象とはしない．

タブローは木構造であり分岐する．分岐は場合分けに相当する．
タブローの根から葉への経路を\emph{枝}と呼び，ある枝の上に$(f, \texttt{T}, 0)$，および$(f, \texttt{F}, 0)$ （$f$は論理式）というエントリが存在するとき，その枝は\emph{閉じている}という．
タブローのすべての枝が閉じているとき，そのタブローは\emph{閉じている}という．
閉じているタブローを\emph{閉鎖タブロー}と呼ぶ．
タブローが閉じていることによって，最初に与えられた論理式と真偽値の対の集合のような真偽値割り当てが存在しないことが証明される．

例として，命題記号$\texttt{p}, \texttt{q}, \texttt{r}$について，$\texttt{p} \land \texttt{q} \rightarrow \texttt{r}$，$\texttt{p}$，$\texttt{q}$が真であるとき，$\texttt{r}$も真であることを命題論理におけるタブロー法を用いて証明する．
この証明には，$\{ (\texttt{p} \land \texttt{q} \rightarrow \texttt{r}, \texttt{T}), (\texttt{p}, \texttt{T}), (\texttt{q}, \texttt{T}), (\texttt{r}, \texttt{F}) \}$に対する完成したタブローが閉じていることを示せば十分である．
完成したタブローを図\ref{fig:meidai-tableau-example}(a)に示す．
初期タブローは，図中のエントリ$e_1$～$e_4$からなるタブローである．
この初期タブローに対して，図\ref{fig:meidai-tableau-example}(b)にその一部を記した命題論理におけるタブロー規則の適用を繰り返すと，図\ref{fig:meidai-tableau-example}(a)が得られる．
その後，各枝において，それが閉じているかどうかを判定する．
この例では，全ての枝が閉じている（図では，×により閉じていることを示す），すなわちこのタブローは閉じている．
これは，$\texttt{p} \land \texttt{q} \rightarrow \texttt{r}$，$\texttt{p}$，$\texttt{q}$に真，$\texttt{r}$に偽を割り当てることができないことを意味しており，$\texttt{p} \land \texttt{q} \rightarrow \texttt{r}$，$\texttt{p}$，$\texttt{q}$が真であるならば，$\texttt{r}$も真であることが証明される．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 1
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f1.pdf}
\end{center}
\caption{命題論理に対するタブロー推論の例}
\label{fig:meidai-tableau-example}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{提案手法}

本章では，タブロー法とニューラルNLIモデルを組み合わせた自然言語推論の手法を提案する．
この手法は以下の処理を順に実行する．

\begin{description}
  \item[依存構造解析]
  前提文$p$と仮説文$h$に依存構造を付与する．
  依存構造が付与された文をそれぞれ$D_p$，$D_h$とする．
  \item[タブローの構成]
  前提$D_p$と仮説$D_h$をもとに，含意関係を証明するタブロー（集合$\{(D_p, \texttt{T}), $\linebreak$(D_h, \texttt{F})\}$から導出される完成したタブロー）と矛盾関係を証明するタブロー（集合$\{(D_p, \texttt{T}), $\linebreak$(D_h, \texttt{T})\}$から導出される完成したタブロー）を構築する．
  以下では，これらのタブローをそれぞれ\textbf{含意タブロー}，\textbf{矛盾タブロー}と呼ぶ．
  \item[タブローの閉鎖性判定]
  含意タブロー，および矛盾タブローが閉じているか否かをニューラルNLIモデルを用いて判定する．
  \item[推論的関係の同定]
  含意タブローと矛盾タブローの閉鎖性の判定から，推論的関係を同定する．
\end{description}

以下では，各処理について，その背景となる考え方と合わせて説明する．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 2
\begin{figure}[b]
\begin{center}
\includegraphics{30-2ia13f2.pdf}
\end{center}
\caption{``Either Smith or Anderson signed the contract.''の依存構造解析結果}
\label{fig:udconvert}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{依存構造解析}

提案手法ではタブローが閉じているか否かの判定にニューラルNLIモデルを利用する．これにはニューラルNLIモデルへの入力は論理式ではなく自然言語文2文であることが課題となる．
この課題を解決する，すなわち，自然言語文をモデルに入力するためのアプローチの一つとして，タブローのエントリは論理式とし，前提文と仮説文を論理式に変換して記号操作を行った後に，論理式を自然言語文へ再変換してニューラルモデルを利用する方法が考えられる．
しかし，論理式からテキストへの変換は現状の技術では困難である\footnote{馬目ら\cite{manome-etal-2018-rnn}はLSTM (Long Short-Term Memory) \cite{HochSchm97}を用いて，高階論理式から文生成を行う手法を提案している．これは，高階論理式を自然言語文にデコードする試みであるが，単純なパターン以外の文のデコードは困難とされている．}．
そこで提案手法では，自然言語文を論理式に変換してタブロー法を適用するのではなく，タブロー法を自然言語文に適用できるように拡張するアプローチを取る．
具体的には，依存構造を付与した自然言語文をタブローのエントリに採用する．
タブロー規則は，依存構造情報をもとに，新しいエントリを導出する．
提案手法では，依存構造としてUniversal Dependencies (UD) \cite{de-marneffe-etal-2021-universal}を採用する．
提案手法の最初のステップは，前提と仮説の自然言語文に依存構造を与える処理であり，この処理には，UDに基づく任意の依存構造解析器を用いることができる．
図\ref{fig:udconvert}に依存構造の例を示す．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{タブローの構成}

本節では，依存構造に基づくタブロー法について述べる．
通常のタブロー法が，タブロー規則により複雑な論理式をより単純な論理式に分解するのに対して，提案手法では，依存構造に基づき，自然言語文をより単純な自然言語文に分解するタブロー規則を設計する．

提案手法におけるタブローのエントリは，四つ組$(D, v, a, o)$である．$D$は依存構造であり，$v$と$a$は通常のタブロー法と同様であり，それぞれ真偽値およびフラグである．
$o$は，そのエントリがどのエントリから導出されたかを表す．初期タブローのエントリ$e$は，自分自身から導出されたものとする．
すなわち$e = (D, v, 0, e)$という形をとる．
タブローは，通常のタブロー法と同じくタブロー規則を繰り返しエントリに適用することで導出される．
提案手法におけるタブロー規則の一般形は，次の表記で表される．
\[
r = (c_{1, 1}\wedge \cdots \wedge c_{1, n_1} ) \vee \cdots \vee ( c_{m, 1}\wedge \cdots \wedge c_{m, n_m} )
\]
ここで，$c_{i,j}$は，エントリ$(D, v, 0, o)$を受け取り，エントリ$(D', v', 0, o)$を返す任意の部分関数である．
$r$を構成するすべての$c_{i,j}$について，$c_{i,j}(e)$が未定義でないとき，タブロー規則$r$はエントリ$e$に\emph{適用可能}であるという．
タブロー中に，タブロー規則が適用可能なエントリ$e$が存在するとき，そのエントリが支配するすべての葉に，それらの子として新たな$m$個の経路$ \langle c_{1,1}(e) \cdots c_{1, n_1}(e) \rangle, \cdots, \langle c_{m,1}(e) \cdots c_{m,n_m}(e) \rangle$を追加する．
タブロー規則が適用されたエントリ$(D,v,0,o)$を$(D,v,1,o)$に置き換える．

図\ref{fig:rules-sample}にタブロー規則の例に示す．
この図において，根は入力として取ることができる依存構造（のパターン）と真偽値の対を表している．
すなわち，このパターンに合致しないような依存構造に対して$c_{i,j}$は未定義である．
根以外のラベルは各c$_{i,j}$に対応しており，入力されたエントリに対してどのようなエントリを返すかを表現している．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 3
\begin{figure}[b]
\begin{center}
\includegraphics{30-2ia13f3.pdf}
\end{center}
\caption{タブロー規則の例}
\label{fig:rules-sample}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

初期タブローを$e_1=$ (Either Smith or Anderson signed the contract, \texttt{T}, 0, $e_1$)，$e_2=$ (If Smith did not sign the contract Anderson made an agreement, \texttt{F}, 0, $e_2$)としたときのタブローの構成を例に，タブロー規則の適用の流れを説明する（完成したタブローを図\ref{fig:tableau-example}に示す）．
$e_2$: (If Smith did not sign the contract Anderson made an agreement, \texttt{F}, 0, $e_2$)に図\ref{fig:rules-sample}(a)の規則を適用すると，$e_2$が支配するすべての葉に新たな2つのエントリ$e_3$: (Smith did not sign the contract, \texttt{T}, 0, $e_2$)と$e_4$: (Anderson made an agreement, \texttt{F}, 0, $e_2$)が追加され，$e_2$のフラグが1に変更される．
次に，$e_3$: (Smith did not sign the contract, \texttt{T}, 0, $e_2$)に図\ref{fig:rules-sample}(b)の規則を適用すると，新たなエントリ$e_5$: (Smith signed the contract, \texttt{F}, 0, $e_2$)が追加され，$e_3$のフラグが1に変更される．
最後に，$e_1$: (Either Smith or Anderson signed the contract, \texttt{T}, 0, $e_1$)に図\ref{fig:rules-sample}(c)の規則を適用すると，新たな2つのエントリ$e_6$: (Smith signed the contract, \texttt{T}, 0, $e_1$)と$e_7$: (Anderson singned the contract, \texttt{T}, 0, $e_1$)が追加され，$e_1$のフラグは1に変更される．
以上により，タブローが構成される．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 4
\begin{figure}[b]
\begin{center}
\includegraphics{30-2ia13f4.pdf}
\end{center}
\caption{含意タブローの例}
\label{fig:tableau-example}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{タブローの閉鎖性判定}

一般のタブロー法においては，枝上に真偽値のみが異なるエントリが存在することをもって閉じた枝を定義している．
提案手法ではこれに加えてニューラルNLIモデルに基づく閉じた枝を定義する．
ニューラルNLIモデルは，前提文$p$と仮説文$h$を入力として受け取ると，それを含意(\texttt{E})，中立(\texttt{N})，矛盾(\texttt{C})のいずれかのクラスに分類するものとする．
以下では，$L \times L（Lは自然言語文の集合）$から集合$\{ \texttt{E}, \texttt{N}, \texttt{C} \}$への関数$\nu$を\emph{NLIシステム}と呼ぶ．
$\nu(p, h)=\texttt{E}$は$p$が$h$を含意することを表す．
\texttt{N}，及び\texttt{C}についても同様である．

提案手法では，枝上に次のいずれかが成り立つようなエントリ$e_1=(D_{s_1}, v_1, 0, o_1)$, $e_2=(D_{s_2}, v_2, 0, o_2)$（ただし$o_1 \neq o_2$）が存在するとき，その枝は閉じていると再定義する（閉じたタブローについてもこの再定義のもとで同様に再定義する）．
以下では再定義した3つの条件を，枝の\emph{閉鎖条件}と呼ぶ．
\begin {enumerate}
  \item $v_1=\texttt{T}$かつ$v_2=\texttt{F}$かつ$s_1 = s_2$
  \item $v_1=\texttt{T}$かつ$v_2=\texttt{T}$かつ$\nu(s_1, s_2)=\texttt{C}$
  \item $v_1=\texttt{T}$かつ$v_2=\texttt{F}$かつ$\nu(s_1, s_2)=\texttt{E}$
\end {enumerate}
閉鎖条件(1)は従来のタブロー法と同じである．
閉鎖条件(2)は，$s_1, s_2$が矛盾関係にあることと$e_1, e_2$の両方が真であることは両立しえないことに由来する条件である．
閉鎖条件(3)は，$s_1$が$s_2$を含意するとき，$s_1$が真ならば，$s_2$も真でなければならないが，エントリはそのようにはなっていないことを意味する．
閉鎖条件(2)，(3)については，4章において改めて議論する．
NLIシステムに応じてタブローが閉じているか否かが異なるため，以下では，いかなるNLIシステムのもとで閉じているかを明示する場合には，NLIシステム\emph{$\nu$のもとで閉じている}ということにする．

$o_1 \neq o_2$という条件は，前提から導出されたエントリ同士，あるいは仮説から導出されたエントリ同士について，閉鎖性の判定の対象から除外するものである．
これは前提や仮説が恒真（偽）でなければ問題となることはない．

タブローの閉鎖性判定の例について見るために，図\ref{fig:tableau-example}のタブローを考える．
また，
\[
\nu \bigl( sen(e_7), sen(e_4) \bigr) = \texttt{E}
\]
であると仮定する\footnote{ここで，$sen((D_s, v, a, o))=s$と定義する．}．
このタブローは2つの枝をもつが，左の枝$\langle e_1, e_2, e_3, e_4, e_5, e_6 \rangle$では，$e_6$: (Smith signed the contract, \texttt{T}, 0, $e_1$)，$e_5$: (Smith signed the contract, \texttt{F}, 0, $e_2$)が存在している．
この枝は閉鎖条件(1)を満たすので，閉じている．
一方，右の枝$\langle e_1, e_2, e_3, e_4, e_5, e_7 \rangle$では，$e_7$: (Anderson signed the contract, \texttt{T}, 0, $e_1$)，$e_4$: (Anderson made an agreement, \texttt{F}, 0, $e_2$)が存在している．
$\nu(sen(e_7), sen(e_4))=\texttt{E}$であるので，閉鎖条件(3)によってこの枝は閉じている．
したがって，図\ref{fig:tableau-example}のタブローは，仮定のようなNLIシステムの下で閉じている．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{推論的関係の同定}

含意タブロー，および矛盾タブローは，それぞれ前提と仮説の間に含意関係，矛盾関係が成り立つかどうかを判定するためのタブローである．
これらのタブローの閉鎖性と，仮説と前提の間の推論的関係は，Abzianidze \cite{abzianidze-2015-tableau}と同様に表\ref{table:closing-and-output}のように整理でき，これに従って推論的関係を同定する\footnote{含意関係も成立し，かつ，矛盾関係も成立すると判定される場合は，解釈不能であるためエラークラスとする．}．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% table 1
\begin{table}[t]
\input{13table01.tex}%
\caption{タブローの閉鎖性と推論的関係の対応}
\label{table:closing-and-output}
\end{table}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{提案手法の意味論}

本章では，3章で提案した手法の論理的な整合性を検証する．提案手法をモデル理論的に定式化し，手法の性質とその限界を理論的に明らかにする．
具体的には，提案手法において健全性が常に成立する一方で，完全性が一般には成立しないことを示す．
本章で使用する記号とその説明を表\ref{table:symbols}に示す．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% table 2
\begin{table}[t]
\input{13table02.tex}%
\caption{提案手法の定式化に使用する記号}
\label{table:symbols}
\end{table}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{モデル}

本節では，提案するタブロー法を形式的に議論するために，まず，その基盤となるモデル理論的な文の解釈について定義する．
次に，モデルに基づいて，タブロー規則，およびNLIシステムを特徴付け，タブロー規則により導出された完成したタブローにおけるNLIシステムを用いた閉鎖性判定のもつ性質を明らかにする．

まず，モデルを定義する．
\begin{dfn}[モデル]
  \label{dfn:sentence-model}
  $L$（$L$は自然言語文の集合）から$\{ \texttt{T}, \texttt{F} \}$への関数$m$をモデルと呼ぶ．$\mathcal{M}$をすべてのモデルの集合とする．
  モデルの集合$M \subseteq \mathcal{M}$に対して，$M(s)=\{m \in M \mid m(s) = \texttt{T}\}$と定義する．
\end{dfn}

以下では，モデル集合$M$が与えられたとき\footnote{ここですべてのモデルの集合$\mathcal{M}$ではなく，その部分集合$M$を考えるのは，$\mathcal{M}$の中には，論理的に不自然なモデル，例えば，すべての自然言語文に対して\texttt{T}を返すようなモデルが含まれるからである．論理的に自然なモデルの集合が仮に$M$として与えられたものとして以下では議論を進める．なお，$M$に対して何の条件も課さないため，$M$がどのような集合であっても以下の議論は成り立つ．}，$M$と整合性のとれたNLIシステム，およびタブロー規則がどのようなものであるかを定義し，整合性が取れているという条件の下で提案手法による推論的関係の同定の理論的限界を明らかにする．
\begin{dfn}
  \label{dfn:nli-system-consistent}
  次の3つの条件が全て成り立つとき，NLIシステム$\nu$はモデル集合$M$と\emph{整合的}であるという．なお，$s_1, s_2 \in L$とする．
  \begin{itemize}
    \item$M(s_1) \subseteq M(s_2)$ならば，かつ，そのときのみ$\nu(s_1, s_2) = \texttt{E}$
    \item $\neg (M(s_1) \subseteq M(s_2)) \land \neg (M(s_1) \cap M(s_2) = \emptyset)$ならば，かつ，そのときのみ$\nu(s_1, s_2) = \texttt{N}$
    \item $M(s_1) \cap M(s_2) = \emptyset$ならば，かつ，そのときのみ$\nu(s_1, s_2) = \texttt{C}$
  \end{itemize}
\end{dfn}
この定義では，含意関係をモデル集合の包含関係として，矛盾関係を互いに素な関係として捉えている．

以下では，モデルに基づいてタブローを特徴付ける．その準備として，エントリ，タブローの枝，タブローに対応するモデルを，$M(s)$を拡張することにより定義する．
\begin{dfn}[エントリに対するモデル集合]
  \label{dfn:entry-model}
  タブローのエントリ$e=(D_s, v, a, o)$に対して，$M(e)$を次のように定義する．
\[
    M(e) =
    \begin{cases}
      M(s) & (v=\texttt{T}) \\
      M - M(s) & (v=\texttt{F})
    \end{cases}
\]
\end{dfn}
\begin{dfn}[タブローの枝に対するモデル集合]
  \label{dfn:branch-model}
  タブローの枝$b$に対して，$M(b)$を次のように定義する．
\[
M(b) = \bigcap_{e \in b} M(e)
\]
\end{dfn}
\begin{dfn}[タブローに対するモデル集合]
  \label{dfn:equal-branch-model-tableau-model}
  タブロー$t$に含まれる全ての枝の集合を$B$とする．$M(t)$を次のように定義する．
\[
M(t) = \bigcup_{b \in B} M(b)
\]
\end{dfn}
提案手法では，タブロー規則の適用前後で，エントリが表現する制約が等価であることを想定しており，この性質を以下のように定義する．
\begin{dfn}
  \label{dfn:tableau-rule-consistent}
  $r = (c_{1, 1}\wedge \cdots \wedge c_{1, n_1} ) \vee \cdots \vee ( c_{m, 1}\wedge \cdots \wedge c_{m, n_m} )$，$E$をすべてのエントリの集合とし，$E_r = \{ e \in E \mid rはeに適用可能 \}$とする．任意の$e \in E_r $に対して次の条件が満たされるとき，タブロー規則$r$はモデル集合$M$と\emph{整合的}であるという．
\[
M(e) = \biggl( M \bigl( c_{1, 1}(e) \bigr) \cap \cdots \cap M \bigl( c_{1, n_1}(e) \bigr) \biggr) \cup \cdots \cup \biggl( M \bigl( c_{m, 1}(e) \bigr) \cap \cdots \cap M \bigl( c_{m, n_m}(e) \bigr) \biggr)
\]
この等式において，左辺は，エントリ$e$に対する制約に相当する．
  右辺は，エントリ$e$にタブロー規則$r$を適用した結果，導出されるエントリにより表現される制約に対応する．
  また，任意の$r \in R$が$M$と整合的であるとき，$R$は$M$と\emph{整合的}であるという．
\end{dfn}

提案手法の振る舞いは，タブロー規則の集合$R$とNLIシステム$\nu$によって定まる．
以下では，この対$(R,\nu)$を\emph{証明システム}とよび，$R$と$\nu$がモデル$M$と整合的であるとき，\emph{$(R,\nu)$は$M$と整合的である}という．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{健全性と完全性}

本節では，前節で定義したモデルに基づき提案手法の健全性と完全性を定義する．
任意の証明システムについて健全性が成り立つことを証明し，完全性について反例を示す．

ここで定義する健全性とは，含意（矛盾）タブローが閉じているとき，前提と仮説に対するモデル集合は，包含（互いに素な）関係にあるという性質である．
定義は以下のとおりである．
\begin{dfn}[含意タブロー，および矛盾タブローの健全性]
  \label{dfn:entailment-tableau-kenzen}
  $M$をモデル集合，$(R,\nu)$を$M$と整合的な証明システムとする．
  任意の前提文$p$と仮説文$h$について，次の条件が成り立つならば，$(R, \nu)$は，モデル集合$M$において\emph{健全}であるという．
  \begin{itemize}
    \item $R$によって構成された含意タブローが$\nu$のもとで閉じているならば，$M(p) \subseteq M(h)$．
    \item $R$によって構成された矛盾タブローが$\nu$のもとで閉じているならば，$M(p) \cap M(h) = \emptyset$．
  \end{itemize}
\end{dfn}
一方で，完全性を次のように定義する．
\begin{dfn}[含意タブロー，および矛盾タブローの完全性]
  \label{dfn:entailment-tableau-kanzen}
  $M$をモデル集合，$(R,\nu)$を$M$と整合的な証明システムとする．
  任意の前提文$p$と仮説文$h$について，次の条件が成り立つならば，$(R,\nu)$は，モデル集合$M$において\emph{完全}であるという．
  \begin{itemize}
    \item $M(p) \subseteq M(h)$ならば，$R$によって構成された含意タブローが$\nu$のもとで閉じている．
    \item $M(p) \cap M(h) = \emptyset$ならば，$R$によって構成された矛盾タブローが$\nu$のもとで閉じている．
  \end{itemize}
\end{dfn}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{健全性の証明}

本節では，健全性に関する以下の定理を証明する．
\begin{thm}[健全性の定理]
  \label{thm:kenzensei}
  $M$をモデル集合とする．
  $M$と整合的な任意の証明システムは，$M$において健全である．
\end{thm}
以下では，まず定理\ref{thm:kenzensei}を証明するための補助定理を導入し，それにも基づき定理\ref{thm:kenzensei}を証明する．
\begin{lem}
  \label{thm:entry-model-immutable-all}
  $R$が$M$と整合的であるならば，$t \stackrel{R}{\rhd} t'$を満たす任意のタブロー$t$と$t'$において次が成立する．
\[
M(t)=M(t')
\]
\end{lem}
補助定理\ref{thm:entry-model-immutable-all}は定義\ref{dfn:tableau-rule-consistent}から明らかである．

\begin{lem}
  \label{thm:tableau-model-immutable-all}
  $t$と$t'$をタブローとし，$t \stackrel{R}{\rhd^{*}} t'$とする．
  $R$が$M$と整合的であるならば，$M(t)=M(t')$．
\end{lem}
補助定理\ref{thm:tableau-model-immutable-all}は補助定理\ref{thm:entry-model-immutable-all}から明らかである．

含意タブローの健全性の証明は次の通りである．

\begin{proof}
  $R$によって構成された含意タブロー$t_\textrm{comp}$が$\nu$のもとで閉じているとする．
  このとき，$t_\textrm{comp}$のすべての枝$b$に閉鎖条件のいずれかを満たす2つのエントリ$e_1 = (D_{s_1}, v_1, 0, o_1)$，$e_2 = (D_{s_2}, v_2, 0, o_2)$（ただし$o_1 \neq o_2$）が存在する．
  \begin{itemize}
    \item 閉鎖条件(1)を満たすならば，$s_1 = s_2$．したがって，定義\ref{dfn:entry-model}より$M(e_1) \cap M(e_2) = M \bigl( (D_{s_1}, \texttt{T}, 0, o_1) \bigr) \cap M \bigl( (D_{s_2}, \texttt{F}, 0, o_2) \bigr) = \emptyset$．
    \item 閉鎖条件(2)を満たすならば，$\nu(s_1, s_2)=\texttt{C}$．$\nu$は$M$と整合的であるから，定義\ref{dfn:nli-system-consistent}より$M(s_1) \cap M(s_2) = \emptyset$．よって，定義\ref{dfn:entry-model}より$M(s_1) \cap M(s_2) = M \bigl( (D_{s_1}, \texttt{T}, 0, o_1) \bigr) \cap M \bigl( (D_{s_2}, \texttt{T}, 0, o_2) \bigr) = M(e_1) \cap M(e_2) = \emptyset$．
    \item 閉鎖条件(3)を満たすならば，$\nu(s_1, s_2)=\texttt{E}$．$\nu$は$M$と整合的であるから，定義\ref{dfn:nli-system-consistent}より$M(s_1) \subseteq M(s_2)$．定義\ref{dfn:entry-model}より$M(e_1) = M(s_1)$，$M(e_2) = M - M(s_1)$．ここで$M(s_1) \subseteq M(s_2)$であるから，$M(e_1) \cap M(e_2) = \emptyset$．
  \end{itemize}

  以上より，$M(e_1) \cap M(e_2) = \emptyset$．
  ゆえに，定義\ref{dfn:branch-model}より$M(b) = \emptyset$となる．
  したがって，すべての$t$中の枝$b$について$M(b) = \emptyset$であるので，定義\ref{dfn:equal-branch-model-tableau-model}から$M(t_\textrm{comp}) = \emptyset$である．
  $t_\textrm{start}$を初期タブローとすると，$t_\textrm{start} \stackrel{R}{\rhd^{*}} t_\textrm{comp}$であるので補助定理\ref{thm:tableau-model-immutable-all}から$M(t_\textrm{start}) = \emptyset$である．
  初期タブローは$e_1 = (D_{p}, \texttt{T}, 0, e_1)$，$e_2 = (D_{h}, \texttt{F}, 0, e_2)$から構成されるため，定義\ref{dfn:branch-model}と\ref{dfn:equal-branch-model-tableau-model}から$M \bigl( (D_{p}, \texttt{T}, 0, e_1) \bigr) \cap M \bigl( (D_{h}, \texttt{F}, 0, e_2) \bigr) = \emptyset$である．
  したがって，$M \bigl( (D_{p}, \texttt{T}, 0, e_1) \bigr) \subseteq M \bigl( (D_{h}, \texttt{T}, 0, e_2) \bigr)$．
  定義\ref{dfn:entry-model}から$M(p) \subseteq M(h)$である．
  以上より定義\ref{dfn:entailment-tableau-kenzen}の1番目の条件は満たされる．
  矛盾タブローに関する2番目の条件も同様に証明できる．
  すなわち，証明システム$(R, \nu)$は$M$において健全である．
\end{proof}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{完全性の反例}

本節では，完全性が一般には成立しないことを反例を用いて説明する．

完全性が一般に成り立たないことを示すには，次の条件を満たすモデル集合$M$，証明システム$(R, \nu)$，前提文$p$，仮説文$h$が存在することを示せば十分である．
\begin{description}
  \item [条件1] $M(p) \subseteq M(h)$
  \item [条件2] $(R, \nu)$は$M$と整合的である．
  \item [条件3] $R$によって構成された$p$と$h$の含意タブローは$\nu$のもとで閉じていない．
\end{description}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% table 3
\begin{table}[b]
\input{13table03.tex}%
\caption{完全性が成立しないモデルの例}
\label{table:not-kanzen-tableau-sample}
\end{table}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 5
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f5.pdf}
\end{center}
\caption{タブローの完全性の反例}
\label{fig:not-kanzen-tableau-sample}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

次のインスタンス，表\ref{table:not-kanzen-tableau-sample}に示すモデル$M$，図\ref{fig:not-kanzen-tableau-sample}に示すタブローを構成する証明システム$(R,\nu)$（$\nu$は$M$と整合的なものを任意に選んでよい）は，上の条件を満たす，完全性が一般には成り立たないことを示す反例となっている．
\begin{description}
  \item{\textbf{前提}}: Smith and Anderson did not go out.
  \item{\textbf{仮説}}: Smith and Anderson were home.
  \item{\textbf{推論的関係}}: 含意
\end{description}
$M(p) = M(h) = \{m_1\}$であるので，$M(p) \subseteq M(h)$ である．すなわち条件1を満たす．
$M(e_1) = M(e_3) = M(e_4) \cap M(e_5) = \{m_1\}，M(e_2) = M(e_6) \cup M(e_7) = \{m_2, m_3, m_4\}$であることから，このタブローの構成に用いられたタブロー規則は$M$と整合的である．$\nu$は$M$と整合的であるので，$(R,\nu)$は$M$と整合的である．すなわち条件2を満たす．
図\ref{fig:not-kanzen-tableau-sample}の含意タブローにおいてタブロー規則が未適用であるエントリ$e_4$，$e_5$，$e_6$，$e_7$ の真偽値はいずれも\texttt{F}である．3.3 節で述べた閉鎖条件に現れるエントリのペアは，いずれかのエントリの真偽値が\texttt{T} でなければならない．
このため，この含意タブローにおいて，閉鎖条件を満たすエントリの対は存在せず，$\nu$のもとでこのタブローが閉じていることはあり得ない．（条件3を満たす）．
以上から，$M$, $(R, \nu)$, $p$, $h$ は完全性が一般には成り立たないことを示す反例となっている．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{実験}

提案手法における論理的な推論過程の明示可能性を評価すること，
\pagebreak
及び，提案手法の欠点を明らかにすることを目的に，下記の準備のもと実験を実施した\footnote{実装したコードは \url{https://github.com/ayahito-saji/nli-tableau-ml} から利用できる．}．
\begin{description}
  \item[データセット] %
  ニューラルNLIモデルの構築，および評価用データセットとしてSNLIコーパスを使用した．
  SNLIコーパスには，訓練データとして549,367件，開発データとして9,842件，テストデータとして9,824件が含まれている\footnote{ラベルなしと分類されているデータはすべて取り除いた．}．

  \item[依存構造解析]
  依存構造解析器としてUdify \cite{kondratyuk-straka-2019-75}，およびUdify事前学習モデルを用いた\footnote{\url{https://github.com/Hyperparticle/udify} を使用した．}．
  UdifyはMultilingual BERT\footnote{\url{https://github.com/google-research/bert/blob/master/multilingual.md}} ベースの多言語対応の依存構造解析器であり，UDに基づく依存構造を出力する．
  \item[ニューラルNLIモデル]
  フレームワーク内で使用するニューラルNLIモデルとして，LSTMに基づくニューラルNLIモデルであるESIM \cite{chen-etal-2017-enhanced}を採用した\footnote{\url{https://github.com/coetaur0/ESIM} の実装を使用した．}．
  ESIMのパラメータは，SNLIコーパスの訓練用データと開発用データを用いて学習した．
  \item[タブロー規則]
  タブロー規則として，命題論理のタブロー法の連言，選言，否定，条件法の4つの規則に相当する規則を合計32個作成した．
  作成したタブロー規則について付録Aにまとめる．
  連言，選言については，文の等位接続だけでなく，UDのcore argument（主語，目的語など）の等位接続を扱える規則となっている．
\end{description}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{推論過程の明示可能性}

提案手法における推論過程の明示可能性を評価するために，含意タブロー，および矛盾タブローのサイズ（エントリの数）を測定した．
提案手法はタブロー規則の適用により推論の明示化を行っており，タブローのサイズは推論の明示化の程度を評価する指標である．
含意タブローと矛盾タブローのサイズの分布を図\ref{fig:tableau_size}の左と右にそれぞれ示す．
サイズが2となる（タブロー規則が適用されなかった）推論も多いが，一方で，サイズが4以上となる（タブロー規則が複数回適用された）推論も少なくなく，提案手法における明示可能性が示された．
なお，何らかのタブロー規則が適用されたインスタンスは，9,824件中800件であった．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 6
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f6.pdf}
\end{center}
\caption{含意タブロー（左）と矛盾タブロー（右）のサイズの分布}
\label{fig:tableau_size}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

実験データ内のあるインスタンスを対象に，提案手法による推論がどのように行われたのかを分析した．
\begin{description}
  \item{\textbf{前提}}: A little boy is standing in front of a wedding party laughing.
  \item{\textbf{仮説}}: There is a bride and groom behind the little boy.
  \item{\textbf{推論的関係}}: 含意
\end{description}
図\ref{fig:correct-tableau-example}に，このインスタンスに対して作成された含意タブローを示す．
この例では，$e_2$に含まれる等位構造``a bride and groom''が``groom''と``bride''に分解され，それぞれ$e_3$と$e_4$として導出された後，それらが$e_1$と矛盾することを正しく判定できている．
すなわち，タブロー法に基づいて名詞句の等位構造により表現された連言を分解する推論過程を明示化できている．
一方で，記号操作的アプローチでは扱いが難しい``wedding party''と``groom''，``bride''といった単語の類似関係や``in front of''と``behind''といった異なる単語（列）によって表現された位置の関係は，ニューラルモデルにより柔軟に扱うことができている．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 7
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f7.pdf}
\end{center}
\caption{正しい含意タブローの例}
\label{fig:correct-tableau-example}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% table 4
\begin{table}[b]
\input{13table04.tex}%
\caption{提案手法とニューラルNLIモデルの予測結果}
\label{table:result-tableau-ml-result}
\end{table}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% table 5
\begin{table}[b]
\input{13table05.tex}%
\caption{提案手法とニューラルNLIモデルの正解率}
\label{table:result-tableau-ml-result-2}
\end{table}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{誤り分析}

タブロー法とニューラルNLIモデルを組み合わせる提案手法の問題点を明らかにするために，提案手法において何らかのタブロー規則が適用された800件を対象に，その推論性能を測定した．
提案手法による結果，及び，ニューラルNLIモデルによる結果を表\ref{table:result-tableau-ml-result}，および表\ref{table:result-tableau-ml-result-2}に併せて示す．
なお，「エラー」とは，3.4節の表\ref{table:closing-and-output}に示したように，含意関係と矛盾関係のいずれも成立すると判定され，解釈不能であることを示すラベルである．
推論性能として，標準的な評価指標である正解率，再現率，精度，$F_1$値を求めた\footnote{提案手法の目的は，NLIタスクの性能向上にはない点に注意．}．
$F_1$値は，以下で定義する再現率と精度の調和平均である．
\begin{align*}
\textrm{Recall}_A & = \frac{\textrm{TP}_A}{\textrm{True}_A} \\
\textrm{Precision}_A & = \frac{\textrm{TP}_A}{\textrm{Positive}_A}
\end{align*}
ここで，$A$ は「含意」，「中立」，「矛盾」のいずれかのラベルを表し，$\textrm{TP}_A$は正解ラベルと予測ラベルがクラス$A$ であるインスタンス数，$\textrm{True}_A$ は正解ラベルがクラス$A$ であるインスタンス数，$\textrm{Positive}_A$は予測ラベルがクラス$A$ であるインスタンス数である．
提案手法は，ニューラルNLIモデルと比べて，正解率の低下がみられた．

以下では，提案手法においてタブロー規則が適用され，かつ誤りが生じたケースについて，その要因を分析し，考察する．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{誤りの原因の分析}

本節では，開発データ中においてタブロー規則が適用された762件のインスタンスを用いて提案手法が推論的関係を誤って同定した原因を分析する．
開発データに対して提案手法を適用した予測結果の混合行列を表\ref{table:result-tableau-dev}に示す．
開発データの結果はテストデータと大きな乖離がなく，誤りの原因についても同様の傾向が見られた．
誤って予測したインスタンスの合計は268件であった．
この268件の中で，正解ラベルが誤っていたインスタンスは35件存在した．
正解ラベルを修正したところ，そのうち16件は提案手法によって正しく推論的関係を同定できていた．
また，文中の単語の誤りによって意味が通らないインスタンスが4件存在した．
そこで，以上の20件を除いた248件のインスタンスについて，その閉鎖性判定が誤っているタブロー292個\footnote{正解クラスが「含意」で，予測ラベルが「矛盾」である場合のように，含意タブローと矛盾タブローの両方が誤っている場合はいずれもがカウントされる．}を，次の4つに分類した\footnote{提案手法では，依存構造解析，タブロー規則の適用によるタブローの構成，NLIシステムによるタブローの閉鎖性判定の順に処理を行う．誤りが最初に生じた処理のみを，閉鎖性判定の誤りの要因として扱った．}．
\begin{itemize}
  \item NLIシステムに起因する誤り（5.2.2節）
  \item タブロー規則に起因する誤り（5.2.3節）
  \item 依存構造解析に起因する誤り（5.2.4節）
  \item 提案手法の限界に起因する誤り（5.2.5節）
\end{itemize}
それぞれに該当するタブローの数を表\ref{table:reason-of-failure}に示す．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% table 6
\begin{table}[b]
\input{13table06.tex}%
\caption{開発データに対する提案手法の予測結果}
\label{table:result-tableau-dev}
\end{table}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% table 7
\begin{table}[b]
\input{13table07.tex}%
\caption{開発データにおける誤りの要因}
\label{table:reason-of-failure}
\end{table}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

以下では具体例を挙げながら，各誤りについて説明する．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{NLIシステムに起因する誤り}

本節では，NLIシステムに起因する誤りについて説明する．
292個の誤りのうち，239個の誤りは，NLIシステムが推論的関係の同定を誤ったことが原因である．
例として，以下のインスタンス
\begin{description}
  \item{\textbf{前提}}: Two people are in a green forest.
  \item{\textbf{仮説}}: The forest is not dead.
  \item{\textbf{推論的関係}}: 含意
\end{description}
に対して生成された含意タブローを図\ref{fig:error-tableau-nli1}に示す．
このインスタンスの推論的関係は「含意」であるため，含意タブローは閉じなければならないが，閉じていなかった．$\textrm{sen}(e_1)$における``green forest''と$\textrm{sen}(e_3)$=``The forest is dead''から，正しくは$\nu(\textrm{sen}(e_1), \textrm{sen}(e_3))=\texttt{C}$であると考えられるが，$\nu(\textrm{sen}(e_1), \textrm{sen}(e_3))=\texttt{N}$と判定されたために，閉鎖条件(2)を満たさず，このタブローは閉じていない．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 8
\begin{figure}[b]
\begin{center}
\includegraphics{30-2ia13f8.pdf}
\end{center}
\caption{NLIシステムに起因して誤った含意タブローの例}
\label{fig:error-tableau-nli1}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

また，NLIシステムの推論的関係の同定の誤り239個のうち，SNLI コーパスから学習したニューラルモデルがもつある特性が原因であると考えられるものが141個存在した．
例として，以下のインスタンス
\begin{description}
  \item{\textbf{前提}}: A man and woman walk atop a hill.
  \item{\textbf{仮説}}: A man and woman are walking.
  \item{\textbf{推論的関係}}: 含意
\end{description}
に対して生成された矛盾タブローを図\ref{fig:error-tableau-nli2}に示す．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 9
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f9.pdf}
\end{center}
\caption{NLIシステムに起因して誤った矛盾タブローの例}
\label{fig:error-tableau-nli2}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

推論的関係は「含意」であるこのタブローのエントリ$e_3$と$e_6$について，$\nu(\textrm{sen}(e_3), \textrm{sen}(e_6))=\texttt{C}$と判定された．そのため，$\nu$のもとでこの矛盾タブローは閉じてしまい，正しい推論的関係を同定できなかった．

$\textrm{sen}(e_3)$と$\textrm{sen}(e_6)$の間の推論的関係には，ある種の不確定性が存在することが，文献\cite{bowman-etal-2015-large}において指摘されている．
名詞句が参照する実体が同一であるか否かに応じて推論的関係が異なる場合があり，$\textrm{sen}(e_3)$と$\textrm{sen}(e_6)$の推論的関係においては ``a man'' と ``woman'' が同一の実体を参照するとすればその推論的関係は「矛盾」であるが，同一の実体を参照しないとすれば「中立」である．
SNLIコーパスにおいては，同一の実体を参照するという想定のもとで推論的関係が定められる傾向にあり，SNLIコーパスに基づき構築されたESIMもその傾向を持っていると考えられる．
ここで注目すべきポイントは，提案したタブロー法による推論によってこの事実を捉えることができた点である．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{タブロー規則に起因する誤り}

本節では，タブロー規則の適用に起因する誤りについて説明する．
タブロー規則を適用することにより不適格文が生成されるケースが確認された．
例えば，次のようなインスタンスが存在した．
\begin{description}
  \item{\textbf{前提}}: The man and woman are both smiling.
  \item{\textbf{仮説}}: A guy and a lady are standing near each other.
  \item{\textbf{推論的関係}}: 中立
\end{description}
この仮説文に対してタブロー規則を適用した結果を図\ref{fig:error-tableau-rule1}に示す．
ここで，$e_1$に含まれる``each other''は，``a guy''が``a lady''を，``a lady''が``a guy'' を先行詞とする相互代名詞であるものの，タブロー規則を適用した結果得られる$e_2$と$e_3$では先行詞が存在しなくなるため，不適格文となる．
タブロー規則を適用した結果，不適格文が生成されたタブローは19個存在した．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 10
\begin{figure}[b]
\begin{center}
\includegraphics{30-2ia13f10.pdf}
\end{center}
\caption{タブロー規則の適用により意味的に不適格な文が生成される例}
\label{fig:error-tableau-rule1}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

別の誤りの要因としては，not + any を含む文に対して否定に関するタブロー規則を適用することによるものが挙げられる．例えば，
\begin{description}
  \item{\textbf{前提}}: A cement truck pours cement on the street.
  \item{\textbf{仮説}}: The truck isn't doing anything.
  \item{\textbf{推論的関係}}: 矛盾
\end{description}
の仮説文に否定に関するタブロー規則を適用すると，図\ref{fig:error-tableau-rule2}のようになる．
$e_1$と$e_2$は等価な制約を表していない．
$e_2$における``anything''を``something''に置き換えれば等価な制約を表せるものの，現状のタブロー規則ではnotを単純に取り除くことしかできない．
このような原因により誤りが生じたタブローは17個存在した．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 11
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f11.pdf}
\end{center}
\caption{not + any を含むエントリに対するタブロー規則の適用の例}
\label{fig:error-tableau-rule2}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

他の誤りの要因として，非合成的な要素（イディオム，固有名詞など）をタブロー規則が分解してしまうことが挙げられる．
以下のインスタンスでは，図\ref{fig:error-tableau-rule3}のように，仮説文に含まれる``hide and seek''というイディオムが分解されたために，意味的に不適格な文が生成されている．
\begin{description}
  \item{\textbf{前提}}: A small child is sitting on a stump in a forest clearing.
  \item{\textbf{仮説}}: A little boy is playing hide and seek in the woods.
  \item{\textbf{推論的関係}}: 矛盾
\end{description}
このようなタブローは2個存在した．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 12
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f12.pdf}
\end{center}
\caption{非合成的な要素を含むエントリの誤った分解}
\label{fig:error-tableau-rule3}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{依存構造解析に起因する誤り}

前提文，または仮説文の依存構造解析に誤っているタブローは53個存在した．
このうち，タブロー規則がマッチする部分における解析誤りによって，意味的に不適格な文が生成されたタブローは3個存在した．
例えば，次のインスタンス
\begin{description}
  \item{\textbf{前提}}: A male and a female with a black hat, and sunglasses stop and talk.
  \item{\textbf{仮説}}: Man and woman stop and chat with each other.
  \item{\textbf{推論的関係}}: 含意
\end{description}
の前提文は，正しくは図\ref{fig:error-tableau-ud-correct}のような依存構造を持つが，依存構造解析の誤りによって図\ref{fig:error-tableau-ud}のように分解されてしまい，意味的に不適格な文``Sunglasses stop and talk.'' が生成されている．
残りのタブロー50個における依存構造解析誤りの影響はみられなかった．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 13
\begin{figure}[b]
\begin{center}
\includegraphics{30-2ia13f13.pdf}
\end{center}
\caption{``A male and a female with a black hat, and sunglasses stop and talk.''の正しい依存構造}
\label{fig:error-tableau-ud-correct}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 14
\begin{figure}[b]
\begin{center}
\includegraphics{30-2ia13f14.pdf}
\end{center}
\caption{依存構造解析の誤りによる意味的に不適格な文の生成}
\label{fig:error-tableau-ud}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 15
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f15.pdf}
\end{center}
\caption{提案手法の限界に起因する誤った含意タブローの例}
\label{fig:error-tableau-limit}
\vspace{-0.5\Cvs}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{提案手法の限界に起因する誤り}

NLIシステム，タブロー規則の適用，依存構造解析のいずれにも誤りがないにもかかわらず，推論的関係の同定を誤ったものは，提案手法の限界，すなわち完全性が一般には成り立たないことに起因するものと位置づけられる．
例として，以下のインスタンス
\begin{description}
  \item{\textbf{前提}}: Two men and one woman are performing music on a stage.
  \item{\textbf{仮説}}: Three musicians are performing at a concert.
  \item{\textbf{推論的関係}}: 含意
\end{description}
に対して生成された含意タブローを図\ref{fig:error-tableau-limit}に示す．
このタブローでは，正しく依存構造解析が行われており，$e_1$は$e_3$および$e_4$に分解されているが，タブロー規則の適用に誤りはない．
また，$\nu(\textrm{sen}(e_3), \textrm{sen}(e_2))=\texttt{N}$，$\nu(\textrm{sen}(e_4), \textrm{sen}(e_2))=\texttt{N}$であり，NLIモデルも正しい．
前提と仮説の間の推論的関係は「含意」であり，このタブローは閉じられる必要があるが，閉じていない．
これは，この提案手法の完全性が一般には成立しないことによるものと位置づけられる．
このように，実際のデータセット中でも，完全性が一般に成立しないために推論的関係を正しく同定できなかったインスタンスが存在することがわかった．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{関連研究}

提案手法は，
\pagebreak
構文構造を用いて推論を行う自然論理(Natural Logic) \cite{lakoff1970linguistics}のアイデアに基づく手法と位置付けられる．
本章では，自然論理に基づく従来のNLI手法と提案手法を定性的に比較する．

自然論理に基づくNLI手法は，遷移に基づく手法と証明に基づく手法に大別できる．

遷移に基づく手法では，前提の自然言語文を仮説の自然言語文へと何らかの操作を用いて変換する．
Bar-Haimら\cite{bar2007semantic}は，依存構造に基づく変換操作を提案している．
この変換操作は，含意関係を保存するような操作に限られ，前提から仮説への変換が成功することは，前提と仮説の間に含意関係が成り立つことを意味する．
MacCartneyら\cite{maccartney-manning-2008-modeling}は，NatLogと呼ばれるシステムを提案している．
このシステムは単調性に関する推論\cite{maccartney-manning-2009-extended}に基づいている．
これらの手法は，自然言語文を直接的に扱うという点で提案手法と同様であるが，NLIモデルと統合できるかどうかは明らかではない．
また，遷移に基づくこれらの手法は，前提が複数の文からなる問題を本質的に解くことができないが，提案手法は初期タブローのエントリとして前提を加えるだけでこのような問題にも適用可能である．

証明に基づく手法として，Abzianidze \cite{abzianidze-2017-langpro}は，LangProと呼ばれるタブロー法に基づくシステムを，Huら \cite{hu-etal-2020-monalog}はMonaLogと呼ばれる単調性推論に基づくシステムを開発している．
これらのシステムでは，自然言語文に似た意味表現を採用しているが，あくまでも似た意味表現であって自然言語文ではない．
このため，提案手法のようにニューラルNLIモデルと証明システムを組み合わせることはできない．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{おわりに}

本論文では，タブロー法とニューラルモデルを用いてNLIを行う手法を提案した．
提案手法をモデル理論的に定式化し，一般に，健全性は成り立つが完全性は成り立たないことを示した．
また，SNLIコーパスを用いた実験により，提案手法の振る舞いを分析した．
今後の発展として，タブロー規則の充実や多言語への対応などが考えられる．
今回の実験では，命題論理に対するタブロー規則を作成し利用したが，より広範に提案手法を適用できるようにするために，量化，時相，様相，命題的態度などの現象を扱うことが可能なタブロー規則を整備する必要がある．
高階論理に対するタブロー法のための規則の拡充法がAbzianidze \cite{abzianidze-2015-tableau}により提案されており，それを本手法に応用することが一つのアプローチとして考えられる．
また，今回の実験では，データセットの前提と仮説をそのまま用いてニューラルモデルを学習したが，
タブロー法に従って前提と仮説をより小さい文に分解した上で，それに基づきモデルを構築する手法の検討も今後の課題である．


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\acknowledgment

本研究は，一部，科学研究費補助金基盤研究 (C) (No. 22K12148) により実施したものである．



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliographystyle{jnlpbbl_1.7}
\bibliography{13refs}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\appendix

\section{付録A}

  図\ref{fig:rule-list}に，実験の際に関数として作成したタブロー規則の一覧を示す．
  ここで$C, C_i, C'_i$は任意の依存構造である．
  また，$X$は依存関係であり，$ X \in \{\textrm{nsubj}, \textrm{csubj}, \textrm{obj}, \textrm{iobj}, \textrm{ccomp}, \textrm{xcomp} \}$である．

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% fig. 16
\begin{figure}[t]
\begin{center}
\includegraphics{30-2ia13f16.pdf}
\end{center}
\caption{作成したタブロー規則の一覧}
\label{fig:rule-list}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\vspace{2\Cvs}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{biography}

\bioauthor{佐治　礼仁}{
2021年名古屋大学情報学部卒．
2023年，同大学院情報学研究科博士前期課程修了．
現在，ヤフー株式会社に在籍中．
}

\bioauthor{高尾　大樹}{
2017年名古屋大学工学部卒．
2019年同大学大学院情報学研究科博士前期課程修了．
現在，同博士後期課程在学中．
}
\bioauthor{加藤　芳秀}{
2003年名古屋大学大学院工学研究科情報工学専攻博士課程後期課程修了．
博士（工学）．
同大助手，助教等を経て，准教授．
言語処理学会，情報処理学会，人工知能学会，電子情報通信学会，ACL各会員．
}
\bioauthor{松原　茂樹}{
1998年名古屋大学大学院工学研究科情報工学専攻博士課程修了．
博士（工学）．
同大助手，助教授，准教授を経て，2017年名古屋大学教授．
}

\end{biography}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\biodate




\end{document}

