# ニューラルモデルとタブロー法を用いた自然言語推論

佐治 礼仁 ${ }^{\dagger, \dagger \dagger} \cdot$ 高尾 大樹 $\dagger \cdot$ 加藤 芳秀 $+\dagger \dagger \cdot$ 松原 茂樹 $\dagger,+\dagger \dagger \dagger$

自然言語推論 (NLI)は，2つのテキストの間に成り立つ推論的関係を同定する夕ス クである。近年, ニューラルモデルに基づくアプローチが高い正答率を達成してい る.しかし, このアプローチに基づく NLI は, 判定結果に至る過程や理由を説明す る能力を有していないという問題がある。一方，NLI では以前より，記号操作に基 づくアプローチが提案されてきた。このアプローチは, 推論の論理的な過程を明示 でき, 推論の根拠を示すことができるものの, 語の意味的知識や常識的な知識を十分に備えることは容易でなく, 高い推論性能の達成は難しいという問題がある。 そ こで本論文では，夕ブロー法とニューラルモデルを組み合わせた手法を提案する。 タブロー法は, 推論規則の適用に基づく論理式の分解, 及び, 論理式への真偽值割 り当てが存在するか否かの検査から構成される，本手法ではこのうち，真偽値割り 当ての検査にニューラルモデルを用いる。なお，夕ブロー法では通常，論理式を操作対象とするのに対し, 本手法では依存構造を対象とする。依存構造を用いること により，ニューラル NLI モデルをタブロー法アルゴリズムに組み込むことが可能と なる。提案手法の論理的整合性を検証するために，手法をモデル理論的に定式化し， その理論的性質を明らかにした。また，SNLI コーパスを用いて推論実験を行い，本手法による推論過程の明示可能性を検証した。

キーワード：自然言語推論, 含意関係認識, 依存構造, 形式論理, タブロー法, ニューラル ネットワーク，SNLI コーパス
## Natural Language Inference Using Neural Network and Tableau Method

Ayahito Saji ${ }^{\dagger, \dagger \dagger}$, Daiki TakaO ${ }^{\dagger}$, Yoshihide Kato $^{\dagger \dagger \dagger}$ and Shigeki Matsubara ${ }^{\dagger, \dagger \dagger \dagger}$

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.

Key Words: Natural Language Inference, Recognizing Textual Entailment, Dependency Structure, Formal Logic, Tableau Method, Neural Network, SNLI corpus

## 1 はじめに

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

近年, ニューラルモデルに基づくアプローチ (Parikh et al. 2016; Chen et al. 2017; Devlin et al. 2019; Lan et al. 2019; Tai et al. 2020; Wang et al. 2021) が提案され, SNLI コーパス (Bowman et al. 2015), MultiNLI (MNLI) コーパス (Williams et al. 2018), Adversarial NLI (ANLI) デー タセット (Nie et al. 2020), QNLI データセット (Wang et al. 2018)などの NLI データセットを用いた実験で高い正答率を達成している。 しかし, このアプローチに基づく NLI は, 判定結果に至る過程や理由を説明する能力を有していないという問題がある。ニューラルモデルの内部はブラックボックスであり，どのような推論を経て判定に至ったのかを人間が推察することは容易ではない1。このような問題に対して, 近年, 機械学習モデルの判定の過程を明らかにするための技術，いわゆる説明可能な AI (XAI) (Barredo Arrieta et al. 2020)の研究が進められており, 自然言語処理の分野においても同様の問題意識を共有している (Danilevsky et al. 2020). また, ニューラルモデルによる推論の正当性についても問題が指摘されている. 例えば, Yanaka ら (Yanaka et al. 2020)は，ニューラルモデルが自然言語における推論の体系性を学習するかについて monotonicity の観点から評価する手法を提案し, 現状のニューラルモデルの汎化性能には限界があることを示している。 また, Gururangan ら (Gururangan et al. 2018) や Tsuchiya
^{1}$ Kumar ら (Kumar and Talukdar 2020) は説明文を生成する NLI システムを提案している。しかし，説明文はニューラルモデルにより生成されるため, 説明文の生成過程はブラックボックス化しており，内部の処理を知ることは困難であるといえる。
}

(Tsuchiya 2018)は, SNLI コーパスや MNLI コーパスなどの NLI データセットには, 本来 $2 \supset$ のテキストに対して定まるはずの推論的関係が，一方のテキストのみから推測できてしまうバイアスがあることを示し, ニューラルモデルが単にバイアスに基づいて推論的関係を同定しているという危険性を指摘している.

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

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

本論文の構成は以下の通りである。まず 2 章で，提案手法のベースとなるタブロー法について概説する． 3 章では，夕ブロー法とニューラル NLI モデルを組み合わせた推論手法を提案する. 続く 4 章では, 提案手法の意味論をモデル理論的に定式化し, 手法の理論的性質を明らか


にする， 5 章では, SLNI コーパスを用いて, 提案手法の推論能力を定量的及び定性的に評価する. 6 章では, 関連研究を整理し, 提案手法との違いを示す.

## 2 タブロー法

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

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

タブローは木構造であり分岐する。分岐は場合分けに相当する．タブローの根から葉への経路を枝と呼び，ある枝の上に $(f, \mathrm{~T}, 0)$, および $(f, \mathrm{~F}, 0)$ （ $f$ は論理式）というエントリが存在するとき，その枝は閉じているという，タブローのすべての枝が閉じているとき，そのタブロー は閉じているという．閉じているタブローを閉鎖タブローと呼ぶ．タブローが閉じていること


（a）命題論理におけるタブローの例

図 1 命題論理に対するタブロー推論の例

によって, 最初に与えられた論理式と真偽値の対の集合のような真偽値割り当てが存在しないことが証明される。

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

## 3 提案手法

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

依存構造解析前提文 $p$ と仮説文 $h$ に依存構造を付与する。依存構造が付与された文をそれぞれ $D_{p}, D_{h}$ とする.

タブローの構成前提 $D_{p}$ と仮説 $D_{h}$ をもと，含意関係を証明するタブロー（集合 $\left.\{\left(D_{p}, \mathrm{~T}\right)\right.$,
$\left.\left(D_{h}, \mathrm{~F}\right)\right.\}$ から導出される完成したタブロー）と矛盾関係を証明するタブロー（集合 $\left.\{\left(D_{p}, \mathrm{~T}\right)\right.$, $\left.\left(D_{h}, \mathrm{~T}\right)\right.\}$ から導出される完成したタブロー) を構築する。以下では, これらのタブロー をそれぞれ含意タブロー，矛盾タブローと呼ぶ.

