# 定理証明に基づく対話的な自然言語推論システム

隅田敦
東京大学
atsushisumita0421@gmail.com
}

峯島宏次
慶應義塾大学
}

minesima@abelard.flet.keio.ac.jp

宮尾祐介

東京大学

yusuke@is.s.u-tokyo.ac.jp
## 1 概要

自然言語推論 (Natural Language Inference; NLI) と は, ある文から別の文が帰結するか否かを判定する タスクである [1]. 自然言語推論は質問応答, 自動要約, ファクトチェックなどの様々な応用先が考えら れ, 近年では自然言語理解のベンチマークとしても 重要性を増している [2].

本論文では, 計算機と人間のインタラクションが NLI を解く上で有益であるかを検討する.ここでイ ンタラクションとは, 人間と計算機が互いの弱みを 補完しながら協力して NLI タスクを解くという形式 を想定している. 一般的に, 人間の方が語彙間の含意関係や常識推論などの柔らかい判断に優れる一方 で, 計算機の方が交錯した論理関係の包括的な探索 や検証において優位性があると考えられる. 自然言語推論は様々な意味現象が組み合わさった複雑な夕 スクであり,これら両方の意味現象を処理する必要 がある.

本研究では形式意味論と定理証明器を用いるアプ ローチに着目する. 定理証明器は 複雑な数学的命題 や形式手法の証明を補佐するためのソフトウェアで あり, 人間と計算機が互いの強みを活かしてインタ ラクティブに複雑な課題を解決している好例であ る.いくつかの既存研究において, 自然言語の意味を 論理式を用いてモデル化する形式意味論 $[3,4]$ と組 み合わせることで, 定理証明器を NLI に応用するこ とが出来ることが示されている $[5,6,7]$. しかし, 定理証明器の重要な特徴であるインタラクティブな課題解決という側面に目を向けた NLI システムはこれ までに十分に研究が行われて来なかった.

そこで, 本研究では形式意味論と定理証明器に基 づいた NLI システムである ccg2lambda [8] に, 証明
に関する知識が不足した際にユーザーが自然言語で インタラクションを行うことが出来るシステムを提案する。

仮説の検証のために，SICK [9] をデータセット， Amazon Mechanical Turk にて募ったクラウドワー カーを被験者として適合率, 再現率, 精度を計測し, エラー分析を行った. 以降で提案手法と実験につい て詳細に説明する。

## 2 提案手法

本節ではユーザーと定理証明器とのインタラク ションを実現するための提案手法について説明す る. 重要な点として,インタラクションは基本的に自然言語で行われる.これにより, 形式意味論や定理証明器について知識がないユーザーであってもインタ ラクションが可能となる.

図 1 に提案手法の大枠を示した. 提案手法の内, セ マンティックパーザーと定理証明器については既存手法を用いている. まず，ユーザーが証明したい文の 組をシステムに入力し,これがセマンティックパー ザーにより論理式に変換される.これが定理証明器 に入力される. 定理証明器は証明をいくつかのサブ ゴールと呼ばれる命題に分解し, 全てのサブゴール が証明された時に全体の証明が完成する. 図 1 の例 では, person $(x 0)$, move $(e 0)$ がサブゴールである.

本研究ではサブゴールを自然言語に変換しユー ザーに提示するインタラクティブな NLI システムを 提案する. 以下, サブゴールを自然言語に変換したも のを可読なサブゴールと呼ぶことにする.より正確 には, あるサブゴールの可読なサブゴールとは, 前提文とそのサブゴールが真の時かつその時のみ真と なるような自然言語文のことである。図の例では, person $(x 0)$, move $(e 0)$ に対応する可読なサブゴール

(1)ユーザーの入カを論理式に変換

図 1 提案手法によるインタラクションの例. ユーザーが証明したい文対を入力すると, セマンティックパーザーにより 文対が論理表現に変換され，定理証明器に入力される。証明が完成しなかった場合にサブゴールを抽出し，提案手法に より可読なサブゴールが生成されユーザーに提示される. ユーザーの反応に応じて公理が生成され，証明が続行される.

は The man is a person, The man is moving となる. ユー ザーが可読なサブゴールの真偽を入力すると, それ に応じて新たな論理式が公理として生成され, 定理証明器にフィードバックされる. 以下でより詳細な ステップについて説明する。

