証明支援系Coqを用いた依存型意味論の照応解析と推論の実装の試み

含意関係認識(RecognizingTextualEntailment)とは，テキスト𝑇が仮説𝐻を含意するかどうかを判定するタスクであり，質問応答(questionanswering)など，さまざまな応用をもつ．このタスクに対しては，大規模なデータを用いてニューラルモデルに含意関係を学習させる深層学習アプローチ[1,2]，定理証明器を用いる論理推論アプローチ[3,4]，およびこの二つを組み合わせるハイブリッドアプローチ[5]がある．論理推論アプローチではさまざまな定理証明器が用いられており，その中には定理証明器Coq[6]を用いるものがある[7,8,9,10,11,12,13]．証明支援系(proofassistants)とも呼ばれるCoqを用いるこのアプローチには以下の利点がある．まず，依存型理論(dependenttypetheory)に基づくCoqでは，自然言語の文がもつ複雑な意味構造を捉えることができる．さらに，証明状態を遷移させることのできる「タクティク」と呼ばれるものを合成することで，ユーザー定義の自動証明手続きを定式化することができる．以上に加え，論理推論アプローチ一般がもつ利点として，含意関係認識タスクにおける判定結果の解釈・判定手続きの修正が容易である点も挙げられる．これまで，様相表現・一般化量化子などを含むさまざまなテキストに対する含意関係認識タスクがCoqアプローチにより研究されてきた．その一方で，照応解析(anaphoraresolution)の結果を含意関係認識の中で用いるという二重タスクを，Coqが提供するタクティクのみを用いて行う手法はこれまでに提案されていない．照応解析とは，英語を例にとれば，テキストの中にある“it”や“he”などの照応表現の指示対象を指定するタスクであり，自然言語処理や形式意味論といった分野で研究されている．次の例は，照応表現を含むテキストに関する含意関係認識を行うには照応解析が必要であることを示している[14,p.46]:Amanentered.Hewhistled.=⇒Amanwhistled.照応解析に続く含意関係認識のためのタクティク整備へ向けて，本研究ではまず，照応解析をCoqタクティクによって行う手法を定式化する．この目的のために，自然言語意味論のフレームワークである依存型意味論(DependentTypeSemantics,DTS)をCoqで実装する．DTSでは未指定項(underspeciﬁedterms)を用いた照応解析手続き[15,16,17]が定式化されており，本研究の基本アイデアは，このDTS照応解析手続きをCoqが提供するrefineタクティクによりシミュレートするというものである．次に，照応解析の結果，テキストが仮説を含意する場合は，その含意関係をCoq内の定理として証明する手法を提案する．