タブローの閉鎖性判定含意タブロー，および矛盾タブローが閉じているか否かをニューラル NLI モデルを用いて判定する.

推論的関係の同定含意タブローと矛盾タブローの閉鎖性の判定から，推論的関係を同定する.以下では，各処理について，その背景となる考え方と合わせて説明する.

## 3.1 依存構造解析

提案手法ではタブローが閉じているか否かの判定にニューラル NLI モデルを利用する。これにはニューラル NLI モデルへの入力は論理式ではなく自然言語文 2 文であることが課題となる. この課題を解決する，すなわち，自然言語文をモデルに入力するためのアプローチの一つとして，夕ブローのエントリは論理式とし，前提文と仮説文を論理式に変換して記号操作を行った後に，論理式を自然言語文へ再変換してニューラルモデルを利用する方法が考えられる。しかし，論理式からテキストへの変換は現状の技術では困難である ${ }^{4}$.そこで提案手法では，自然言語文を論理式に変換してタブロー法を適用するのではなく，タブロー法を自然言語文に適用できるように拡張するアプローチを取る。具体的には，依存構造を付与した自然言語文をタブロー のエントリに採用する。夕ブロー規則は，依存構造情報をもとに，新しいエントリを導出する。提案手法では, 依存構造として Universal Dependencies (UD) (de Marneffe et al. 2021)を採用する。提案手法の最初のステップは，前提と仮説の自然言語文に依存構造を与える処理であり， この処理には, UDに基づく任意の依存構造解析器を用いることができる. 図 2 に依存構造の例を示す.

図 2 "Either Smith or Anderson signed the contract." の依存構造解析結果


## 3.2 タブローの構成

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

提案手法におけるタブローのエントリは，四つ組 $(D, v, a, o)$ である。 $D$ は依存構造であり, $v$ と $a$ は通常のタブロー法と同様であり，それぞれ真偽値およびフラグである，oは，そのエントリがどのエントリから導出されたかを表す。初期タブローのエントリ $e$ は, 自分自身から導出されたものとする. すなわち $e=(D, v, 0, e)$ という形をとる. タブローは, 通常のタブロー 法と同じくタブロー規則を繰り返しエントリに適用することで導出される。提案手法におけるタブロー規則の一般形は, 次の表記で表される.

$
r=\left(c_{1,1} \wedge \cdots \wedge c_{1, n_{1}}\right) \vee \cdots \vee\left(c_{m, 1} \wedge \cdots \wedge c_{m, n_{m}}\right)
$

ここで， $c_{i, j}$ は, エントリ $(D, v, 0, o)$ を受け取り，エントリ $\left(D^{\prime}, v^{\prime}, 0, o\right)$ を返す任意の部分関数である． $r$ を構成するすべての $c_{i, j}$ について,$c_{i, j}(e)$ が未定義でないとき, タブロー規則 $r$ はエントリ $e$ に適用可能であるという，夕ブロー中に，夕ブロー規則が適用可能なエントリ $e$ が存在するとき, そのエントリが支配するすべての葉に, それらの子として新たな $m$ 個の経路 $\left.\langle c_{1,1}(e) \cdots c_{1, n_{1}}(e)\right.\rangle, \cdots,\left.\langle c_{m, 1}(e) \cdots c_{m, n_{m}}(e)\right.\rangle$ を追加する. タブロー規則が適用されたエントリ $(D, v, 0, o)$ を $(D, v, 1, o)$ に置き換える.

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

(a) 条件法に関する規則
(b) 否定に関する規則
(c) 選言に関する規則

図 3 タブロー規則の例
初期タブローを $e_{1}=\left(\right.$ Either Smith or Anderson signed the contract, T, $\left.0, e_{1}\right), e_{2}=($ If Smith did not sign the contract Anderson made an agreement, F, $\left.0, e_{2}\right)$ としたときのタブローの構成を例に，タブロー規則の適用の流れを説明する（完成したタブローを図 4 に示す)。 $e_{2}$ ：(If Smith did not sign the contract Anderson made an agreement, F $\left., 0, e_{2}\right)$ に図 3(a)の規則を適用すると， $e_{2}$ が支配するすべての葉に新たな 2 つのエントリ $e_{3}$ : (Smith did not sign the contract, $\mathrm{T}, 0, e_{2}$ ) と $e_{4}$ : (Anderson made an agreement, $\left.\mathrm{F}, 0, e_{2}\right)$ が追加され， $e_{2}$ のフラグが 1 に変更される. 次に， $e_{3}$ : (Smith did not sign the contract, $\mathrm{T}, 0, e_{2}$ )に図 3(b) の規則を適用すると，新たなエントリ $e_{5}$ ：(Smith signed the contract, $\left.\mathrm{F}, 0, e_{2}\right)$ が追加され， $e_{3}$ のフラグが 1 に変更される。最後に， $e_{1}$ : (Either Smith or Anderson signed the contract, T $\left., 0, e_{1}\right)$ に図 3(c) の規則を適用すると，新たな 2 つのエントリ $e_{6}$ : (Smith signed the contract, T, $0, e_{1}$ ) と $e_{7}$ : (Anderson singned the contract, $\left.\mathrm{T}, 0, e_{1}\right)$ が追加され， $e_{1}$ のフラグは 1 に変更される. 以上により, タブローが構成される.

$e_{1}$ : (Either Smith or Anderson signed the contract, T, 1, $e_{1}$ )

$e_{2}$ : (If Smith did not sign the contract Anderson made an agreement, F, 1, $e_{2}$ )

図 4 含意タブローの例

## 3.3 タブローの閉鎖性判定

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

提案手法では，枝上に次のいずれかが成り立つようなエントリ $e_{1}=\left(D_{s_{1}}, v_{1}, 0, o_{1}\right), e_{2}=$ $\left(D_{s_{2}}, v_{2}, 0, o_{2}\right)$ （ただし $o_{1} \neq o_{2} ）$ が存在するとき，その枝は閉じていると再定義する（閉じた夕ブローについてもこの再定義のもとで同様に再定義する).以下では再定義した 3 つの条件を,枝の閉鎖条件と呼ぶ.

(1) $v_{1}=\mathrm{T}$ かつ $v_{2}=\mathrm{F}$ かつ $s_{1}=s_{2}$