## 2.1 可読なサブゴールの生成

サブゴールを可読なサブゴールに変換する問題を 考える. 以下の説明では, 図 1 中の move $(e 0)$ を例に とる.

サブゴールを自然言語文に変換するためには, サ ブゴールに含まれていないが自然言語文には必須の 要素を識別し正しく補充することが必要となる. 例 えば, 適格な (英語の) 自然言語文は主語が必ず必要 である. move $(e 0)$ の例では, 誰が moveしているのか を識別しなければならない。

まず第一ステップとして, 可読なサブゴールに含 めるべき変数の集合を識別する.これは論理式中の 意味役割を表す式から識別できる. 意味役割は主語 や動詞の必須項などを表現しており, 適格な自然言語文には含める必要がある. よって, 各変数について その変数が含まれている意味役割の式を抽出し, そ の式に含まれている全ての変数を集合に追加すると いう手続きを再帰的に適用すれば良い. 現在の例で は, $\operatorname{Subj}(e 0)=x 0$ から 可読なサブゴールに含める べき変数は $\{e 0, x 0\}$ であることが分かる.次のステップでは，それぞれの変数に語を割り 当て, 変数の内容を自然言語で表す.これには, そ の変数を引数としている述語を選択すれば良い.現在の手法では entity 型の変数に関してはそれを 引数に取る名詞を, event 型の変数に関してはそ れを引数に取る動詞を選択している. 現在の例で は, $x 0$ には man, $e 0$ には move を選ぶ. 結果として, $\{e 0$ : “move”, $x 0$ : “man” $\}$ を得る.

最後に, 得られた語の正しい語順と必要な機能語 を適宜補充し, 文法的に正しい文を生成する. 可読な サブゴールはごく簡単な宣言文なので, 語の品詞か ら語順, 時制, 必要な機能語を特定するルールベース のシステムが比較的容易に構築可能である.この例 では, The man is moving が可読なサブゴールとなる.

表 1 に実際に生成された可読なサブゴールを示し た. 二列目にサブゴール, 三列目に可読なサブゴール が示されている.

## 2.2 ユーザーの反応

可読なサブゴールを受け取ったユーザーは true, false, unknown から一つを選び, これを返答とする。 true が選択されると, 可読なサブゴールが論理表現 に変換され, 公理として定理証明器に追加される. false が選ばれた場合には可読なサブゴールを否定 した論理表現が追加される. unknown が選ばれた場合には公理は追加されず, 証明が完成しないことが

 & boy $(x 0)$ & The kid is a boy. & $\forall x, \operatorname{kid}(x) \rightarrow \operatorname{boy}(x)$ \\
 & & & \\

and the man is smiling nearby. & near $(e 0, x 1)$ & The man is with a smile. & $\forall x, y, e, \operatorname{boy}(x) \rightarrow$ \\
H: The kids are playing outdoors near a & with $(e 1, ? x 2)$ & The boys are near a man. & $\operatorname{Subj}(x)=e \wedge \operatorname{near}(e, y)$ \\
man with a smile. & $\operatorname{smile}(? x 2)$ & & $\wedge \operatorname{man}(y)$ \\

H: Two dogs are wrestling and hugging. & hug $(e 1)$ & The dogs are hugging. & $\forall e, \operatorname{fight}(e) \rightarrow \operatorname{wrestle}(e)$ \\

表 1 文のペアに SICK の訓練データから抽出した文を示している，T から始まる文が前提文, $\mathbf{H}$ から始まる文が帰結文 であり, 前者から後者への含意関係を示すことがタスクの内容となる. イタリックで示した箇所が非論理的推論が必要と なる箇所であり, サブゴールとして定理証明器により出力される. サブゴールには定理証明器が証明出来なかった命題を 示している. 可読なサブゴールには提案手法が生成しユーザーに提示された文を示した. 公理にはユーザーが trueで反応した場合に生成される論理式を示した.

表 2 SICK における適合率, 再現率, 精度. チェックマークは axiom injection [5], readable subgoal は提案手法の可読なサブ ゴールを使用しているか否かを示している。

確定するのでプロセスが停止する. 表 1 の四列目に trueが選択された場合の公理を示した.

## 3 実験

