研究プロジェクト

戸次研究室は、言語学、論理学、哲学、自然言語処理の融合分野である数理言語学を専門としており、同分野においてこれまで主に三つの研究成果を挙げている。第一に、形式統語論の研究として、組み合わせ範疇文法(CCG)に基づく網羅的、形式的、統合的な日本語文法理論を構築したこと、第二に、形式意味論の研究として、依存型理論に基づく合成的な証明論的談話意味論である「依存型意味論」の枠組みを新たに提案したこと、第三に、自然言語処理の研究として、頑健なCCGパーザと高階論理に基づく自動推論を組み合わせた含意関係認識システム"ccg2lamda"を完成させたこと、である。これら三つの研究は全体として、記号列と意味がどのように対応しているかという理論言語学の問題、意味とは何かという言語哲学の問題、人間がどのような機構によって文から意味を理解するかという自然言語処理の問題に、統一的な回答を与えうる研究プログラムを提供する。

日本語や英語のような自然言語の統語論と意味論の研究、すなわち、記号列と意味を対応付けている機構の研究には、理論言語学と自然言語処理という二つの研究分野からの視点がある。前者は、チョムスキーに始まる生成文法、モンタギューに始まる形式意味論を代表とする「自然科学としての言語学」である。後者は、たとえば「人間の言葉を理解する人工知能の実現」といった、あるいは「自然言語をインターフェイスとするサービスの質を向上させる」といった計算機による自然言語の処理を目指す情報工学である。

理想的には、前者が提供する理論、もしくはその近似が、後者においても解決法を提供するべきであるが、現実には、両者は1980年代後半から90年代半ばにかけて袂を分かち、内容的にも人的にもほぼ無関係となった。自然言語処理における数理モデルは理論言語学が用いてきた形式言語理論・高階内包論理から大きく乖離し、統計モデルやニューラルモデルを用いた機械学習の手法が主流となった。近年では特に深層学習による言語処理が注目されているが、たとえば現在の日本語処理で理解できる「意味」の射程は、一般に抱かれる印象とは異なり、単文内における述語と名前の関係（述語項構造と呼ばれる）に限られている。それを越える「意味」については、いわば大雑把な推量を行うことしかできず、形式意味論が説明対象としてきたような様々な意味的関係（否定、モダリティ、テンス、条件文、照応、前提、慣習的含み等（†後述））を体系的に扱える見通しは今のところ得られていない。

人間は、自然言語の文を与えられれば、その意味を理解し、意識することができるが、自らが文を理解する過程を意識しているわけではない。したがって「文を理解する」ということがそもそも何を意味するのかは、実は言語処理研究者にとっても自明ではない。この問題に、分析的な手法を提供するのが理論言語学なのである。

理論言語学の側では、自然言語処理と袂を分かってから現在に至るまで、いくつかの概念的進展があった。1) 形式統語論の理論的基盤：形式統語論と論理学の、特に証明論との間に豊かな関係性(Ono 1990)が発見され、チョムスキーの生成文法よりも言語の普遍的な制約を自然に捉えた枠組みである「範疇文法」の研究が進んだ。特に、組み合わせ範疇文法(Combinatory Categorial Grammar (CCG): Steedman 1996)の登場によって、生成文法と自然言語処理の共通の大問題であった等位接続構文の問題が解消した。2) 形式統語論の経験的基盤：生成文法におけるデータと検証手法の再解釈が行われ、内省による言語学を厳密科学として推進するための基盤が整った(Hoji 2015)。3) 依存型理論と証明支援系の登場：依存型理論(dependent type theory (DTT): Martin-Löf 1984)は構成的数学の基礎理論として知られていたが、その計算的性質の理解が進み、Coq等、依存型理論に基づく証明支援系/定理証明器が登場した。

このような背景を踏まえて、本研究は自然言語のシンタクスと意味の構造を解明する理論の構築を目標としつつ、それによって「人間の言葉を理解する人工知能」の実現を目指す。そのような理論は、(A) 統語論 (B) 意味論・語用論 (C) 実装、の三部門に分かれ、(A)(B)の理論は言語現象に対する網羅性、計算機に実装可能な高い形式性、計算的効率を併せ持つものでなければならない。

統語部門については、組み合わせ範疇文法と高階動的論理に基づく形式日本語文法を完成させ、2010年に書籍「日本語文法の形式理論－活用体系・統語構造・意味合成－」（くろしお出版）として出版した。この理論は、「日本語の言語現象に対する網羅性」「計算機で扱うのに充分な形式的厳密性」「活用体系・統語構造・意味合成にわたる理論的統合性」を同時に満たす「日本語文法史において類を見ない研究」として評価されている。また組み合わせ範疇文法の理論的研究、組み合わせ範疇文法による日本語のかきまぜ現象の分析、敬語の分析等の研究も行っている。