(2) $v_{1}=\mathrm{T}$ かつ $v_{2}=\mathrm{T}$ かつ $\nu\left(s_{1}, s_{2}\right)=\mathrm{C}$

(3) $v_{1}=\mathrm{T}$ かつ $v_{2}=\mathrm{F}$ かつ $\nu\left(s_{1}, s_{2}\right)=\mathrm{E}$

閉鎖条件 (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 システム $\nu$ のもとで閉じているということにする.

$o_{1} \neq o_{2}$ という条件は, 前提から導出されたエントリ同士, あるいは仮説から導出されたエントリ同士について，閉鎖性の判定の対象から除外するものである。これは前提や仮説が恒真 (偽) でなければ問題となることはない.

タブローの閉鎖性判定の例について見るために，図 4 のタブローを考える。また，

$
\nu\left(\operatorname{sen}\left(e_{7}\right), \operatorname{sen}\left(e_{4}\right)\right)=\mathrm{E}
$

であると仮定する 5 . このタブローは 2 つの枝をもつが, 左の枝 $\left.\langle e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{6}\right.\rangle$ では, $e_{6}$ : (Smith signed the contract, T, $0, e_{1}$ ), $e_{5}$ : (Smith signed the contract, F, $0, e_{2}$ ) が存在している. この枝は閉鎖条件 $(1)$ を満たすので，閉じている。一方，右の枝 $\left.\langle e_{1}, e_{2}, e_{3}, e_{4}, e_{5}, e_{7}\right.\rangle$ では, $e_{7}$ : (Anderson signed the contract, T, $0, e_{1}$ ), $e_{4}$ : (Anderson made an agreement, F, $0, e_{2}$ ) が存在している. $\nu\left(\operatorname{sen}\left(e_{7}\right), \operatorname{sen}\left(e_{4}\right)\right)=\mathrm{E}$ であるので，閉鎖条件 $(3)$ によってこの枝は閉じている. した
\left(\left(D_{s}, v, a, o\right)\right)=s$ と定義する.
}

表 1 タブローの閉鎖性と推論的関係の対応

がって, 図4のタブローは, 仮定のような NLI システムの下で閉じている.

## 3.4 推論的関係の同定

含意タブロー，および矛盾タブローは，それぞれ前提と仮説の間に含意関係，矛盾関係が成り立つかどうかを判定するためのタブローである。これらのタブローの閉鎖性と，仮説と前提の間の推論的関係は, Abzianidze (Abzianidze 2015) と同様に表 1 のように整理でき,これに従って推論的関係を同定する ${ }^{6}$.

## 4 提案手法の意味論

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

## 4.1 モデル

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

まず，モデルを定義する.

定義 1 (モデル). $L$ ( $L$ は自然言語文の集合）から $\{\mathrm{T}, \mathrm{F}\}$ の関数 $m$ をモデルと呼ぶ. $\mathcal{M}$ をべてのモデルの集合とする. モデルの集合 $M \subseteq \mathcal{M}$ に対して, $M(s)=\{m \in M \mid m(s)=\mathrm{T}\}$ と定義する。


 &  \\

表 2 提案手法の定式化に使用する記号

以下では，モデル集合 $M$ が与えられたとき7， $M$ と整合性のとれた NLI システム，および夕ブロー規則がどのようなものであるかを定義し, 整合性が取れているという条件の下で提案手法による推論的関係の同定の理論的限界を明らかにする.

定義 2. 次の 3 つの条件が全て成り立つとき, NLI システム $\nu$ はモデル集合 $M$ と整合的であるという。なお, $s_{1}, s_{2} \in L$ とする.
- $M\left(s_{1}\right) \subseteq M\left(s_{2}\right)$ ならば, かつ, そのときのみ $\nu\left(s_{1}, s_{2}\right)=\mathrm{E}$
- $\neg\left(M\left(s_{1}\right) \subseteq M\left(s_{2}\right)\right) \wedge \neg\left(M\left(s_{1}\right) \cap M\left(s_{2}\right)=\emptyset\right)$ ならば, かつ, そのときのみ $\nu\left(s_{1}, s_{2}\right)=\mathrm{N}$
- $M\left(s_{1}\right) \cap M\left(s_{2}\right)=\emptyset$ ならば，かつ，そのときのみ $\nu\left(s_{1}, s_{2}\right)=\mathrm{C}$

この定義では，含意関係をモデル集合の包含関係として，矛盾関係を互いに素な関係として捉えている.

以下では，モデルに基づいてタブローを特徴付ける。その準備として，エントリ，タブロー の枝, タブローに対応するモデルを， $M(s)$ を拡張することにより定義する.
$ ではなく, その部分集合 $M$ を考えるのは， $\mathcal{M}$ の中には，論理的に不自然なモデル，例えば，すべての自然言語文に対して T を返すようなモデルが含まれるからである。論理的に自然なモデルの集合が仮に $M$ として与えられたものとして以下では議論を進める。なお， $M$ に対して何の条件も課さないため， $M$ がどのような集合であっても以下の議論は成り立つ.
}
定義 3 (エントリに対するモデル集合). タブローのエントリ $e=\left(D_{s}, v, a, o\right)$ に対して, $M(e)$ を次のように定義する.

$
M(e)= \begin{cases}M(s) & (v=\mathrm{T}) \\ M-M(s) & (v=\mathrm{F})\end{cases}
$

定義 4 (タブローの枝に対するモデル集合). タブローの枝 $b$ に対して,$M(b)$ を次のように定義する.

$
M(b)=\bigcap_{e \in b} M(e)
$

定義 $\mathbf{5}$ (タブローに対するモデル集合). タブロー $t$ に含まれる全ての枝の集合を $B$ とする. $M(t)$ を次のように定義する。

$
M(t)=\bigcup_{b \in B} M(b)
$

提案手法では，タブロー規則の適用前後で，エントリが表現する制約が等価であることを想定しており，この性質を以下のように定義する.

定義 6. $r=\left(c_{1,1} \wedge \cdots \wedge c_{1, n_{1}}\right) \vee \cdots \vee\left(c_{m, 1} \wedge \cdots \wedge c_{m, n_{m}}\right), E$ をすべてのエントリの集合とし, $E_{r}=\{e \in E \mid r$ は $e$ に適用可能 $\}$ とする. 任意の $e \in E_{r}$ に対して次の条件が満たされるとき, タブロー規則 $r$ はモデル集合 $M$ と整合的であるという.

