技術要約：ForEx – 論理的誤謬検出における説明可能な推論のための形式検証フレームワーク

1. 問題提起

大規模言語モデル（LLM）による論理的誤謬検出の現在の評価は、主に予測精度（ラベルの正誤）に依存している。しかし、このアプローチでは、モデルが提供する推論が実際に予測されたラベルを支持しているかどうかを検証することができない。正しい予測であっても、真の論理的導出ではなく表層的な相関関係から生じている可能性があり、逆に、誤った予測であっても、特定の解釈の下では形式的に妥当な推論が伴っている場合がある。

さらに、既存の記号的アプローチ（例：NL2FOL）は、通常、充足可能性をチェックするために「入力された議論」を定式化するが、「モデルが生成した推論過程」を定式化するものではない。加えて、標準的なアノテーションの実践では、解釈のバリエーションを単一の「ゴールドラベル」に圧縮してしまうことが多く、議論に対する妥当な代替解釈を覆い隠してしまう可能性がある。予測ラベル、生成された説明、およびそれらの説明の形式的な導出可能性を共同で分析するフレームワークが欠如している。

2. 手法：ForExフレームワーク

著者らは、ForEx（Formal Verification for Explainable Reasoning）を提案する。これは、LLMが生成した自然言語による説明をLean4（形式証明アシスタント）へと翻訳し、翻訳された根拠がエンコードされた前提の下で導出可能であるかを検証するフレームワークである。ワークフローは以下の3つのステージで構成される。

A. 推論候補の生成

「Reasoner（推論器）」モデルは、入力文を受け取り、最大$k$個の候補を生成する。各候補は、以下の要素を含むタプル $(f_i, a_i, s_i)$ である。

• $f_i$: 予測された論理的誤謬の型。
• $a_i$: 自然言語による説明（根拠）。
• $s_i$: 説明を定式化したLean4の構造。

「Modifier（修正器）」は、$s_i$ を初期のLean4コードへと変換する。

B. 実行フィードバックとLean4検証

このステージでは、生成されたLean4コードがコンパイルされることを保証するために、反復的な修復ループを採用する。

1. コンパイル試行: 「Executor（実行器）」は、Lean4コードのコンパイルを試みる。
2. フィードバックループ: コンパイルに失敗した場合（状態F）、Executorはエラーメッセージと元の説明 $a_i$ を受け取り、コードを修正する。
3. 制約: セマンティック・ドリフト（意味の逸脱）を防ぐため、修正は元の説明と初期コードに厳格に制限される。Executorは新しい論理的内容を導入することはできない。
4. 終了: コードが正常にコンパイルされる（状態T）、または最大修復回数（$iter_{max}$）に達するまで、ループは継続される。

C. ラベル整合性評価

本フレームワークは、ラベルの正誤と形式検証のステータスを切り離すために、LLM議論検証マトリックスを導入している。このマトリックスは、2つの軸に基づいて出力を4つの象限に分類する。

1. Lean4検証: 通過（コンパイル成功） vs 失敗（コンパイル不可）。
2. ラベル整合性: 一致（予測が人間によるアノテーションと一致） vs 不一致。

結果として得られる4つのカテゴリは以下の通りである。

• Compilable-Correct (CC): 通過 かつ 一致。
• Compilable-Alternative (CA): 通過 かつ 不一致（人間のアノテーションとは異なるラベルを支持する、形式的に妥当な推論過程を示唆する）。
• Uncompilable-Correct (UC): 失敗 かつ 一致。
• Uncompilable-Incorrect (UI): 失敗 かつ 不一致。

D. コンセンサス誘導型アノテーション・パイプライン

アノテーションの曖昧さに対処するため、著者らは以下のパイプラインを提案する。

1. モデルと人間によるアノテーションを、誤謬カテゴリに関するマルチホットベクトルとして表現する。
2. 主成分分析（PCA）とマハラノビス距離を用いて、外れ値となるモデルを特定し、フィルタリングする。
3. ペアごとのJaccard距離を計算し、「高コンセンサス（合意形成が高い）」な文（不一致が少ないもの）を特定する。
4. 高コンセンサスの文に対し、保持されたモデルの少なくとも50%が形式検証の下で特定のラベルを割り当てている場合、アノテーションを拡張する。

3. 主な貢献