意味計算部門については、依存型理論を用いた談話意味論である依存型意味論(Dependent Type Semantics: DTS)を2014年に発表した。また、DTSの理論を理解するのに必要な背景知識を学べる教科書として、2012年に教科書「数理論理学」（東京大学出版会）を出版している。DTSは言語学において主流である（タルスキ、ディヴィッドソン、モンタギュー由来の）モデル理論的意味論とは異なり（ゲンツェン、プラヴィッツ、ダメット由来の）証明論的意味論に基づく意味の理論である。特に「照応解決・前提束縛」の現象は、一階述語論理では表現できないことが知られているが、DTSはこれを関数型プログラミングで発展した一般的な手法（型検査・型推論）を用いて計算できる点が特長である。またDTSは（†）で挙げたような、自然言語の意味現象の全体を記述することが可能な理論であり、これまで、一階述語論理では表現できない量化である「一般化量化子」、モダリティを伴う照応・前提、叙実述語、照応解決の難題である「橋渡し推論」「コアーション」等の現象の分析において成果を挙げている。またDTS以外の意味論的枠組みについても、圏論的意味論、限定継続、等の研究を行っている。

語用論計算部門についても、たとえば「慣習的含み」は含意・前提とは異なる推論パターンを示す現象であるが、証明論的意味論の観点からの分析によって、先行研究が未解決であった意味合成の問題を解決できることを示した。これは我々が研究分担者をつとめた科学研究費補助金基盤研究(C) "Computational semantics and pragmatics of politeness phenomena"（研究代表者：Eric McCready教授）の成果である。

実装部門については、自然言語の複数の文に対して、頑健なCCGパーザの出力から形式意味論に基づいて高階論理表示の意味合成を行い、定理証明器Coqによる自動推論を行う推論システム"ccg2lambda"を構築した。これは、主たる共同研究者を務める「知識に基づく構造的言語処理の確立と知識インフラの構築」プロジェクト（平成25年度－30年度, 研究代表者：黒橋禎夫教授，戦略的創造研究推進事業(CREST)「ビッグデータ統合利活用のための次世代基盤技術の創出・体系化」領域）の成果であり、お茶の水女子大学戸次研究室のメンバーとの共同研究である（右記URLで公開：https://github.com/mynlp/ccg2lambda）。検証はFraCaSテストセット(Cooper et al. 1996)によって行い、一階述語論理に基づく最先端の推論システム(Nutcracker, Bos et al.2008)の正解率50％に対して、69％の正解率を達成した。

形式意味論とは何か

形式意味論とは，自然言語の意味を対象とする自然科学である．理論言語学の意味部門であり，典型的には以下の構成をとる．

  1. 自然言語の意味とは何か，という問題について何らかの立場を採り，意味を表示するための形式言語を定義する．
  2. 自然言語の統語論について，何らかの立場を採る．
  3. 与えられた言語の与えられた文もしくは談話について，2. の統語論が与える構造にしたがって，1. による意味表示を計算する機構を与える．
  4. その言語の個々の文または談話について，3. によって予測される意味と，母語話者の言語直観とを照合することにより経験的検証を行う．誤りは1.2.3. に遡り（通常は3. を）修正する．

形式意味論の研究は，R.Montague の1970 年代前半の一連の論文をもって嚆矢とする[39]．一般にはモンタギュー文法の名で知られ，その登場は，1940年代から1960 年代にかけての計算機科学・理論言語学・論理学・言語哲学のさまざまな動きを背景としている．第一に，1930 年代以降のA.Turing,A.Church, H.Curry らによる理論計算機科学の発展により，型付きラムダ計算が登場したこと，第二に，1950 年代に始まるN.Chomsky の生成文法によって，普遍文法の概念や，「自然科学としての理論言語学」というパラダイムが提示されたこと，第三に，N.Chomsky がもたらした形式言語理論の発展によって，J.Lambek らが（1930 年代にK.Ajdukiewicz によって考案された）範疇文法を，自然言語の統語理論として蘇らせたこと，第四にC.I.Lewis による様相論理にS.Kripke がクリプキ意味論を与えたことで様相論理のモデル理論的意味論が確立し，計算機科学や言語哲学において広く用いられ始めたこと，第五に，D.Davidson による自然言語の真理条件的意味論が登場していたこと，である．