$
M(e)=\left(M\left(c_{1,1}(e)\right) \cap \cdots \cap M\left(c_{1, n_{1}}(e)\right)\right) \cup \cdots \cup\left(M\left(c_{m, 1}(e)\right) \cap \cdots \cap M\left(c_{m, n_{m}}(e)\right)\right)
$

この等式において, 左辺は, エントリ $e$ に対する制約に相当する。右辺は, エントリ $e$ にタブロー規則 $r$ を適用した結果，導出されるエントリにより表現される制約に対応する。また，任意の $r \in R$ が $M$ と整合的であるとき， $R$ は $M$ と整合的であるという.

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

## 4.2 健全性と完全性

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

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

定義 8 (含意タブロー, および矛盾タブローの完全性). $M$ をモデル集合, $(R, \nu)$ を $M$ と整合的な証明システムとする。任意の前提文 $p$ と仮説文 $h$ について, 次の条件が成り立つならば, $(R, \nu)$ は，モデル集合 $M$ において完全であるという.
- $M(p) \subseteq M(h)$ ならば, $R$ によって構成された含意タブローが $\nu$ のもとで閉じている.

## 4.2.1 健全性の証明

本節では，健全性に関する以下の定理を証明する。

定理 1 (健全性の定理)． $M$ をモデル集合とする． $M$ と整合的な任意の証明システムは， $M$ において健全である。

以下では，まず定理 1 を証明するための補助定理を導入し，それにも基づき定理 1 を証明する.

補助定理 2. $R$ が $M$ と整合的であるならば， $t \stackrel{R}{\triangleright} t^{\prime}$ を満たす任意のタブロー $t$ と $t^{\prime}$ において次が成立する.

$
M(t)=M\left(t^{\prime}\right)
$

補助定理 2 は定義 6 から明らかである.

補助定理 3. $t$ と $t^{\prime}$ をタブローとし, $t \triangleright^{R} t^{\prime}$ とする， $R$ が $M$ と整合的であるならば, $M(t)=M\left(t^{\prime}\right)$.補助定理 3 は補助定理 2 から明らかである.

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

証明. $R$ によって構成された含意タブロー $t_{\mathrm{comp}}$ が $\nu$ のとで閉じているとする.このとき, $t_{\text {comp }}$ のすべての枝 $b$ に閉鎖条件のいずれかを満たす 2 つのエントリ $e_{1}=\left(D_{s_{1}}, v_{1}, 0, o_{1}\right), e_{2}=$ $\left(D_{s_{2}}, v_{2}, 0, o_{2}\right)$ （ただし $\left.o_{1} \neq o_{2}\right)$ が存在する.
- 閉鎖条件 (1) を満たすならば, $s_{1}=s_{2}$. したがって, 定義 3 より $M\left(e_{1}\right) \cap M\left(e_{2}\right)=$ $M\left(\left(D_{s_{1}}, \mathrm{~T}, 0, o_{1}\right)\right) \cap M\left(\left(D_{s_{2}}, \mathrm{~F}, 0, o_{2}\right)\right)=\emptyset$.
- 閉鎖条件 $(2)$ を満たすならば, $\nu\left(s_{1}, s_{2}\right)=$ C. $\nu$ は $M$ と整合的であるから, 定義 2 より $M\left(s_{1}\right) \cap M\left(s_{2}\right)=\emptyset$. よって, 定義 3 より $M\left(s_{1}\right) \cap M\left(s_{2}\right)=M\left(\left(D_{s_{1}}, \mathrm{~T}, 0, o_{1}\right)\right) \cap$ $M\left(\left(D_{s_{2}}, \mathrm{~T}, 0, o_{2}\right)\right)=M\left(e_{1}\right) \cap M\left(e_{2}\right)=\emptyset$.
- 閉鎖条件 $(3)$ を満たすならば, $\nu\left(s_{1}, s_{2}\right)=\mathrm{E} . \nu$ は $M$ と整合的であるから，定義 2 より $M\left(s_{1}\right) \subseteq M\left(s_{2}\right)$. 定義 3 より $M\left(e_{1}\right)=M\left(s_{1}\right), M\left(e_{2}\right)=M-M\left(s_{1}\right)$. ここで $M\left(s_{1}\right) \subseteq$ $M\left(s_{2}\right)$ であるから, $M\left(e_{1}\right) \cap M\left(e_{2}\right)=\emptyset$.

以上より, $M\left(e_{1}\right) \cap M\left(e_{2}\right)=\emptyset$. ゆえに, 定義 4 より $M(b)=\emptyset$ となる. したがって，すべての

$e_{1}=\left(D_{p}, \mathrm{~T}, 0, e_{1}\right), e_{2}=\left(D_{h}, \mathrm{~F}, 0, e_{2}\right)$ から構成されるため, 定義 4 と 5 から $M\left(\left(D_{p}, \mathrm{~T}, 0, e_{1}\right)\right) \cap$ $M\left(\left(D_{h}, \mathrm{~F}, 0, e_{2}\right)\right)=\emptyset$ である. したがって, $M\left(\left(D_{p}, \mathrm{~T}, 0, e_{1}\right)\right) \subseteq M\left(\left(D_{h}, \mathrm{~T}, 0, e_{2}\right)\right)$. 定義 3 から $M(p) \subseteq M(h)$ である．以上より定義 7 の 1 番目の条件は満たされる。矛盾タブローに関する 2 番目の条件も同様に証明できる。すなわち, 証明システム $(R, \nu)$ は $M$ において健全である.

## 4.2.2 完全性の反例

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

完全性が一般に成り立たないことを示すには，次の条件を満たすモデル集合 $M$ ，証明システ厶 $(R, \nu)$, 前提文 $p$, 仮説文 $h$ が存在することを示せげ十分である.

## 条件 $1 M(p) \subseteq M(h)$

条件 $2(R, \nu)$ は $M$ と整合的である.

条件 $3 R$ によって構成された $p$ と $h$ の含意タブローは $\nu$ のとで閉じていない.

次のインスタンス, 表 3 に示すモデル $M$, 図 5 に示すタブローを構成する証明システム $(R, \nu)$ （ $\nu$ は $M$ と整合的なものを任意に選んでよい）は，上の条件を満たす，完全性が一般には成り立たないことを示す反例となっている.

前提: Smith and Anderson did not go out.

仮説: Smith and Anderson were home.

推論的関係: 含意

$M(p)=M(h)=\left.\{m_{1}\right.\}$ であるので, $M(p) \subseteq M(h)$ である. すなわち条件 1 を満たす. $M\left(e_{1}\right)=$

