自然言語推論(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}，AdversarialNLI(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}．このアプローチには，ニューラルモデルによるものと異なり，推論の論理的な過程を明示できるという利点がある．また，推論における記号操作は，論理学や言語学による裏付けが与えられているため，推論の根拠を示すことができる．しかし，このアプローチでは，推論規則を人手で作成する必要があり，語の同義・対義関係や上位・下位関係を網羅的に扱うことが難しいという問題がある．加えて，「雨が降ると地面が濡れる」といった常識的知識を推論規則として表現しなければならず，それを人手で網羅することは困難である．実際，記号操作に基づくアプローチは，FraCaStestsuite\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章では，関連研究を整理し，提案手法との違いを示す．%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%