モンタギュー文法は，1. についてはD.Davidsonの真理条件的意味論の立場を取り，「文の意味」とは「文の真理条件」であるとした．これは現在に至るまで形式意味論の標準的立場である．また，内包論理という，高階様相論理と型付きラムダ計算を融合させた独自の論理体系を定義し，そのモデル理論によって，各論理式に真理条件を与えた．2. の統語論については独自の範疇文法を設計し，英語の断片についてカバーする（モンタギューの理論がモンタギュー文法と呼ばれた理由である）とともに，3. についてはその断片の各語に内包論理による表示を与える辞書，および，範疇文法の各規則に並行する意味合成規則が定められている．これによって，範疇文法の生成する任意の文について，内包論理による意味表示を計算することができる．4. については，言語哲学の伝統的問題であった量化子のスコープ曖昧性，およびde re/de dicto 読みの問題を，統一的に解決することに成功している．

モンタギュー文法には，それまでの言語哲学にはみられない特徴が二つあり，その後の形式意味論研究を方向付けている．第一に，統語論の与える構造から意味表示に至る対応付けの過程を明示したことである．モンタギューの定式化においては，統語規則の適用に並行して意味合成規則が適用されるという点で，統語論と意味論の間に強い対応関係があり，これは語彙化文法，あるいは語彙主義と呼ばれる立場の草分けである．技術的には，内包論理の語彙化を可能にしたのは型付きラムダ計算との融合である．ただし，語彙化は形式意味論にとって必須の要請というわけではなく「統語論の与える構造から意味表示に至る対応付け」の一つの方法に過ぎない．そのような対応付けの存在が，形式意味論をそれまでの言語哲学と区別するのである．

モンタギュー以前の言語哲学においては，論理表示によって文の意味の分析を行う際に，文に対して論理表示を対応付けるための理論は与えられていなかった．ところが，これは言語哲学の分析が，未知の文に対しては予測をもたらさないことを意味する．一方，モンタギュー文法では（範疇文法がカバーする英語の断片に含まれる）任意の文について真理条件を予測することができる．結果的に，この特徴は意味論の研究に反証可能性をもたらす．反証可能性は，経験データの再現性と併せて，かつてC.Popper が自然科学と疑似科学を区別する基準として挙げたものである[43]．しかし，形式意味論にみられるこのような自然科学的態度は，同時代に発達した生成文法がもたらした文化とみることもできる．

モンタギュー文法の第二の特徴は，非古典論理の採用である．論理学においては証明論とモデル理論の発展により，古典論理が暗黙に仮定していた構造（二値性，二重否定律，構造規則等）が明らかになり，それに伴って，それらの構造の一部あるいは全部を持たない論理体系の性質が緻密に調べられるようになった．J.-Y.Girard による線形論理，J.Lambek のランベック計算はその一例である．そのような論理体系の存在意義は，20 世紀前半まではあまり認識されていなかったが，計算機科学が論理学を相対化した20 世紀後半において，論理学の主要テーマの一つとなった．古典論理はもはや「唯一の」論理ではなく，分析の対象に合わせて新たな論理体系を設計しても良い，という意識が醸成された．また「計算」という概念が新たに論理学の分析対象となったことにより，自然言語の意味の計算過程も，相対化された論理学の分析対象となった．このような意味において，形式意味論の理解には現代的な論理学の理解が必須である．

これらの新しい特徴の一方で，モンタギュー文法は，「理論の形式化によって，新たな言語現象の発見が促される」という，論理学に基づく言語哲学の特徴をより顕著に受け継いでいる．モンタギュー文法はその形式的厳密さと反証可能性ゆえに，モンタギュー文法では扱うことのできない言語現象の発見を促したのである．その中には，一般化量化子，モダリティ，前提，総称，種，複数性，等位接続，イベント，疑問文，フォーカス，条件文，選言などの多様な現象が含まれる．形式意味論の発展に伴い，これらの現象にまつわる問題が認識され，またそれらの相互作用から生じる問題についても認識されるに至った．詳しくは[44][30] 等を参照されたい．そしてそれらの問題に対して，形式意味論では非古典論理の精神に従って，新たな論理体系を設計することによる解決を試みてきた．