表 3 完全性が成立しないモデルの例

$e_{1}$ : (Smith and Anderson did not go out, T, 1, $e_{1}$ )

$e_{2}$ : (Smith and Anderson were home, $\mathrm{F}, 1, e_{2}$ )

$e_{3}$ : (Smith or Anderson went out, F, 1, $e_{1}$ )

図 5 タブローの完全性の反例

$M\left(e_{3}\right)=M\left(e_{4}\right) \cap M\left(e_{5}\right)=\left.\{m_{1}\right.\}, M\left(e_{2}\right)=M\left(e_{6}\right) \cup M\left(e_{7}\right)=\left.\{m_{2}, m_{3}, m_{4}\right.\}$ であることから, このタブローの構成に用いられたタブロー規則は $M$ と整合的である。 $\nu$ はと整合的であるので， $(R, \nu)$ は $M$ と整合的である。 すなわち条件 2 を満たす. 図 5 の含意タブローにおいてタブ

このため, この含意タブローにおいて，閉鎖条件を満たすエントリの対は存在せず， $\nu$ のもとでこのタブローが閉じていることはあり得ない。（条件 3 を満たす)。以上から， $M,(R, \nu), p, h$ は完全性が一般には成り立たないことを示す反例となっている.

## 5 実験

提案手法における論理的な推論過程の明示可能性を評価すること, 及び, 提案手法の欠点を
明らかにすることを目的に，下記の準備のもと実験を実施した8 8.

データセットニューラル NLI モデルの構築, および評価用データセットとして SNLIコーパスを使用した．SNLIコーパスには，訓練データとして 549,367 件，開発データとして 9,842 件，テストデータとして 9,824 件が含まれている 9.

依存構造解析依存構造解析器として Udify (Kondratyuk and Straka 2019), および Udify 事前学習モデルを用いた ${ }^{10}$. Udify は Multilingual BERT ${ }^{11}$ ベースの多言語対応の依存構造解析器であり，UDに基づく依存構造を出力する.

ニューラル NLI モデルフレームワーク内で使用するニューラル NLI モデルとして，LSTM に基づくニューラル NLI モデルである ESIM (Chen et al. 2017) を採用した ${ }^{12}$. ESIM のパラメータは，SNLIコーパスの訓練用データと開発用データを用いて学習した。

タブロー規則タブロー規則として，命題論理のタブロー法の連言，選言，否定，条件法の 4 つの規則に相当する規則を合計 32 個作成した。作成したタブロー規則について付録 Aにまとめる。連言，選言については，文の等位接続だけでなく，UDの core argument（主語，目的語など）の等位接続を扱える規則となっている.

## 5.1 推論過程の明示可能性

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

実験デー夕内のあるインスタンスを対象に，提案手法による推論がどのように行われたのかを分析した。

前提: A little boy is standing in front of a wedding party laughing.

仮説: There is a bride and groom behind the little boy.

推論的関係: 含意

図 7 に，このインスタンスに対して作成された含意タブローを示す。この例では， $e_{2}$ に含まれる等位構造 “a bride and groom” が “groom” と “bride”に分解され，それぞれ $e_{3}$ と $e_{4}$ として導


図 6 含意タブロー（左）と矛盾タブロー（右）のサイズの分布

$e_{1}$ : (A little boy is standing in front of a wedding party laughing, $\mathrm{T}, 0, e_{1}$ )

$e_{2}$ : (There is a bride and groom behind the little boy, $\mathrm{F}, 1, e_{2}$ )

$e_{3}$ : (There is a bride behind the little boy, $\mathrm{F}, 0, e_{2}$ )

$e_{4}$ : (There is a groom behind the little boy, $\mathrm{F}, 0, e_{2}$ )

図 7 正しい含意タブローの例

出された後，それらが $e_{1}$ と矛盾することを正しく判定できている。 すなわち，タブロー法に基づいて名詞句の等位構造により表現された連言を分解する推論過程を明示化できている。一方で, 記号操作的アプローチでは扱いが難しい "wedding party" と "groom", "bride"といった単語の類似関係や “in front of" と “behind” といった異なる単語（列）によって表現された位置の関係は, ニューラルモデルにより柔軟に扱うことができている.

## 5.2 誤り分析

タブロー法とニューラル NLI モデルを組み合わせる提案手法の問題点を明らかにするために,提案手法において何らかのタブロー規則が適用された 800 件を対象に，その推論性能を測定した. 提案手法による結果, 及び，ニューラル NLI モデルによる結果を表 4 , および表 5 に併せて示す。なお,「エラー」とは， 3.4 節の表 1 に示したように，含意関係と矛盾関係のいずれも成立すると判定され，解釈不能であることを示すラベルである．推論性能として，標準的な評価指標である正解率, 再現率, 精度, $F_{1}$ 値を求めた ${ }^{13} . F_{1}$ 値は, 以下で定義する再現率と精度の調和平均である.

$
\begin{aligned}
\text { Recall }_{A} & =\frac{\mathrm{TP}_{A}}{\operatorname{True}_{A}} \\
\text { Precision }_{A} & =\frac{\mathrm{TP}_{A}}{\text { Positive }_{A}}
\end{aligned}
$

ここで， $A$ は「含意」，「中立」，「矛盾」のいずれかのラベルを表し， $\mathrm{TP}_{A}$ は正解ラベルと予測ラベルがクラス $A$ であるインスタンス数, True $A$ は正解ラベルがクラス $A$ であるインスタンス数, Positive ${ }_{A}$ は予測ラベルがクラス $A$ であるインスタンス数である. 提案手法は, ニューラル NLI モデルと比べて, 正解率の低下がみられた.

以下では，提案手法において夕ブロー規則が適用され，かつ誤りが生じたケースについて，そ

の要因を分析し，考察する.

表 4 提案手法とニューラル NLI モデルの予測結果

表 5 提案手法とニューラル NLI モデルの正解率


## 5.2.1 誤りの原因の分析

