本稿では理論言語学に基づく自然言語推論システムである言語学的パイプラインを実社会タスクに応用する試みとして，金融テキストを対象としたファクトチェックシステムを提案する．具体的には，自然言語の文を高階論理の意味表現に変換し，自動定理証明を行うことで，顧客アンケートとエキスパートの回答の整合性を検証する．本手法では検証結果として証明図を伴うため，その結果に信頼性を持たせることができる．実験の結果，Accuracyは76.7%に達し，金融テキストを対象とする妥当性の検証手法として本手法の有効性を示した．

人工知能および自然言語処理の分野において，大規模言語モデル(LargeLanguageModels:LLM)の進化は加速の一途を辿っている[1]．LLMの急速な発展に伴い，社会経済や科学研究におけるLLMへの依存度は今後さらに高まると予想される．しかし，実社会への実装が進むにつれて，現在のLLMを組み込んだシステムは二つの本質的な課題に直面している．検証手法の問題LLMによる要約や翻訳，調査結果の正確性を定量的に評価することは極めて困難である．人手による正解データの作成はコストが高く，BLEUやCOMETといった既存の自動評価指標も生成文の論理的妥当性を測るには不十分である．改善手法の問題出力結果に誤りや不満があった場合，ブラックボックスであるLLMに対してど∗本研究は著者が独自に実施したものであり，Amazonの見解や立場を反映するものではない．のように修正を適用し，精度低下をモニタリングすべきかという解決策は非自明である．これらの問題は，LLMの推論過程が不透明であることに起因しており，LLM同士による相互評価や内部表現分析といったアプローチも，評価者がLLMである以上，循環論法に陥る危険性を孕んでいる．これに対し，自然言語理解の言語学的研究には，形式統語論や形式意味論，数理論理学に基づき長年研究されてきた「意味の理論」の蓄積がある．特に2000年代中盤以降，これら理論言語学の知見を実装した「言語学的パイプライン」は著しい進展を遂げている．言語学的パイプラインは，人間の言語機能の分析や意味原理に基づいて推論を行うため，計算履歴がそのまま言語理論による説明となり反証可能性を持つ，というLLMにはない特徴を有する．本研究では，この「説明可能な」言語学的パイプラインを実社会タスクに応用する試みとして，金融テキストを対象としたファクトチェックに取り組んだ．高度な専門知識と論理的整合性が求められる実務において，LLMのみを用いたアプローチではハルシネーションや論理矛盾のリスクが払拭できない．そこで本研究では，対象文書を言語学的パイプラインによって高階論理の意味表現へ変換し，整合性や矛盾を自動検出する手法を提案する．本手法では，整合性が確認された場合には「証明図」が出力され，判定結果に高い信憑性が与えられる．本論文では，このLLMと言語学的パイプラインの協働によるファクトチェックシステムの構築手法と，その有効性と課題について論じる．Thisworkispublishedwithoutpeerreviewandislicensedbytheauthor(s)underCCBY4.0(https://creativecommons.org/licenses/by/4.0/).org/licenses/by/4.0/).の間に含意関係があればyes，矛盾関係があればno，どちらでもなければunknown，型検査に失敗し証明探索が行われない場合はotherと判定する．1≦푘≦푛，Γ′≡푆1:푀1,...,푆푘−1:푀푘−1，Γ≡푆1:푀1,...,푆푛−1:푀푛−1とする．方法も指定するため，構文解析の結果をもとにDTSに基づく意味合成を行うことが可能である．また，lightblueには型検査という解析結果の整合性を保証するための機能がある．具体的には，DTSの文の意味の型はtypeでなければならないという制約を満たしているかを検査する．さらに，文푆푘の意味を表す意味表示푀푘の中に，聞き手にとって未知の意味を記述する演算子である未指定項(underspecifiedterm)が含まれている場合には，型検査を行う際に自動定理証明器waniを呼び出し，先行詞を探索する照応解決も同時に行われる．入力されたすべての文が型検査に成功したら，含意関係を判定するために自動定理証明器waniによる証明探索が行われる．DTSでは文の意味は型で記述されるが，カリー＝ハワード対応により，型理論における環境・項・型はそれぞれ証明論における前提・証明・帰結と対応するため，前提文푆1,...,푆푛−1のもとで仮説文푆푛が成り立つか，つまり前提文と仮説文の間に含意関係が成り立つかを判定することは前提文푆1:푀1,...,푆푛−1:푀푛−1のもとで命題푀푛を持つ証明퐻を探索することに帰結する．また，前提文と仮説文の矛盾関係を検知するには，命題¬푀푛を持つ証明퐻を探索する．この推論システムには大きく分けて統語・意味解析，型検査，証明探索の3つの工程があり，それぞれの工程の計算過程を表すCCG統語構造，DTS意味表示，型検査図，証明探索図および含意関係の判定結果を出力する．これにより，LLMを用いた推論ではブラックボックスとなってしまう推論過程を追うことが可能となる．また，証明探索により含意関係の判定を行う際には，与えられた前提からは何が言えるのか・証明したい命題が真であるためには何が必要なのかを探索するため，証明を構築する上で判定の根拠は前提のどの部分であるかという説明を伴うという特徴もある．3.2データセットデータセットは，資産運用や金融商品投資への考えを問う，アンケートの自由記述と，エキスパートによる回答のペアデータ200件を母集団とした．そこから，機微情報（個人を特定し得る情報や特定の機関・商品、秘匿性の高い情報）が含まれないデータのみを対象とし，かつ，顧客の意図や求める支援内容，対応方針が実質的に同一なものを重複として省き，20件を選定した．アンケート文および回答文に複数文構成や表現揺れが含まれるため，LLMを用いて表現を正規化した．具体的には，文を1文に整形し，主語の省略や語彙の揺れ（同義語・言い換え）を統一することで，後続の論理表現や比較が可能な文へ変換した．この正規化後のアンケート文をA，正規化後の回答をDと定義した．さらに，AとDだけでは含意関係の分析に必要な要素が不足するため，補助的なデータを付与した．顧客が期待する支援内容については，別途整備された「個人が期待する支援リスト」から該当する項目を人手で選択し，これをBとした．同様に，業務上提供可能な対応手段については，「提供手段リスト」から該当する手段を人手で選択し，これをCとした．いずれも，自由記述を直接ラベル化するのではなく，定義済みリストの中から最も適合する項目を選ぶ運用とすることで，付与基準の一貫性を確保した．ただし，A・B・Cだけでは，Dが一意に導かれるとは限らない．そこで，A・B・CからDへ至る推論を可能にするための追加知識を明示的に導入する．具体的には，推論の中間段階を表す条件文をEとし，提供手段(C)と中間段階(E)が満たされるとorg/licenses/by/4.0/).最終行為(D)が導かれる条件文をFとしてLLMにより生成した．以上により，各事例をA〜Fの6要素（各1文）で表現した30組のデータセットを構築した．いずれも正解ラベルはyes（含意）とする．lightblueはサ行変格活用動詞を含む文の解析に課題が残されており，本稿では構築したデータセットについて，サ行変格活用動詞が含まれる場合は，サ行変格活用動詞ではない類似の語に置き換えて使用した（例：作成する→作る）．3.3推論の構造§3.1.3で紹介した言語学的パイプラインを用いて，金融テキストを対象としたファクトチェックを試みる．推論の構造は図2の通りである．前提文として「A.顧客アンケート」「B.個人が期待する支援」「C.金融機関の提供手段」を，公理として世界知識である「E.金融機関の対応方針1」「F.金融機関の対応方針2」を与えた際に，仮説文である「D.エキスパートの回答」を含意しているか判定する．金融機関の方針1はある状態の顧客に対する金融機関がとるべき対応、金融機関の方針2は金融機関の対応や手段を言い換える公理である．含意関係が認められた際には，エキスパートによる回答は，顧客アンケートの内容に対して金融機関の提供手段や対応方針に沿った妥当な対応案であるとする．またDTSでは「かつ」は単純型付き휆計算の直積型퐴×퐵の一般化であるΣ型，「ならば」は関数型퐴→퐵の一般化であるΠ型によって表現される．3）つまり「휙かつ휓ならば휒」は（휙×휓）→휒と表現されるが，（휙×휓）→휒⇔휙→(휓→휒)であることより，本稿ではEおよびFは휙→(휓→휒)として実装した．3）Σ型は푥:퐴퐵，Π型は(푥:퐴)→퐵と表記する．4結果本システムでは統語・意味解析や照応解決の曖昧性を加味して複数の解析結果を出力するが，本稿では最上位の解析結果のみを分析の対象として実験を行った．全30題のうち，A〜Fの全ての文で型検査に成功したのは28題だった．28題について証明探索を行った結果，含意関係が認められると判定されたのは23題(76.7%)であった．含意関係が認められた問題の例は以下の通りである．【A】顧客は目標に届くか不安だ。【B】顧客は進み具合が分かると安心する。【C】金融機関は進捗メモを作る。【D】金融機関は半年に1回進捗メモを顧客に送る。【E】顧客は目標に届くか不安かつ進み具合が分かると安心するならば、金融機関は進み具合を知らせる。【F】金融機関は進み具合を知らせるかつ進捗メモを作成するならば、半年に1回進捗メモを顧客に送る。推論が不正解だった5問は，いずれも妥当な統語・意味解析および型検査が行われており，証明が見つかる（含意関係が認められる）ことが望ましい．これはwaniの証明探索に起因するエラーである．型検査に失敗した2問は，いずれも時制(tense)に関する統語・意味解析にエラーの原因があり，これの改善により妥当な推論が可能になると考えられる．5おわりに本稿では，言語学的パイプラインに基づく推論システムを金融テキストのファクトチェックに応用する手法を提案し，ブラックボックスになりがちなLLM推論とは異なる，説明可能な検証枠組みを実現した．一方で，統語・意味解析におけるtenseの分析，自動定理証明器における証明探索の失敗など，実用化に向けた課題も明らかになった．今後は整合性の判定だけでなく，矛盾関係の判定の検証も行い，実社会における高い信頼度を持つ推論システムの応用可能性をさらに検討していきたい．org/licenses/by/4.0/).