# ニューラルモデルとタブロー法を用いた自然言語推論 のモデル理論的な定式化

佐治 礼仁 1 加藤 芳秀 2 松原 茂樹 1,2
1 名古屋大学大学院情報学研究科 2 名古屋大学情報連携推進本部
saji.ayahito.y7@s.mail.nagoya-u.ac.jp

## 概要

自然言語推論とは，2つのテキストの間に成立す る推論的関係を同定するタスクである. Saji ら [1] は，ニューラルモデルに基づく自然言語推論システ ムと記号操作的な証明手法であるタブロー法を組み 合わせた手法を提案したが，その理論的限界は明ら かではない. 本論文では，Saji らの手法をモデル理論的に定式化し，その定式化に基づいて，手法の性質とその限界を明らかにする。

## 1 はじめに

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

近年，ニューラルモデルに基づく手法が自然言語推論において用いられている（例えば，[2]）。ニュー ラルモデルは単純でありながら，SNLIコーパス [3] やMNLIコーパス [4]を用いた実験において高い正解率を達成している. しかし一方で，この手法に は，判定結果に至る過程や理由を説明する能力を持 たないという問題がある.ニューラルモデルの内部 はブラックボックス化しており，どのような推論 が行われたのかを推察することも困難である。一方，自然言語推論への記号操作的な手法（例えば， $[5,6,7]$ ）が提案されている.この手法は，ニューラ ルモデルによる手法と異なり, 結果に至る推論過程 が人間にとって理解可能であるという利点が挙げら れる. また，この手法における記号操作は一般に，形式論理学や言語学による裏付けが与えられてお
り，そのような推論を行った根拠を与えることがで きる.

Saji ら [1] はこの二つの手法を組み合わせ，ニュー ラル自然言語推論モデルに，記号操作的手法のよう な推論過程を明示化する性質を付加する手法を提案 している.この手法は, 形式論理の証明法の一つで あるタブロー法をその背景としているが，その理論的限界は明らかにされていなかった。

そこで本論文では, モデル理論的に Saji らの手法 を定式化し，その定式化に基づいて，この手法の理論的限界を明らかにする. 具体的には Saji らの手法 について，ある種の健全性が成立する一方で，完全性が成立しないことを示す.

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

## 2.1 タブロー法の概略

本節では，Saji らのタブロー法について説明する。 このタブロー法は，自然言語文と真偽値の対の集合 が与えられたとき，その集合中のすべての文にその 対となる真偽値を割り当てることが可能か否かを証明する。自然言語推論とタブロー法の関係は次のよ うに整理されている. ${ }^{1)}$
- 前提，仮説が共に真となるような真偽値割り当 てが存在しないことが証明されるとき，それ は前提と仮説が矛盾の関係にあることを意味 する。

・前提が真，仮説が偽となるような真偽値割り当 てが存在しないことが証明されるとき，前提が 真であるならば仮説も真となるのは必然であ る，すなわち，前提が仮説を含意することを意味する。

・どちらの証明もできない場合は，前提と仮説は 中立の関係にあることを意味する。


タブロー法では，与えられた文，真偽値の対の集合をもとに, タブローと呼ばれる木構造を構成す る. タブローのノードのラベルは， 3 つ組 $(s, X): Y$ であり，エントリと呼ばれる。これは，文 $s$ が真偽值として $X$ を取らなければならないという制約を 示しており， $Y$ は，このエントリに対して後述する タブロー規則が適用されたか否かを表すフラグであ る. 真偽値は，Tか $\mathrm{F}$ のいずれかであり，それぞれ 真と偽を表す.フラグは，0か 1 のいずれかであり， 0 はタブロー規則が未適用， 1 は適用済みであるこ とを表す. 初期タブローは，与えられた自然言語文 と真偽値の対に対して，規則が適用されていないこ とを示す值 0 をフラグとして付加したエントリから 構成される.これにタブロー規則をエントリに対し て繰り返し適用することによりタブローは導出さ れる。タブロー規則の適用により，エントリが表現 する制約は，より単純な文に関する制約へと分解さ れ，新たなエントリとしてタブローに付け加えられ る. タブローにおける枝分かれは場合分けに相当す る. この分解により, 推論の過程が明示化される. タブロー規則は，以下の形式で表現される. ${ }^{2)}$

$
\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_{1,1}, \cdots, C_{1, n_{1}}, \cdots, C_{m, 1}, \cdots, C_{m, n_{m}}$ は自然言語文と真偽値の対を入力とし, 自然言語文 と真偽値を出力する関数である. タブロー中 に, 次のようなエントリ $(s, X): Y$ が存在すると き，それが支配するすべての葉に新たな $m$ 個の 枝 $\left.\langle C_{1,1}(s, X): 0, \cdots, C_{1, n_{1}}(s, X): 0\right.\rangle, \cdots,\left.\langle C_{m, 1}(s, X)\right.$ : $\left.0, \cdots, C_{m, n_{m}}(s, X): 0\right.\rangle$ を追加する.