本節では，開発データ中においてタブロー規則が適用された 762 件のインスタンスを用いて提案手法が推論的関係を誤って同定した原因を分析する。開発データに対して提案手法を適用した予測結果の混合行列を表 6 に示す. 開発データの結果はテストデータと大きな乘離がなく，誤りの原因についても同様の傾向が見られた。誤って予測したインスタンスの合計は 268 件であった. この 268 件の中で, 正解ラベルが誤っていたインスタンスは 35 件存在した. 正解ラベルを修正したところ，そのうち 16 件は提案手法によって正しく推論的関係を同定できていた. また, 文中の単語の誤りによって意味が通らないインスタンスが 4 件存在した. そこで, 以上の 20 件を除いた 248 件のインスタンスについて, その閉鎖性判定が誤っているタブロー 292 個 ${ }^{14}$ を, 次の 4 つに分類した ${ }^{15}$.
- NLI システムに起因する誤り（5.2.2 節）

$\cdot$ タブロー規則に起因する誤り (5.2.3 節)
- 依存構造解析に起因する誤り (5.2.4 節)
- 提案手法の限界に起因する誤り (5.2.5 節)

それぞれに該当するタブローの数を表 7 に示す.

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

表 6 開発デー夕に対する提案手法の予測結果

表 7 開発デー夕における誤りの要因


## 5.2.2 NLI システムに起因する誤り

本節では, NLI システムに起因する誤りについて説明する。 292 個の誤りのうち, 239 個の誤りは，NLI システムが推論的関係の同定を誤ったことが原因である．例として，以下のインスタンス

前提: Two people are in a green forest.

仮説: The forest is not dead.

推論的関係: 含意

に対して生成された含意タブローを図 8 に示す.このインスタンスの推論的関係は「含意」であるため，含意夕ブローは閉じなければならないが，閉じていなかった. $\operatorname{sen}\left(e_{1}\right)$ における "green forest" $\operatorname{sen}\left(e_{3}\right)=$ "The forest is dead" から, 正しくは $\nu\left(\operatorname{sen}\left(e_{1}\right), \operatorname{sen}\left(e_{3}\right)\right)=$ Cであると考えられるが, $\nu\left(\operatorname{sen}\left(e_{1}\right), \operatorname{sen}\left(e_{3}\right)\right)=\mathrm{N}$ と判定されたために，閉鎖条件 $(2)$ を満たさず，このタブロー は閉じていない.

また，NLI システムの推論的関係の同定の誤り 239 個のうち, SNLI コーパスから学習したニューラルモデルがもつある特性が原因であると考えられるものが 141 個存在した. 例として,以下のインスタンス

前提: A man and woman walk atop a hill.

仮説: A man and woman are walking.

推論的関係: 含意

に対して生成された矛盾タブローを図 9 に示す.

推論的関係は「含意」であるこのタブローのエントリ $e_{3}$ と $e_{6}$ について, $\nu\left(\operatorname{sen}\left(e_{3}\right), \operatorname{sen}\left(e_{6}\right)\right)=\mathrm{C}$ と判定された。 そのため, $\nu$ のもとでこの矛盾タブローは閉じてしまい, 正しい推論的関係を

$e_{1}$ : (Two people are in a green forest, $\mathrm{T}, 0, e_{1}$ )

図 8 NLI システムに起因して誤った含意タブローの例

$e_{1}$ : (A man and woman walk atop a hill, T, $1, e_{1}$ )

$e_{3}$ : (A man walk atop a hill, $\mathrm{T}, 0, e_{1}$ )

$e_{4}$ : (Woman walk atop a hill, $\mathrm{T}, 0, e_{1}$ )

$e_{6}$ : (Woman are walking, $\mathrm{T}, 0, e_{2}$ )

$e_{3}$ と $e_{6}$ より誤って $\mathbf{x}$

図 9 NLI システムに起因して誤った矛盾タブローの例

同定できなかった.

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

## 5.2.3 タブロー規則に起因する誤り

本節では，夕ブロー規則の適用に起因する誤りについて説明する。夕ブロー規則を適用することにより不適格文が生成されるケースが確認された。例えば，次のようなインスタンスが存在した。

前提: The man and woman are both smiling.

仮説: A guy and a lady are standing near each other.

推論的関係: 中立

この仮説文に対してタブロー規則を適用した結果を図 10 に示す.ここで， $e_{1}$ に含まれる “each other”は, “a guy”が “a lady”を, “a lady”が “a guy”を先行詞とする相互代名詞であるものの, タブロー規則を適用した結果得られる $e_{2}$ と $e_{3}$ では先行詞が存在しなくなるため, 不適格文となる。タブロー規則を適用した結果, 不適格文が生成されたタブローは 19 個存在した.

別の誤りの要因としては， not + any を含む文に対して否定に関するタブロー規則を適用することによるものが挙げられる。例えば,

前提: A cement truck pours cement on the street.

仮説: The truck isn't doing anything.

## 推論的関係: 矛盾

の仮説文に否定に関するタブロー規則を適用すると，図 11 のようになる. $e_{1}$ と $e_{2}$ は等価な制約を表していない． $e_{2}$ における“anything”を“something”に置き換えれば等価な制約を表せるものの, 現状のタブロー規則では not を単純に取り除くことしかできない. このような原因により誤りが生じたタブローは 17 個存在した.

$e_{2}$ : (A guy are standing near each other, $\mathrm{T}, 0, o$ )

図 10 タブロー規則の適用により意味的に不適格な文が生成される例