## 3.1 データ

提案手法の評価には, 語彙的な推論と論理的な推論の両方を適度に含み, 関連する既存手法 $[5,6]$ にお いても使用されている自然言語推論データセットで ある SICK [9]を用いた. SICK は 10000 件の文対から 成り, 各文対について一つ目の文から二つ目の文が 帰結するか否かを判定する分類タスクである. 正解 ラベルは entailment, contradiction, neutral の三通りで ある.

## 3.2 実験設定

セマンティックパーザーには ccg2lambda [8], 定理証明器に Coq [10] を使用した. SICK の訓練データか らサンプルした 1000 ペアを depccg と ccg2lambdaに より論理表現に変換し, 定理証明器に渡して証明を 行った. 定理証明器が証明を完成させた場合はプロ セスが終了する. 証明が完成しなかった場合はサブ ゴールを抽出し, 提案手法により可読なサブゴール
を生成し, ユーザーがインタラクションを行う. 本実験においては Amazon Mechanical Turkにより被験者 を募り,各ペアについて 3 人が true, false, unknown を 付与した. 精度を高めるため, 3 人が一致した時のみ 公理を生成した。

## 3.3 結果

適合率, 再現率, 精度を表 2 に示した. 一行目の ベースラインは majority class であり, $61.5 \%$ を占め る neutral の割合を示している. 二行目は ccg2lambda [8] の結果であり, $99.7 \%$ と高い適合率を達成してい るが, 再現率が $34.7 \%$ と低く, 全体として低い精度と なっている. 三行目に ccg2lambdaを拡張し知識デー タベースから公理生成を行う word abduction [5] の結果を示した. 語彙的推論がカバーされたため再現率 が $53.8 \%$ に向上している. 四行目に提案手法の結果 を示した. 再現率は $59.0 \%$ と最も高く, 偽陽性も少な く適合率の高さも維持されたため, 精度についても 比較した手法の中では最も良い結果となった.

## 3.4 エラー分析

提案手法の成功例と失敗例について表 3 にまと めた.

 & Yes & Yes & The helmet is red. \\

表 3 本実験中に得られた提案手法の成功例と失敗例. 単純な語彙間の含意関係では捉えられない句間の含意関係が捉え られている (1-2 行目). 一方で, 帰結文との重複が多いケース (3 行目) や蓋然性を高めるだけの関係を含意とアノテーショ ンしてしまうケース (4-5 行目) が多く見られた.

一行目のペアは成功例である.この証明を完成さ せるためには, 句間に成立する含意関係を認識する 必要があり, 単純な語彙間の含意関係に基づいた手法では処理することが出来ない. より形式的には, こ こで用いられている知識は以下のようなものであ る. The helmet is red については

$
\begin{aligned}
& \forall x, y, e, \operatorname{paint}(e) \wedge \operatorname{red}(x) \wedge(\operatorname{Acc}(e)=x) \\
& \wedge(\operatorname{Dat}(e)=y) \rightarrow \operatorname{red}(y)
\end{aligned}
$

The man is a motorcyclist については

$
\begin{gathered}
\forall e, x, y, \text { ride }(e) \wedge \operatorname{man}(x) \wedge \operatorname{motorcycle}(y) \\
\rightarrow \operatorname{motorcyclist}(x)
\end{gathered}
$

実際この例においては知識ベースにより公理を生成する既存手法 [5] は証明を完成させることが出来 ていない. 二行目に示した例も同様に, ride the wave から surf を導く必要がる.

三行目に示した例は成功しているがやや問題を含 んでいる. 可読なサブゴールは正しく生成され予測結果も正しいが, 帰結文とほとんど重複してしまっ ている.これは帰結文が短すぎるために分解の余地 がないためである.したがってこのようなケースで は可読なサブゴールを介する有用性が低く, より長 い前提文・帰結文において提案手法が価値を発揮す ることが示唆される。

四行目に示した例は典型的な失敗例である.この 例では The stage is a podium という可読なサブゴール に対して true とラベルが付与されたが, 全ての stage が podium である訳ではないので unknown が正しい 反応となる. ただしこの文脈で stage が podium であ るという蓋然性は高く, このようなケースと他の語彙間の含意関係や常識判断の間に厳密な線を引くの は難しい. 五行目に示した例も同様である.
また, 曖昧性のある場合にも解析誤りが見られ た. 例えば The men are women はその女性は男性であ るともその女性は人間であるとも解釈でき, それぞ れの解釈の下で適切な反応が異なってしまう。この ような曖昧性の解消が将来的には必要になると考え られる。