・すべての $C_{i, j_{i}}$ について, $C_{i, j_{i}}(s, X)$ は未定義で ない. ${ }^{3)}$
- $Y=0$.

タブロー規則の適用は，適用元のエントリが表現 する制約を，それと等価な制約へと変換する操作と 位置づけられる。例えば， (Either Smith or Anderson signed the contract, $\mathrm{T}$ ): 0 に図 1 左の規則を適用す ると，その経路の終点（タブローの葉）に2つの エントリ (Smith signed the contract, T): 0 と (Anderson signed the contract, $\mathrm{T}$ ): 0 が追加される. また，導出元 のエントリである (Either Smith or Anderson signed the contract, T): 0 のフラグを 1 に変更する. 新たに追加


選言に関する規則条件法に関する規則

図 1 タブロー規則の例

された 2 つのエントリにより表現される制約は，元 のエントリの制約と等価である.

## 2.1.1 タブローの閉鎖

真偽値を割り当てることができないという事実 は，経路，及びタブローの閉鎖という概念により表現される。一般のタブロー法においては，経路上に 真偽値のみが異なるエントリが存在することをもっ て閉鎖経路を定義しているが，Saji らの手法では， これに加えてニューラル自然言語推論モデルに基 づく閉鎖経路を定義している. 自然言語推論モデル は，前提 $p$ と仮説 $h$ を力力とて受け取ると，それ を含意 (E)，中立 (N)，矛盾 (C)のいずれかのクラス に分類すると想定する．以下では， $L \times L(L$ は文の 集合）から $\{E, N, C\} へ の$ 関数を NLI システムと呼び， $N L I(p, h)=$ C といった表記を用いる. 経路上に $2 \supset$ のエントリ $\left(s_{1}, X_{1}\right): 0,\left(s_{2}, X_{2}\right): 0$ が存在し, 次のい ずれかが成り立つとき，その経路は閉じているとい う. 以下では，これを経路の閉鎖条件と呼ぶ.
- $X_{1}=\mathrm{T} \wedge X_{2}=\mathrm{F} \wedge s_{1}=s_{2}$
- $X_{1}=\mathrm{T} \wedge X_{2}=\mathrm{T} \wedge \operatorname{NLI}\left(s_{1}, s_{2}\right)=\mathrm{C}$
- $X_{1}=\mathrm{T} \wedge X_{2}=\mathrm{F} \wedge N L I\left(s_{1}, s_{2}\right)=\mathrm{E}$

全ての経路が閉じているとき，タブローは閉じると いう．タブローが閉じていることは，与えられたエ ントリの集合が表す制約を満たす真偽值割り当てが 存在しないことに相当する。

推論過程の明示化という観点からは，タブロー規則をできる限り適用したタブローに対して閉鎖性を 判定するのが望ましい，以下では，そのようなタブ ローを区別するために，初期タブローにタブロー規則を適用できなくなるまで適用を繰り返したタブ ローを終端タブローと呼ぶことにする。

前提文を T，仮説文を $\mathrm{F}$ としたときの終端タブ ローを含意タブローと呼び，上で述べた 1 番目の ケースの証明に用いる. 前提文と仮説文の両方を $\mathrm{T}$ としたときの終端タブローを矛盾タブローと呼び， これは 2 番目のケースの証明に用いる.

## 3 モデル理論的な定式化

## 3.1 モデル

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

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

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

直観的には，モデルの集合 $M(s)$ は，文 $s$ が成り 立つ状況の集合とみなすことができる.

以下では，モデル集合が与えられたとき，それと 整合性のとれた NLI システム及びタブロー規則がど のようなものであるかを定義し，整合性が取れてい るという条件の下で Saji らのタブロー法による証明 の理論的限界を明らかにする。

定義 2. 次の 3 つの条件が全て成り立つとき，NLI シ ステムはモデル集合 $M$ と整合的であるという.
- $M\left(s_{1}\right) \subseteq M\left(s_{2}\right) \Leftrightarrow N L I\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) \Leftrightarrow$ $N L I\left(s_{1}, s_{2}\right)=\mathrm{N}$
- $M\left(s_{1}\right) \cap M\left(s_{2}\right)=\emptyset \Leftrightarrow N L I\left(s_{1}, s_{2}\right)=\mathrm{C}$

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

以下では，モデルに基づいてタブローを特徴付け るが，その準備として，エントリ，タブローの経路， タブローに対応するモデルを， $M(s)$ を拡張するこ とにより定義する。