$e_{1}$ : (The truck is n't doing anything, $\mathrm{T}, 1, o$ )

図 11 not + any を含むエントリに対するタブロー規則の適用の例

$e_{1}$ : (A little boy is playing hide and seek in the woods, $\mathrm{T}, 1, o$ )

$e_{2}$ : (A little boy is playing hide in the woods, $\mathrm{T}, 0, o$ )

$e_{3}$ : (A little boy is playing seek in the woods, $\mathrm{T}, 0, o$ )

図 12 非合成的な要素を含むエントリの誤った分解

他の誤りの要因として, 非合成的な要素（イディオム, 固有名詞など）をタブロー規則が分解してしまうことが挙げられる，以下のインスタンスでは，図 12 のように，仮説文に含まれる “hide and seek”というイディオムが分解されたために, 意味的に不適格な文が生成されている.

前提: A small child is sitting on a stump in a forest clearing.

仮説: A little boy is playing hide and seek in the woods.

推論的関係: 矛盾

このようなタブローは 2 個存在した.

## 5.2.4 依存構造解析に起因する誤り

前提文，または仮説文の依存構造解析に誤っているタブローは 53 個存在した。このうち，夕ブロー規則がマッチする部分における解析誤りによって，意味的に不適格な文が生成された夕

ブローは 3 個存在した。例えば，次のインスタンス

前提: A male and a female with a black hat, and sunglasses stop and talk.

仮説: Man and woman stop and chat with each other.

推論的関係: 含意

の前提文は, 正しくは図 13 のような依存構造を持つが，依存構造解析の誤りによって図 14 のように分解されてしまい，意味的に不適格な文 “Sunglasses stop and talk.” が生成されている.残りのタブロー 50 個における依存構造解析誤りの影響はみられなかった.

A male and a female with a black hat, and sunglasses stop and talk

図 13 "A male and a female with a black hat, and sunglasses stop and talk." の正しい依存構造

$e_{1}$ : (A male and a female with a black hat, and sunglasses stop and talk, $\mathrm{T}, 1, o$ )

$e_{2}:($ A male stop and talk, $\mathrm{T}, 0, o)$

$e_{3}$ : (A female with a black hat stop and talk, $\mathrm{T}, 0, o$ )

図 14 依存構造解析の誤りによる意味的に不適格な文の生成

$e_{1}$ : (Two men and one woman are performing music on a stage, T, $1, e_{1}$ )

$e_{2}$ : (Three musicians are performing at a concert, $\mathrm{F}, 0, e_{2}$ )

図 15 提案手法の限界に起因する誤った含意タブローの例

## 5.2.5 提案手法の限界に起因する誤り

NLI システム, タブロー規則の適用, 依存構造解析のいずれにも誤りがないにもかかわらず,推論的関係の同定を誤ったものは, 提案手法の限界, すなわち完全性が一般には成り立たないことに起因するものと位置づけられる。例として，以下のインスタンス

前提: Two men and one woman are performing music on a stage.

仮説: Three musicians are performing at a concert.

推論的関係: 含意

に対して生成された含意タブローを図 15 に示す.このタブローでは, 正しく依存構造解析が行われており, $e_{1}$ は $e_{3}$ おび $e_{4}$ に分解されているが，夕ブロー規則の適用に誤りはない. また, $\nu\left(\operatorname{sen}\left(e_{3}\right), \operatorname{sen}\left(e_{2}\right)\right)=\mathrm{N}, \quad \nu\left(\operatorname{sen}\left(e_{4}\right), \operatorname{sen}\left(e_{2}\right)\right)=\mathrm{N}$ であり, NLI モデルも正しい. 前提と仮説の間の推論的関係は「含意」であり, このタブローは閉じられる必要があるが, 閉じていない.これは,この提案手法の完全性が一般には成立しないことによるものと位置づけられる。このように，実際のデータセット中でも，完全性が一般に成立しないために推論的関係を正しく同定できなかったインスタンスが存在することがわかった.

## 6 関連研究

提案手法は, 構文構造を用いて推論を行う自然論理 (Natural Logic) (Lakoff 1970)のアイデア

に基づく手法と位置付けられる。本章では，自然論理に基づく従来の NLI 手法と提案手法を定性的に比較する。

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

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

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

## 7 おわりに

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

## 謝 辞

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

## 参考文献

Abzianidze, L. (2015). "A Tableau Prover for Natural Logic and Language." In Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pp. 2492-2502, Lisbon, Portugal. Association for Computational Linguistics.

Abzianidze, L. (2017). "LangPro: Natural Language Theorem Prover." In Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing: System Demonstrations, pp. 115-120, Copenhagen, Denmark. Association for Computational Linguistics.

Bar-Haim, R., Dagan, I., Greental, I., and Shnarch, E. (2007). "Semantic Inference at the LexicalSyntactic Level." In Proceedings of the 22nd AAAI Conference on Artificial Intelligence, pp. 871-876.

Barredo Arrieta, A., Díaz-Rodríguez, N., Del Ser, J., Bennetot, A., Tabik, S., Barbado, A., Garcia, S., Gil-Lopez, S., Molina, D., Benjamins, R., Chatila, R., and Herrera, F. (2020). "Explainable Artificial Intelligence (XAI): Concepts, Taxonomies, Opportunities and Challenges Toward Responsible AI." Information Fusion, 58, pp. 82-115.

Bowman, S. R., Angeli, G., Potts, C., and Manning, C. D. (2015). "A Large Annotated Corpus for Learning Natural Language Inference." In Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pp. 632-642, Lisbon, Portugal. Association for Computational Linguistics.

Chen, Q., Zhu, X., Ling, Z.-H., Wei, S., Jiang, H., and Inkpen, D. (2017). "Enhanced LSTM for Natural Language Inference." In Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 1657-1668, Vancouver, Canada. Association for Computational Linguistics.

Cooper, R., Crouch, D., Eijck, J. V., Fox, C., Genabith, J. V., Jaspars, J., Kamp, H., Milward, D., Pinkal, M., Poesio, M., Pulman, S., Briscoe, T., Maier, H., and Konrad, K. (1996). "Using the Framework." Tech. rep., FraCaS: A Framework for Computational Semantics. FraCaS deliverable D16.

Dagan, I., Roth, D., Sammons, M., and Zanzotto, F. M. (2013). Recognizing Textual Entailment: Models and Applications. Synthesis Lectures on Human Language Technologies. Morgan \& Claypool Publishers.

Danilevsky, M., Qian, K., Aharonov, R., Katsis, Y., Kawas, B., and Sen, P. (2020). "A Survey of the State of Explainable AI for Natural Language Processing." In Proceedings of the 1 st Conference of the Asia-Pacific Chapter of the Association for Computational Linguistics and the 10th International Joint Conference on Natural Language Processing, pp. 447-459, Suzhou, China. Association for Computational Linguistics.

de Marneffe, M.-C., Manning, C. D., Nivre, J., and Zeman, D. (2021). "Universal Dependencies." Computational Linguistics, 47 (2), pp. 255-308.

Devlin, J., Chang, M.-W., Lee, K., and Toutanova, K. (2019). "BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding." In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Short Papers), pp. 4171-4186, Minneapolis, Minnesota. Association for Computational Linguistics.

Gururangan, S., Swayamdipta, S., Levy, O., Schwartz, R., Bowman, S., and Smith, N. A. (2018). "Annotation Artifacts in Natural Language Inference Data." In Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 2 (Short Papers), pp. 107-112, New Orleans, Louisiana. Association for Computational Linguistics.

Hochreiter, S. and Schmidhuber, J. (1997). "Long Short-Term Memory." Neural Computation, 9 (8), pp. 1735-1780.