他の失敗ケースで多く見られたのは CCG タグ付 けやセマンティックパーザーなどの前処理の段階で の解析結果の誤りが影響するケースである. 特に複合表現など構成性を満たさない表現は誤った意味表現が付与される例が多く見られた.

## 4 結論と今後の課題

本論文では形式意味論と定理証明器に基づいたイ ンタラクティブな自然言語推論システムを提案し た. 実験の結果, 提案手法により再現率と精度が向上 しており,ユーザーとのインタラクションが有益で あることが示された.

今後の課題としては, 前節で示した典型的な失敗例の解決に加え, より複雑な設定でインタラクショ ンを成立させることが挙げられる. SICK は単文と単文の間の含意関係を認識するタスクだが, 人間が論理関係を包括的に把握するのが困難な量のドキュメ ントを前提文とする場合の方が応用上は有益であ る. そのためには共参照などの問題を考慮する必要 が生じる. また, SICK では非論理的推論のほとんど がシンプルな語彙間の推論だが, 常識推論などのよ り高度かつ計算機には処理が難しい推論を含んだ場合にもインタラクションを成立させることが出来れ ば, ユーザーとシステムの協働により高い価值を見 いだせるので,これらを今後の課題としたい.

## 参考文献

[1] Omer Levy, Torsten Zesch, Ido Dagan, and Iryna Gurevych. Recognizing partial textual entailment. In Proceedings of the 51st Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), pages 451-455, Sofia, Bulgaria, August 2013. Association for Computational Linguistics.

[2] Alex Wang, Amanpreet Singh, Julian Michael, Felix Hill, Omer Levy, and Samuel Bowman. GLUE: A multi-task benchmark and analysis platform for natural language understanding. In Proceedings of the 2018 EMNLP Workshop BlackboxNLP: Analyzing and Interpreting Neural Networks for NLP, pages 353-355, Brussels, Belgium, November 2018. Association for Computational Linguistics.

[3] Terence Parsons. Events in the Semantics of English. MIT Press, 1990

[4] Claudia Maienborn. Event semantics. In Claudia Maienborn, Klaus von Heusinger, and Paul Portner, editors, Semantics. An International Handbook of Natural Language Meaning, volume 1, pages 802829. Mouton de Gruyter, 2011.

[5] Pascual Martínez-Gómez, Koji Mineshima, Yusuke Miyao, and Daisuke Bekki. On-demand injection of lexical knowledge for recognising textual entailment. In Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 1, Long Papers, pages 710-720, Valencia, Spain, April 2017. Association for Computational Linguistics.

[6] Hitomi Yanaka, Koji Mineshima, Pascual MartínezGómez, and Daisuke Bekki. Acquisition of phrase correspondences using natural deduction proofs. In Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Papers), pages 756-766, New Orleans, Louisiana, June 2018. 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, pages 115-120,
Copenhagen, Denmark, September 2017. Association for Computational Linguistics.

[8] Pascual Martínez-Gómez, Koji Mineshima, Yusuke Miyao, and Daisuke Bekki. ccg2lambda: A compositional semantics system. In Proceedings of ACL2016 System Demonstrations, pages 85-90, Berlin, Germany, August 2016. Association for Computational Linguistics.

[9] Marco Marelli, Stefano Menini, Marco Baroni, Luisa Bentivogli, Raffaella Bernardi, and Roberto Zamparelli. A SICK cure for the evaluation of compositional distributional semantic models. In Proceedings of the Ninth International Conference on Language Resources and Evaluation (LREC'14), pages 216-223, Reykjavik, Iceland, May 2014. European Language Resources Association (ELRA).

[10] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development: Coq'Art: the Calculus of Inductive Constructions. Springer, 2013.
 隅田敦 東京大学 atsushisumita0421@gmail.com }  峯島宏次 慶應義塾大学 }  minesima@abelard.flet.keio.ac.jp  宮尾祐介  東京大学  yusuke@is.s.u-tokyo.ac.jp 