定義 3 (エントリに対するモデル集合). タブローの エントリ $e=(s, X): Y$ に対して,$M(e)$ を次のよう に定義する。

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

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

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

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

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

2 節で述べたように，Saji らの手法ではタブロー 規則の適用前後で，エントリが表現する制約が等価 であることが想定されているが，これを以下のよう に定義する。

定義 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_{1, n_{m}}\right)$, $E=L \times\{\mathrm{T}, \mathrm{F}\} \times\{0,1\}, 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_{1, n_{m}}(e)\right)\right)$ また，任意の $r \in R$ が $M$ と整合的であるとき， $R$ は $M$ と整合的であるという.

## 3.2 Saji らのタブロー法の健全性と完全性

本節では，前節で定義したモデルに基づき Saji ら のタブロー法における健全性と完全性を定義する。 また，健全性について証明し，完全性について反例 を示す.

ここで定義する健全性は，含意（矛盾）タブロー が閉じるならば，前提と仮説に対するモデル集合 は，包含（互いに素な）関係にあるという性質であ る.これを前節で導入したモデルに基づき定式化す ると，次のように定義できる。

定義 7 (含意タブロー・矛盾タブローの健全性). $M$ をモデル集合， $R$ を $M$ と整合的なタブロー規則の 集合，NLIを $M$ と整合的である NLI システムであ るとする．任意の前提文 $p$ と仮説文 $h$ について，次 の条件が成り立つならば， $R$ と NLIによる閉鎖性判定は，モデル集合 $M$ において健全であるという.

・Rによって構成された含意タブローが NLI に よって閉じると判定されるならば， $M(p) \subseteq$ $M(h)$ が成り立つ.

・ $R$ によって構成された矛盾タブローが $N L I$ によって閉じると判定されるならば， $M(p) \cap$ $M(h)=\emptyset$ が成り立つ.
一方で，完全性は次のように定義する。

定義 8 (含意タブロー・矛盾タブローの完全性). $M$ をモデル集合， $R$ を $M$ と整合的なタブロー規則の 集合，NLIを $M$ と整合的である NLI システムであ るとする。任意の前提文 $p$ と仮説文 $h$ につて，次 の条件が成り立つならば， $R$ と $N L I$ による閉鎖性判定は，モデル集合 $M$ において完全であるという.

$\cdot$ $M(p) \subseteq M(h)$ が成り立つなら，Rによって構成 された含意タブローが NLIによって閉じると 判定される.

・ $M(p) \cap M(h)=\emptyset$ が成り立つならば， $R$ によっ て構成された矛盾タブローが NLIによって閉 じると判定される.

## 3.2.1 健全性の証明

本節では，まず健全性を証明するための補助定理 を導入し，それにも基づき健全性を証明する。

補助定理 1. $R$ が $M$ と整合的であるならば，任意の $r \in R$ の適用前のエントリの集合に対応するモデル 集合と, その $r$ の適用後のエントリの集合に対応す るモデル集合が等しい.

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

補助定理 2. $t_{\text {start }}$ を初期タブローとし， $t_{\text {trm }}$ を $t_{\text {start }}$ か ら導かれる終端タブローとする． $R$ が $M$ と整合的 であるならば， $M\left(t_{\text {start }}\right)=M\left(t_{\text {trm }}\right)$ である.

補助定理 2 は補助定理 1 から明らかである. 含意 タブローの健全性の証明は次の通りである． $R$ に よって構成された含意タブロー $t_{\mathrm{trm}}$ が $N L I$ によって 閉じていると判定されるとする。このとき， $t_{\mathrm{trm}}$ の すべての経路 $b$ に閉鎖条件のいずれかを満たす 2 つ のエントリ $\left(s_{1}, X_{1}\right): 0,\left(s_{2}, X_{2}\right): 0$ が存在する.

・ 1 番目の閉鎖条件を満たすならば，定義 1 より $s_{1}=s_{2}$. したがって, $M\left(\left(s_{1}, \mathrm{~T}\right)\right) \cap M\left(\left(s_{2}, \mathrm{~F}\right)\right)=$ $M\left(\left(s_{1}, \mathrm{~T}\right)\right) \cap M\left(\left(s_{1}, \mathrm{~F}\right)\right)=\emptyset$.

・2 番目の閉鎖条件を満たすならば，定義 2 より $N L I\left(s_{1}, s_{2}\right)=$ Cであるが，NLI は $M$ と整合的で あるので $M\left(s_{1}\right) \cap M\left(s_{2}\right)=\emptyset$. よって，定義 3 よ り $M\left(\left(s_{1}, \mathrm{~T}\right)\right) \cap M\left(\left(s_{2}, \mathrm{~T}\right)\right)=\emptyset$.