Hu, H., Chen, Q., Richardson, K., Mukherjee, A., Moss, L. S., and Kuebler, S. (2020). "MonaLog: a Lightweight System for Natural Language Inference Based on Monotonicity." In Proceedings of the Society for Computation in Linguistics 2020, pp. 334-344, New York, New York. Association for Computational Linguistics.

Kondratyuk, D. and Straka, M. (2019). "75 Languages, 1 Model: Parsing Universal Dependencies Universally." In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing, pp. 2779-2795, Hong Kong, China. Association for Computational Linguistics.

Kumar, S. and Talukdar, P. (2020). "NILE : Natural Language Inference with Faithful Natural Language Explanations." In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pp. 8730-8742, Online. Association for Computational Linguistics.

Lakoff, G. (1970). "Linguistics and Natural Logic." Synthese, 22 (1), pp. 151-271.

Lan, Z., Chen, M., Goodman, S., Gimpel, K., Sharma, P., and Soricut, R. (2019). "ALBERT: A Lite BERT for Self-supervised Learning of Language Representations." CoRR,
abs/1909.11942.

MacCartney, B. and Manning, C. D. (2007). "Natural Logic for Textual Inference." In Proceedings of the ACL-PASCAL Workshop on Textual Entailment and Paraphrasing, pp. 193-200, Prague. Association for Computational Linguistics.

MacCartney, B. and Manning, C. D. (2008). "Modeling Semantic Containment and Exclusion in Natural Language Inference." In Proceedings of the 22nd International Conference on Computational Linguistics, pp. 521-528, Manchester, UK. Coling 2008 Organizing Committee.

MacCartney, B. and Manning, C. D. (2009). "An Extended Model of Natural Logic." In Proceedings of the 9th International Conference on Computational Semantics, pp. 140-156, Tilburg, The Netherlands. Association for Computational Linguistics.

馬目華奈, 谷中瞳, 吉川将司, 峯島宏次, 戸次大介 (2018). RNN 系列変換モデルを用いた高階論理式からの文生成. 言語処理学会第 24 回年次大会発表論文集, pp. 380-383. [K. Manome et al. (2018). RNN Henkan Keiretsu Moderu wo Mochiita Kokaironrishiki karano Bunseisei. The 24th Annual Meeting of the Association for Natural Language Processing, pp. 380-383.].

Marelli, M., Menini, S., Baroni, M., Bentivogli, L., Bernardi, R., and Zamparelli, R. (2014). "A SICK Cure for the Evaluation of Compositional Distributional Semantic Models." In Proceedings of the 9th International Conference on Language Resources and Evaluation, pp. 216-223, Reykjavik, Iceland. European Language Resources Association.

Mineshima, K., Martínez-Gómez, P., Miyao, Y., and Bekki, D. (2015). "Higher-order Logical Inference with Compositional Semantics." In Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pp. 2055-2061, Lisbon, Portugal. Association for Computational Linguistics.

Nie, Y., Williams, A., Dinan, E., Bansal, M., Weston, J., and Kiela, D. (2020). "Adversarial NLI: A New Benchmark for Natural Language Understanding." In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pp. 4885-4901, Online. Association for Computational Linguistics.

Parikh, A., Täckström, O., Das, D., and Uszkoreit, J. (2016). "A Decomposable Attention Model for Natural Language Inference." In Proceedings of the 2016 Conference on Empirical Methods in Natural Language Processing, pp. 2249-2255, Austin, Texas. Association for Computational Linguistics.

Saji, A., Takao, D., Kato, Y., and Matsubara, S. (2021). "Natural Language Inference using Neural Network and Tableau Method." In Proceedings of the 35th Pacific Asia Conference on Language, Information and Computation, pp. 406-414, Shanghai, China. Association for Computational Lingustics.

Tai, W., Kung, H. T., Dong, X., Comiter, M., and Kuo, C.-F. (2020). "exBERT: Extending Pretrained Models with Domain-specific Vocabulary Under Constrained Training Resources." In Findings of the Association for Computational Linguistics: EMNLP 2020, pp. 1433-1439, Online. Association for Computational Linguistics.

Tsuchiya, M. (2018). "Performance Impact Caused by Hidden Bias of Training Data for Recognizing Textual Entailment." In Proceedings of the 11th International Conference on Language Resources and Evaluation, Miyazaki, Japan. European Language Resources Association.

Wang, A., Singh, A., Michael, J., Hill, F., Levy, O., and Bowman, S. (2018). "GLUE: A MultiTask Benchmark and Analysis Platform for Natural Language Understanding." In Proceedings of the 2018 EMNLP Workshop BlackboxNLP: Analyzing and Interpreting Neural Networks for NLP, pp. 353-355, Brussels, Belgium. Association for Computational Linguistics.

Wang, S., Fang, H., Khabsa, M., Mao, H., and Ma, H. (2021). "Entailment as Few-Shot Learner." ArXiv, abs/2104.14690.

Williams, A., Nangia, N., and Bowman, S. (2018). "A Broad-Coverage Challenge Corpus for Sentence Understanding through Inference." In Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Papers), pp. 1112-1122, New Orleans, Louisiana. Association for Computational Linguistics.

Yanaka, H., Mineshima, K., Bekki, D., and Inui, K. (2020). "Do Neural Models Learn Systematicity of Monotonicity Inference in Natural Language?" In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pp. 6105-6117, Online. Association for Computational Linguistics.

## 付録

## A 付録 A

図 16 に，実験の際に関数として作成したタブロー規則の一覧を示す.ここで $C, C_{i}, C_{i}^{\prime}$ は任意の依存構造である。また， $X$ は依存関係であり， $X \in\{$ nsubj, csubj, obj, iobj, ccomp, xcomp $\}$ である。

図 16 作成したタブロー規則の一覧

## 略歴

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

高尾大樹：2017 年名古屋大学工学部卒. 2019 年同大学大学院情報学研究科博士前期課程修了. 現在, 同博士後期課程在学中.

加藤芳秀 : 2003 年名古屋大学大学院工学研究科情報工学専攻博士課程後期課
程修了. 博士 (工学). 同大助手, 助教等を経て, 准教授. 言語処理学会, 情報処理学会, 人工知能学会, 電子情報通信学会, ACL 各会員.

松原茂樹：1998 年名古屋大学大学院工学研究科情報工学専攻博士課程修了.博士 (工学). 同大助手, 助教授, 准教授を経て, 2017 年名古屋大学教授.

(2022 年 9 月 1 日受付)

(2023 年 1 月 26 日再受付)

(2023 年 3 月 3 日採録)