NeuralWani：依存型理論のための自動定理証明器waniの高速化に向けて

計算言語学では，自然言語の構造的な意味に関わる計算過程を明らかにする取り組みが長年行われている．計算言語学の目的の一つは言語現象の背後にある計算機構の解明であるが，手計算で計算過程を明らかにするのは困難である．そこで，計算を自動化するパイプラインシステムの構築が求められてきた．その中で，Tomitaetal.[1]はCCG統語・意味解析器lightblue1）[2]と依存型理論(DependentTypeTheory:DTT)[3]のための定理自動証明器wani[4,5]を組み合わせた自然言語推論システムを提唱・実装した．この自然言語推論システムでは，自然言語の文を入力とし，統語解析，意味解析，型検査，照応・前提解決，自動定理証明を経て，推論の結果を出力する．1.1wani上述の自然言語推論システムに組み込まれている定理自動証明器waniは，証明体系としてDTTを採∗本研究は著者が独自に実施したものであり，Amazonの見解や立場を反映するものではない．1）https://github.com/DaisukeBekki/lightblue/用している．DTTの型判定(judgment)は，以下の形式をもつ．Γ⊢𝑀:𝐴Γを環境(context)，𝑀を項(term)，𝐴を型(type)としたとき，上記の型判定は，型理論の観点からは「環境Γのもとで項𝑀が型𝐴を持つ」ことを意味する．同時に，証明論の観点からは「前提Γから帰結𝐴に至る証明𝑀が存在する」ことを意味する（カリー・ハワード対応）．証明項𝑀が未知である以下のような型判定を証明探索クエリといい，証明探索クエリに対して証明項を探索するタスクを証明探索と呼ぶ．Γ⊢?:𝐴waniでは証明探索を解くために，前向き推論と後ろ向き推論を組み合わせて探索を行う．前向き推論では，「前提から何が導けるか」という点に着目し，上から下へと証明木を構築する．一方，後ろ向き推論では，「与えられた命題を示すには何が必要なのか」という点に着目し，下から上へと証明木を構築する．その際，示したい命題に規則を適用し，それを示すために必要な条件をミニゴールとして割り出す．1.2依存型意味論(DTS)§1節で述べた自然言語推論システムでは，意味表示・意味合成の枠組みとして依存型意味論(DependentTypeSemantics:DTS)[6,7]を採用している．DTSはDTTに基づく自然言語の意味の理論である．DTTでは，関数型と直積型の一般化としてΠ型とΣ型を用い，それぞれ(𝑥:𝐴)→𝐵，(𝑥:𝐴)×𝐵と表現する．後件の型𝐵が前件の型𝐴に依存できる性質を持つことから，DTSでは先行する文の意味に依存した文の意味を表すことができる．これにより，DTSでは照応解決・前提束縛といった複雑な言語現象を扱うことが可能となる．Thisworkispublishedwithoutpeerreviewandislicensedbytheauthor(s)underCCBY4.0(https://creativecommons.org/licenses/by/4.0/).org/licenses/by/4.0/).ファイル1SYN001+1.pの例%---------------------------------------------%File:SYN001+1:TPTPv9.2.1.Releasedv2.0.0.%Domain:Syntactic%...（ヘッダー情報の省略）...%---------------------------------------------fof(pel2,conjecture,(~~p<=>p)).%---------------------------------------------4評価実験4.1学習・評価用データセット本実験では，学習・評価用データとして，TPTP(ThousandsofProblemsforTheoremProvers)ProblemLibrary2）[11]を使用した．具体的には，ファイル1のようなSYN(Syntactic)ドメインのFOF(ﬁrst-orderform)問題を対象とし，以下の手順でデータの抽出を行った．1.字句解析器生成系Alexおよび構文解析器生成系Happyを用いて，TPTPの問題をDTTの証明探索問題へと変換する．