そこから生まれた一つの流れは，H.Kamp, I.Heimらによる談話表示理論[27][24] である．モンタギュー文法では単文の意味のみが対象であったが，文間の照応およびテンス等の現象を考慮すると，複数の文からなる談話の意味を分析する必要が生じた．また，P.Geach の著作[20] によって知られるロバ文の問題のように，単文内の照応であるにも関わらず，複文間の照応と並行する構造をもつものも指摘されていた．初期のDRT では，談話表示構造という一階述語論理の存在量化の構造を大きく変更した表示言語を導入し，照応の動的側面を捉えようとした．1990 年代に入り，J.Groenendijk, M.Stokhof らによる動的意味論[22] が登場する．動的意味論は，DRT の意味表示を得る手続きが合成的ではないという問題を解決する体系であり，プログラミングにおける副作用を捉えるための様相論理である動的論理を自然言語の意味論に転用したものである．しかし，その後のDRT の度重なる修正によって，両者は一つの理論へと収束していく．その流れのなかで，R.van der Sandt, R.Geurts らによって前提と照応の統一理論が提示され[54]，またN.Asher らのsegmented DRT(SDRT[2]) によって談話理論がDRT と統一されるなど，形式意味論の分析は1990年代から2000 年代前半にかけて大きな進展をみせた．

もう一つの大きな流れは，B.Partee, I.Heim らによる，生成文法との融合である[26]．R.Montague の範疇文法は英語の一断片しかカバーできず，形式意味論研究には本格的な統語部門が必要であった．一方，N.Chomsky らによる生成文法は，1980 年代に言語の意味に関わる議論を切り捨てるという選択肢を取り，意味論は説明の対象外となっていた．したがって，モンタギュー文法から統語部門を除いたものを，生成文法と融合するというのは自然な要求であった．この頃から，モンタギュー文法はモンタギュー意味論と呼ばれるようになる．

生成文法との融合は，論理学の基礎をもたない言語学者が形式意味論の分野に参入するきっかけとなった．このことは，論理的表示を，言語現象を記述するための道具として用いる立場を生むことになり，これまで述べてきたような「自然科学としての意味論」と「記述言語に論理表示を用いる記述的意味論」が混在する状況をもたらした．現在の形式意味論は，形式意味論以外の言語学，論理学，言語哲学，自然言語処理などから多様な人材が出入りする学際領域であり，冒頭の1.～4. のいずれを重視（あるいは軽視）するかによって様々な形態の研究が存在している．

また，理論構築に用いられる手法もあらゆる論理体系に拡大しているが，論理学をベースとすること自体はそもそも形式意味論にとって必須の要求ではないこともあり，確率モデル，圏論，関数型プログラミングなど，あらゆる数理モデルが用いられ始めている．扱われるテーマも，伝統的な意味論の問題に加えて，認知意味論，語彙意味論などが形式意味論へのアンチテーゼとして提唱してきた多義，メタファーなどの言語現象も裾野に含まれつつある．さらには自然言語処理における計算意味論，意味処理との相互作用もあり，形式意味論の外延を定めることは次第に難しくなりつつある．

また，本稿で触れなかった立場として，主辞駆動句構造文法の意味部門として生まれたMinimal Recursion Semantics (MRS[12]) のような体系も存在するが，ここでは詳しくは論じない．

（初出：戸次大介 (2017)「形式意味論」, 人工知能学事典, 人工知能学会.）

意味論の証明論的転回

