形式論理学に基づく演繹コーパスによる言語モデルに対する演繹推論能力の付与

論理的に物事を考える機械の実現は，人工知能黎明期からの夢である[1]．このゴールに対して近年，様々な論理推論ベンチマークが提案されている[2,3,4,5]．これらは通常，優れた言語理解能力を持つ最先端の言語モデルを用いて取り組まれている．しかしながら，言語モデルをもってしても論理推論は難しいことが認識されつつある[6,7,8]．言語モデルは，人間が書いた文章中の多くの良質な事例から，言語理解能力を帰納的に獲得した[9].逆に考えると，言語モデルの論理推論能力の低さは，人間が書いた文章中に良質な論理推論の事例が十分数含まれていないことを示唆している．そうであるならば，良質な論理推論の事例を多く含むコーパスを生成し，言語モデルに学習させることで，論理推論能力を獲得することができるはずである．このようなコーパスの1つとして，近年提案されたRuleTaker[10]が挙げられる．RuleTakerは，自動生成された多段演繹証明を含む．各演繹証明は，与えられた事実の集合に対して演繹規則を複数回適用することにより，仮説を証明(あるいは反証)する(図1中の“DeductionInstance”と同様)．演繹規則としては，∀𝑥𝐹(𝑥)→𝐺(𝑥),𝐹(𝑎)⊢𝐺(𝑎)(⊢は“導出する”の意)等の，含意に類する規則が用いられた．ArtiﬁcalArgumentCorpus[11]はRuleTaker同様，自動生成された一段演繹証明からなるコーパスで，演繹規則として人手で選ばれたクリティカル・シンキングに役立つ規則，例えば対偶F→G⊢¬G→¬F(¬は否定)が用いられた．これらの演繹コーパスはいずれも，最も普遍的な論理推論能力の一つである，演繹推論能力を獲得する機会を提供し得る．しかしながら，これら演繹コーパスで採用された演繹規則は少数に限られ，また，恣意的であった．現実世界の複雑な演繹推論では多様な演繹規則が求められるため，再考する必要がある．本研究はこの問題に答えることを目指す．まず，形式論理学(FormalLogic)を訪れる(2節)．形式論理学によれば，既存コーパスで使用された演繹規則も含め，妥当な演繹規則は無限に存在する．しかし，その中でも基本的な演繹規則群(公理系)が存在し，公理系による多段演繹推論によって，その他の任意の演繹規則を導出できる（完全性)．よって，公理系による多段演繹推論は任意の演繹規則による多段演繹推論を模擬することができる．既存コーパスの演繹規則群はこの性質を持たないので，たとえそれらを獲得したとしても，他の多様な演繹規則を模擬できない．我々はこの点を改め，演繹規則群として公理系を採用したコーパスFLD(FormalLogicDeduction,3節)を構築し，言語モデルに公理系を用いた演繹推論能力を獲得させることを目指す．次にFLDの有効性を実験的に確かめる(4節-6節)．複数種のベンチマークにて，FLDで学習された言語モデルが既存コーパスで学習された言語モデルより頑健な演繹推論能力を持つことを示す．最後に，FLDコーパス・ソースコード・学習済みモデルを公開する1）．FLDコーパスは既存コーパスより挑戦的なのでベンチマークとして有用である．1）https://github.com/hitachi-nlp/FLD.ProofTreeArguments(deductionrules)ProofModusponensTreeGenerator𝓕𝓕𝓕𝓕→𝓖𝓖→introduction…∧elimination𝓖𝓖…Modusponenstreedepth=3#ofbranches=5𝓕𝓕𝓕𝓕→𝓖𝓖𝓗𝓗formulacomplexityforwardupto2propositions𝓖𝓖with∧,∨,¬(default)theaxiomsoffirst-orderpredicatelogicNaturalLanguageNLtemplatesAssigner{𝐴𝐴}→{𝐵𝐵}:“if{𝐴𝐴},then{B}”“{A}resultsin{B}”∀𝑥𝑥{𝐴𝐴}𝑥𝑥→{𝐵𝐵}(𝑥𝑥):“ifsomethingis{𝐴𝐴},thenitisalso{𝐵𝐵}”Vocab=100000“{𝐴𝐴}thingsare{𝐵𝐵}”