1. ForExフレームワーク: 入力引数ではなく、形式化された推論過程の機械チェック可能な分析を可能にするために、LLM生成の説明をLean4に翻訳する新しいシステム。
2. LLM議論検証マトリックス: ラベルの整合性と形式検証のステータスを分離する指標であり、既存の人間のラベルと矛盾する形式的に導出可能な推論過程を提供するケース（「Compilable-Alternative」カテゴリ）を明らかにする。
3. コンセンサス誘導型アノテーション・パイプライン: 人間の基準、マルチLLMの合意、および形式検証を組み合わせ、アノテーションの不一致をノイズではなく解釈のバリエーションのシグナルとして扱い、コンセンサスに基づく代替ラベルによる保守的なアノテーション拡張をサポートする手法。

4. 実験結果

本フレームワークは、LOGIC-Climateデータセット（1,074インスタンス、13の誤謬カテゴリ）を用い、10%のサンプリングサブセットと15種類の異なるReasonerモデル（思考型および非思考型を含む）を用いて評価された。

• コンパイル成功率: Lean4の平均パス率は、4回の修復イテレーションを経て、初期の**36.70%から98.65%**に上昇した。ほとんどの利得は最初のイテレーションの後に発生した。
• 検証とラベルの一致:
  • Compilable-Correct (CC) + Compilable-Alternative (CA) の合計率は一貫して高く、ほとんどのモデルで**90%を超え、ピーク時には97.59%**に達した。これは、大多数のLLM出力が、形式的な検証を通過する形式的な推論過程に翻訳可能であることを示している。
  • しかし、CC率（人間によるラベルとの一致）は著しく低く、トップモデル間で概ね**17%から23%**の間であった。
  • CA率が支配的であり、これは多くの形式的に検証された推論過程が、人間のアノテーションとは異なるラベルを支持していることを示唆している。
• エラー分析:
  • Uncompilable-Correct (UC) 率（失敗 かつ 一致）は非常に低く（<2%）、この設定においては、検証可能な推論過程なしに正しいラベルが生じることは稀であることを示している。
  • Uncompilable-Incorrect (UI) の失敗は、多くの場合「誤謬なし（No Fallacy: NF）」の予測によるものであり、孤立した単一文章入力におけるコンテキストの欠如に起因する可能性がある。
• アノテーション拡張: コンセンサス誘導型パイプラインは、高コンセンサスの文を特定した。拡張されたアノテーションは、元の人間によるアノテーションに対して0.77のリコールを達成し、元のラベルの大部分を保持しつつ、形式的に支持された代替ラベルを追加した。

5. 意義と主張

本論文は、ForExがLLMの評価を、単純なラベルの正誤を超えて、形式化された推論過程の機械チェック可能な分析へと移行させるものであると主張している。

• 系統的なギャップ: 結果は、形式的な導出可能性とラベルの一致との間の系統的なギャップを露呈させている。「Compilable-Alternative」の出力が頻繁に見られることは、既存の人間のアノテーションが入力の議論に対する妥当な解釈を完全には捉えきれていないか、あるいはモデルが異なる仮定の下で正しく推論していることを示唆している。
• 予測を超えて: 本フレームワークは、モデルが「ゴールド」ラベルとは異なるラベルを支持するとしても、形式的に妥当な（エンコードされた前提の下で導出可能な）推論過程を提供できることを実証している。この区別は、標準的な予測ベースの指標では不可視である。
• アノテーションの有用性: ForExは、単なる検証ツールとしてだけでなく、ダウンストリームのアノテーション分析のためのメカニズムとしても提示されている。それは、ゴールドラベルが不十分なケースや、複数の妥当な解釈が存在するケースを特定し、コンセンサスに基づく代替ラベルによるアノテーションの拡張をサポートする。

著者らは、Lean4による形式検証はエンコードされた前提の下での導出可能性を証明するものであり、元の自然言語文との意味的な整合性を保証するものではないとして、その含意について慎重な姿勢を保っている。自然言語には完全に指定された意味論的基盤が欠けているため、形式化自体が不完全である場合、形式的な結果はモデルの能力を過大評価する可能性があることを認めている。今後の課題として、より豊かな議論構造やコンテキスト情報を組み込むことで、検証結果と意味的な正しさの間の整合性を向上させることが提案されている。