Montague以来、自然言語の意味論における主流はモデル理論的意味論であり、文の意味とはその真理条件(truth-condition)であるとされてきた。一方で1980年代にはEタイプ照応[16]や（意味論的）前提[25]といった一階述語論理やMontagueの内包論理では説明できない現象が知られるようになり、談話表示理論(DRT: Discourse Representation Theory [27]）やファイル変更意味論(FCS: File Change Semantics [24])の登場を動機付けた。1990年代には、動的述語論理(DPL: Dynamic Predicate Logic [22])が提案され、文の意味をその真理条件ではなく、CCP (context change potential)として捉え直す試みがなされ始めた。また、Eタイプ照応と（意味論的）前提のDRTによる統一理論が[54]によって提示され、CCPのような動的な意味の捉え方が自然言語にとって本質的である、という見解が受容されつつ、2000年代以降に至っているように見受けられる。

言語哲学の末裔である形式意味論から生じたこれらの流れで興味深いのは、照応や（意味論的）前提といった（普遍的現象であるとはいえ）特定の言語現象の分析が、言語哲学の問題である「言語の意味とは何であるか」という問いに対して、特定の立場（真理条件的意味論）を棄却することを要請していることである。しかしながら、その代替案たるCCPの受容が、照応や（意味論的）前提といった言語現象が要請する唯一の結論であるか否かについては、より慎重に検討されなければならない。

その点において、自然言語の意味論に真理条件的意味論とは異なる流れが存在していることには、より多くの関心が寄せられるべきである。それは、Sundholm, Ranta, Cooper, Luoらによる証明論的意味論の流れである。 依存型理論に基づいた自然言語の意味の研究としては、[49][47][11][32]等が知られている。依存型理論以外の体系に基づく自然言語の証明論的意味論には[18][19]等があり、また依存型理論を用いた自然言語のモデル理論的意味論には[23]等があるが、これらとの比較については別の機会に述べたい。

モデル理論的意味論が、文の意味を真理条件とする立場であるのに対し、証明論的意味論とは、文の意味を検証条件とする立場[14][15]に由来する。真理条件的意味論は、Tarskiによる数学の意味論にその起源を持つが、検証条件的意味論は[21][46]らによる数学の意味論に遡る。

特に、理論装置としてMartin-Löfの依存型理論[35]を用いた場合は「証明」を表す式を論理式の中で用いることが可能となり、これは形式意味論の分野において動的意味論を導入する動機となったEタイプ照応や（意味論的）前提といった現象に、まったく別の説明を与えることができるのである。

また、筆者らの近年の研究（[5][8][7]を参照。）において、Rantaらの証明論的意味論を合成的意味論として再構成できることが示され、動的意味論に対して経験的、計算的に優位であることも明らかにされつつある。意味論におけるこのような近年の展開を「証明論的転回」と呼ぶことにする。

形式意味論の証明論的転回

依存型理論は、Martin-Löfによって構成的数学の基礎をなす論理体系として考案され、数度の改訂を経て[40]による現在の体系に至っている。

ラムダ計算・型理論の標準的教科書の1冊である[3]においては、依存型理論のうち型構成子をΠに制限した体系λPがいわゆるλキューブを構成する体系の一つとして解説されている。また、依存型理論では証明支援系Coq[13]の基礎理論でもある。

依存型理論がはじめて自然言語の意味論に用いられたのは、[49]においてであり、いわゆるロバ文[20]に適切な意味表示を与えうる可能性が示された。続いて[1]においてDRTの意味表示(DRS)から依存型理論の型への変換が可能であることが示された。

依存型を用いた本格的な自然言語の意味の理論は[47]によるType-Theoretical Grammar (TTG)を待つことになる。ここでは、ロバ文を始めとして、さまざまな照応現象、（意味論的）前提の一部、テンスやモダリティに至る言語現象が依存型を用いてうまく表示されうることが示され、依存型による意味理論の一つのランドマークとして知られる。

その後、[11]によるType Theory with Record (TTR)や、[31][32]によるCoercionの研究は、依存型理論のうち照応・（意味論的）前提以外の拡張可能性に着目し、可能性の裾野を広げている。

依存型意味論(DTS)

TTGはそれまでの研究と比較して、より広範囲な言語現象に依存型理論による分析を与え、依存型理論による自然言語の意味論の可能性を示したといえるが、合成原理(principle of compositionality)を満たしていないという点において、形式意味論の理論としての基準を満たしていないものであった。この点を修正しようとする試みとして、[42]によるMontague文法とTTGの融合があるが、このアプローチの問題点については[5]を参照されたい。

依存型意味論(dependent type semantics: DTS [5][8][7])は依存型理論に未指定項(underspecified term)と呼ばれる構文を追加することで、TTGなど依存型理論に基づく自然言語の意味論を、合成原理を満たす体系として再構築したものである。

DTSによる分析の例として、Eタイプ照応の例 A man entered. He whistled.を考える。統語理論には、ここでは統語計算の過程を明示するために組み合わせ範疇文法[48]を仮定するが、意味部門としてのDTSは統語部門としてのCCGに依存しておらず、語彙化文法であればどのような理論を仮定しても構わない。

一文目と二文目の統語構造および意味合成過程は以下の通りである。DTSでは自然言語の意味表示を見やすくするために、依存型に一部独自の記号を用いる。詳しくは[7]を参照されたい。最下段には、それぞれの文の意味表示が現れており、これらはΣ型を用いて（連言として）接続し、一文目、二文目を合わせた談話の意味表示となる。

ここで@記号は未指定項@_iA（ただしi∈{N}は異なる未指定項を区別するための指標、Aは型）を構成するために用いられる。未指定項のための規則は@規則と呼ばれ、「Aが型であり、かつ型Aに何らかの証明項が存在するとき、@_iAをA型の項として用いることができる」という意味を与える。直観的には、これは「Aであるような項」として用いる。

この意味表示に含まれる照応詞の先行詞を解決するには、型検査を行う。依存型理論には、決定可能な型検査アルゴリズムをもつ断片が存在しており、自然言語の意味表示はその断片を用いて記述することができる。詳細は[9]を参照されたい。

冒頭で述べたように、依存型理論を用いた自然言語の意味の分析はいくつか存在するが、DTSの特長は合成原理を満たすという点にある。この特長によりDTSでは、Montague意味論と同じように、これまで形式意味論で論じられてきた幅広い言語現象を分析することができる。

[54]は照応と（意味論的）前提が同質の現象であることを指摘し、DRTに基づく統一理論を提示したが、[7]ではそれの証明論版ともいえる分析を展開することが可能であることを示した。加えて[6]では、慣習的含み(conventional implicature: CI [45])について、従来の（意味論的）前提と表示の次元を区別する立場ではなく、同一の次元で表示する分析を提案している。

また、DTSによって捉えうる現象の射程は、一階述語論理を越えるとされる言語現象にまで広がっている。たとえば[51]では一般化量化子(Generalized Quantifier; GQ [4])について、[52]では叙実的前提(factive presupposition)について、それぞれ分析を行っている。前者については[50]において依存型理論を用いた分析が提案されているが、ロバ文のstrong/weak readingsの導出については問題点が残るとし、その修正案について議論している。後者についてはDRTでの分析が難しいことが知られている。

さらに、[53]では複数性(plurality)の扱いについて、特に一般化量化子が複数形照応詞の先行詞となる場合について論じている。[28]では述語の選択制限を一種の（意味論的）前提と見なす立場に立ち、DTSを用いた分析を与えている。

言語処理の証明論的転回

自然言語の意味論と、自然言語処理における意味処理に共通して求められる要請の一つに、任意の文が伝える意味を過不足なく表現し、それらの間の含意関係を正確に抽出することが挙げられる。そのためには、言明間あるいは言明と実世界の関係を規定するモダリティ、前提・含意、時制などの意味的関係を正確に表現する意味表現が必要である。

「自然言語の意味に関わる情報のかなりの部分が、一階述語論理の記述力の範囲では表現できない」という事実は、Montague意味論の初期の研究において指摘されて以来、幾度となく議論されてきた。それ以降の形式意味論は、高階論理であるMontagueの内包論理(Intensional Logic: IL)を拡張する形で進展しており、高階論理を用いることがほぼ通例である。

一方、Montague自身の意味論が内包論理の証明論とともに提示された(Montague, 1970)のに対し、その後の形式意味論においてはモデル理論のみが受け継がれて主流となった。そのことは、形式意味論を用いた意味の分析が、「計算」という側面においてどのように振る舞うかを不透明にしたきらいがある。

同時に、高階論理による意味表示は、これまで計算面では「一階述語論理による意味表示に対して不利である」と信じられてきた。しかし、著者らの近年の研究によって、この点には再考の余地があることが明らかになりつつある。

Mineshima et al. (2015)[36], Martinez-Gomez et al. (2016)[34]では、組合せ範疇文法に基づく頑健な構文解析（C&Cパーザ (Clark and Curran 2007)[10]）と、様々な意味的現象に対して推論・証明手続きを与える高階論理による意味論を接続することにより、実世界の大規模テキストに対して頑健かつ高速に意味計算を行う含意関係認識システムccg2lambdaを開発した。ccg2lambdaはgithub上で公開されている：https://github.com/mynlp/ccg2lambda

ccg2lambdaでは、自然言語文の構文解析木を得たのち、λ計算に基づいて高階論理の意味表示を計算し、定理証明器Coqによる自動推論を行う。検証はFraCaSテストセット (Cooper et al. 1994)[17]によって行っており、一階述語論理に基づく推論システムとして2015年当時最高であったNutcrackerの正解率50％に対して、69％の正解率を達成した。また、それまで高階論理による推論は速度の点で非効率であると考えられていたが、Mineshima et al. (2015)[36]では機能語に対する80個の語彙項目、内容語に対する57個の語彙テンプレート、および（一般化量化子や内包性を含む）高階の公理群を用いて、Nutcrackerの速度11.23秒/問に対して速度3.72秒/問を達成している。

Mineshima et al. (2016)[38]では、Jigg (Noji and Miyao 2016)[41]に付属の日本語CCGパーザに対しても同様の高階論理による意味合成・含意関係認識システムの構築を行い、JSeMテストセット (Kawazoe et al. 2015)[29]を用いて日本語含意関係認識の評価を行った。一般化量化子など複雑な言語現象を伴う推論課題523問に対して、速度3.58秒/問で正解率75％を達成した。このようにccg2lambdaの性能は、英語用・日本語用ともに含意関係認識器のstate-of-the-artに匹敵するものである。

さらに Martinez-Gomez et al. (2017)[37]では、ccg2lambdaの推論において語彙的知識が必要になった際に、WordNetやword2vecを用いて、動的に公理を生成する技術を提案した。分散表現の合成的意味論の評価のために構築されたSICKデータセット (Marelli et al. 2014)[33]を用いて含意関係認識タスクの評価実験を行った結果、従来の一階述語論理や自然論理に基づくシステムの性能を上回る正解率(83％)を達成している。

これらの研究は、高階論理が自然言語の含意関係認識の計算において、記述面のみならず、速度面においてもむしろ有利となりうることを示しており、意味処理においてどのような表現形式が妥当であるか、という問題に対して一石を投じるものである。たとえば、高階論理による意味表示は、自然言語の意味のうち一階述語論理を越えた記述力を要求する（典型的には一般化量化子やモダリティが関わる）情報に対して、性質の良い「圧縮」を与えていることを示唆している。すなわち、これらの情報が頻繁に要求する証明過程に短い計算過程を割り当てることによって、一階述語論理によって書き下した意味表示が冗長な、そしてより強力な計算リソースを要求するのに比して、効率的な計算を可能とする、ということである。

（初出：戸次・峯島・金子・田中・谷中・木下・伊藤・簗 (2017)「意味論の証明論的転回」, 第31回人工知能学会全国大会論文集, 2B3-OS-07a-4.）

参考文献
  1. Ahn, René and Kolb, Hans-Peter (1990). Discourse Representation meets Constructive Mathematics. Papers from the Second Symposium on Logic and Language.
  2. Asher, Nicholas and Lascarides, Alex (2003). Logics of Conversation. Cambridge University Press.
  3. Barendregt, Henk P. (1992). Lambda Calculi with Types. Handbook of Logic in Computer Science.
  4. Barwise, Jon and Cooper, Robin (1981). Generalized Quantifiers and Natural Language. Linguistics and Philosophy.
  5. Bekki, Daisuke (2014). Representing Anaphora with Dependent Types. Logical Aspects of Computational Linguistics (LACL 2014), LNCS 8535.
  6. Bekki, Daisuke and McCready, Eric (2015). CI via DTS. New Frontiers in Artificial Intelligence (JSAI-isAI 2014 Workshops).
  7. Bekki, Daisuke and Mineshima, Koji (2017). Context-Passing and Underspecification in Dependent Type Semantics. Modern Perspectives in Type-Theoretical Semantics.
  8. Bekki, Daisuke and Mineshima, Koji (2016). Dependent Type Semantics: An Introduction. ESSLLI 2016 Lecture Notes.
  9. Bekki, Daisuke and Sato, Miho (2015). Calculating Projections via Type Checking. TYpe Theory and LExical Semantics (TYTLES), ESSLLI 2015 Workshop.
  10. Clark, Stephen and Curran, James R. (2007). Wide-coverage efficient statistical parsing with CCG and log-linear models. Computational Linguistics.
  11. Cooper, Robin (2005). Records and Record Types in Semantic Theory. Journal of Logic and Computation.
  12. Copestake, Ann and Flickinger, Dan and Pollard, Carl J. and Sag, Ivan A. (2006). Minimal Recursion Semantics: An Introduction. Research on Language and Computation.
  13. Coquand, Thierry and Huet, Gérard (1988). The Calculus of Constructions. Information and Computation.
  14. Dummett, Michael (1975). What is a Theory of Meaning?. Mind and Language.
  15. Dummett, Michael (1976). What is a Theory of Meaning? (II). Truth and Meaning.
  16. Evans, Gareth (1980). Pronouns. Linguistic Inquiry.
  17. Cooper, R. et al. (1994). FraCaS: A Framework for Computational Semantics. FraCaS Technical Report.
  18. Francez, Nissim and Dyckhoff, Roy (2010). Proof-theoretic semantics for a natural language fragment. Linguistics and Philosophy.
  19. Francez, Nissim (2015). Proof-Theoretic Semantics. College Publications.
  20. Geach, Peter (1962). Reference and Generality. Cornell University Press.
  21. Gentzen, Gerhard (1935). Untersuchungen über das logische Schliessen I, II. Mathematische Zeitschrift.
  22. Groenendijk, Jeroen and Stokhof, Martin (1991). Dynamic Predicate Logic. Linguistics and Philosophy.
  23. Grudzińska, Justyna and Zawadowski, Marek (2014). System with Generalized Quantifiers on Dependent Types for Anaphora. EACL 2014 Workshop on Type Theory and Natural Language Semantics (TTNLS).
  24. Heim, Irene (1983). File Change Semantics and the Familiarity Theory of Definiteness. Meaning, Use and the Interpretation of Language.
  25. Heim, Irene (1983). On the Projection Problem for Presuppositions. West Coast Conference on Formal Linguistics II.
  26. Heim, Irene and Kratzer, Angelika (1998). Semantics in Generative Grammar. Blackwell Publishers.
  27. Kamp, Hans (1981). A Theory of Truth and Semantic Representation. Formal Methods in the Study of Language.
  28. Kinoshita, Eriko and Mineshima, Koji and Bekki, Daisuke (2017). An Analysis of Selectional Restrictions with Dependent Type Semantics. New Frontiers in Artificial Intelligence. JSAI-isAI 2016, LNCS vol. 10247.
  29. Kawazoe, Ai and Tanaka, Ribeka and Mineshima, Koji and Bekki, Daisuke (2015). An Inference Problem Set for Evaluating Semantic Theories and Semantic Processing Systems for Japanese. LENLS 12.
  30. Lappin, Shalom (ed.) (1996). The Handbook of Contemporary Semantic Theory. Blackwell.
  31. Luo, Zhaohui (2010). Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT 20).
  32. Luo, Zhaohui (2012). Formal Semantics in Modern Type Theories with Coercive Subtyping. Linguistics and Philosophy.
  33. Marelli, M. and Menini, S. and Baroni, M. and Bentivogli, L. and Bernardi, R. and Zamparelli, R. (2014). A SICK Cure for the Evaluation of Compositional Distributional Semantic Models. LREC 2014.
  34. Martínez Gómez, Pascual and Mineshima, Koji and Miyao, Yusuke and Bekki, Daisuke (2016). ccg2lambda: A Computational Semantics System. ACL 2016 System Demonstrations.
  35. Martin-Löf, Per (1984). Intuitionistic Type Theory. Bibliopolis.
  36. Mineshima, Koji and Martínez Gómez, Pascual and Miyao, Yusuke and Bekki, Daisuke (2015). Higher-order logical inference with compositional semantics. EMNLP 2015.
  37. Martinez-Gomez, Pascual and Mineshima, Koji and Miyao, Yusuke and Bekki, Daisuke (2017). Injection of Lexical Knowledge for Recognising Textual Entailment. EACL 2017.
  38. Mineshima, Koji and Tanaka, Ribeka and Martinez-Gomez, Pascual and Miyao, Yusuke and Bekki, Daisuke (2016). Building compositional semantics and higher-order inference system for a wide-coverage Japanese CCG parser. EMNLP 2016.
  39. Montague, Richard (1974). Formal Philosophy. Yale University Press.
  40. Nordström, Bengt and Petersson, Kent and Smith, Jan (1990). Programming in Martin-Löf's Type Theory. Oxford University Press.
  41. Noji, Hiroshi and Miyao, Yusuke (2016). Jigg: A Framework for an Easy Natural Language Processing Pipeline. ACL 2016 System Demonstrations.
  42. Dávila-Pérez, Rogelio (1995). Semantics and Parsing in Intuitionistic Categorial Grammar. PhD thesis, University of Essex.
  43. Popper, Karl Raimund (1934). The Logic of Scientific Discovery. Routledge.
  44. Portner, Paul and Partee, Barbara H. (eds.) (2002). Formal Semantics: The Essential Readings. Blackwell.
  45. Potts, Christopher (2005). The Logic of Conventional Implicatures. Oxford University Press.
  46. Prawitz, Dag (1965). Natural Deduction: A Proof-Theoretic Study. Dover Publications.
  47. Ranta, Aarne (1994). Type-Theoretical Grammar. Oxford University Press.
  48. Steedman, Mark (1996). Surface Structure and Interpretation. The MIT Press.
  49. Sundholm, Göran (1986). Proof Theory and Meaning. Handbook of Philosophical Logic.
  50. Sundholm, Göran (1989). Constructive Generalized Quantifiers. Synthese.
  51. Tanaka, Ribeka (2014). A Proof-Theoretic Approach to Generalized Quantifiers in Dependent Type Semantics. ESSLLI 2014 Student Session.
  52. Tanaka, Ribeka and Mineshima, Koji and Bekki, Daisuke (2015). Factivity and Presupposition in Dependent Type Semantics. TYpe Theory and LExical Semantics (TYTLES), ESSLLI 2015 Workshop.
  53. Tanaka, Ribeka and Mineshima, Koji and Bekki, Daisuke (2017). On the Interpretation of Dependent Plural Anaphora in a Dependently-Typed Setting. New Frontiers in Artificial Intelligence. JSAI-isAI 2016, LNCS vol. 10247.
  54. van der Sandt, Rob (1992). Presupposition Projection as Anaphora Resolution. Journal of Semantics.