・ 3 番目の閉鎖条件を満たすならば，定義 2 より $N L I\left(s_{1}, s_{2}\right)=\mathrm{E}$ であるが，NLI は $M$ と 整合的であるので $M\left(s_{1}\right) \subseteq M\left(s_{2}\right)$. よって，定義 3 より $M\left(\left(s_{1}, \mathrm{~T}\right)\right) \subseteq M\left(\left(s_{2}, \mathrm{~T}\right)\right)$ すなわち， $M\left(\left(s_{1}, \mathrm{~T}\right)\right) \cap M\left(\left(s_{2}, \mathrm{~F}\right)\right)=\emptyset$.

以上より, $M\left(\left(s_{1}, X_{1}\right)\right) \cap M\left(\left(s_{2}, X_{2}\right)\right)=\emptyset$. 沟えに，定
1 (Smith and Anderson didn't go out, $T$ ): 1

2 (Smith and Anderson were home, F): 1

(Smith or Anderson went out, F): 1

4 (Smith went out, F): 0

(Anderson went out, F): 0

6 (Smith was home, F): $0 \quad 7$ (Anderson was home, F): 0

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

義 4 より $M(b)=\emptyset$ となる. したがって，定義 5 から $M\left(t_{\text {trm }}\right)=\emptyset$ である. $t_{\text {start }}$ を $t_{\text {trm }}$ の初期タブローとす ると, 補助定理 2 から $M\left(t_{\text {start }}\right)=\emptyset$ である. 初期夕 ブローは $(p, \mathrm{~T}): 0,(h, \mathrm{~T}): 0$ から構成されるため，定義 4, 5 から $M((p, \mathrm{~T})) \cap M((h, \mathrm{~F}))=\emptyset$. したがって， $M((p, \mathrm{~T})) \subseteq M((h, \mathrm{~T}))$. 定義 3 から $M(p) \subseteq M(h)$ で ある。以上より題意は満たされる。矛盾タブローの 健全性も同様に証明できる。

## 3.2.2 完全性の反例

本節では，含意タブローの完全性の反例を示す.

図 2 に示す含意タブローにおいて，タブロー規則が未適用であるエントリ 4505670 真偽值は いずれもがFである。閉鎖条件においては，いず れかのエントリの真偽値が Tでなければならな い.このため，この含意タブローは，どのような $N L I$ を用いても閉じていると判定されることはな い。この例に対して $M$ を用意し，それと整合的で $N L I(1,2)=\mathrm{E}(\Leftrightarrow M(\boxed{1}) \subseteq M(\boxed{2})$ )であるよう な $N L I$ は容易に構成できるが，この $M$ 及び NLIに おいて含意タブローは閉じると判定されない。すな わち，完全性が成立しない。矛盾タブローについて も同様の反例が存在する。つまり，完全性は一般に 成立しない。

## 4 おわりに

本論文は，Saji らの手法をモデル理論的に定式化 し，その定式化に基づいて，その性質を明らかにし た。一般に，健全性は成り立つが完全性は成り立た ないことを示した．現在，タブロー規則集合が特定 の条件を満たすとき，完全性が成り立つようなケー スを確認しているが，今後の課題としては，そのよ うな条件がいかなるものであるかの分析が挙げら れる。

## 参考文献

[1] Ayahito Saji, Daiki Takao, Yoshihide Kato, and Shigeki Matsubara. 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, November 2021. Association for Computational Lingustics.

[2] Qian Chen, Xiaodan Zhu, Zhen-Hua Ling, Si Wei, Hui Jiang, and Diana Inkpen. 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, July 2017. Association for Computational Linguistics.

[3] Samuel R. Bowman, Gabor Angeli, Christopher Potts, and Christopher D. Manning. 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, September 2015. Association for Computational Linguistics.

[4] Adina Williams, Nikita Nangia, and Samuel Bowman. 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, June 2018. Association for Computational Linguistics.

[5] Bill MacCartney and Christopher D. Manning. Natural logic for textual inference. In Proceedings of the ACL-PASCAL Workshop on Textual Entailment and Paraphrasing, pp. 193-200, Prague, June 2007. Association for Computational Linguistics.

[6] Lasha Abzianidze. 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, September 2015. Association for Computational Linguistics.

[7] Lasha Abzianidze. 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, September 2017. Association for Computational Linguistics.
 佐治 礼仁 1 加藤 芳秀 2 松原 茂樹 1,2 1 名古屋大学大学院情報学研究科 2 名古屋大学情報連携推進本部 saji.ayahito.y7@s.mail.nagoya-u.ac.jp  