技術要約：LLMによる自動形式化における忠実性のギャップ（The Faithfulness Gap in LLM Autoformalization）

1. 問題定義：忠実性のギャップ

自然言語（NL）の数学を形式的な証明助手（例：Lean 4, Isabelle/HOL）へと翻訳する現代の自動形式化システムは、現在、翻訳の流暢さではなく、**忠実性（faithfulness）**によってボトルネックに直面している。生成された形式的記述は、構文的に正しく（型チェックを通過し）、かつ証明可能であっても、元のNL記述と意味的に異なる内容をエンコードしてしまう可能性がある。

著者らはこれを**忠実性のギャップ（faithfulness gap）**と定義している。コードの場合、ユニットテストが実行可能なオラクル（判定器）として機能するが、数学の形式化においては、NL（暗黙の慣習の下で解釈される）と形式論理（依存型理論の下で解釈される）の間に直接的な架け橋が存在しない。BLEUスコアのような標準的な評価指標（参照文との比較）、専門家によるスポットチェック、あるいは下流の証明器の成功といった指標は、形式化が流暢で証明可能でありながら、意味的に誤っているという「潜行的な」失敗を検出できない。

本論文は、この問題を解釈分布（interpretation distribution） $D_N$ を用いて定式化している。これは、あるNL記述 $N$ を表現していると数学者が認める形式的記述の集合を表す。候補となる形式化 $F$ が $\epsilon$-忠実であるとは、$F$ が $D_N$ に含まれる記述の $1-\epsilon$ に対して証明可能な同値性を持つことを指す。著者らは、意味的なドリフト（乖離）を以下の4つの典型的なクラスに分類している：

1. $\Delta\forall$ (量化子の反転): 量化子の順序の入れ替え（例：$\forall x \exists y$ と $\exists y \forall x$）。
2. $\Delta H$ (仮定の欠落): 前提条件を落とすことで、形式的記述が意図よりも厳密に強くなってしまうこと。
3. $\Delta C$ (結論の一般化): 結論を強化し、$F \Rightarrow N$ は成立するが $N \not\Rightarrow F$ となる状態。
4. $\Delta T$ (型の強制): 型のサイレントな再タグ付け（例：$\mathbb{R} \to \mathbb{Q}$）。これは構文的には検出が最も困難な場合が多い。

2. 手法：双方向証明指紋法（Bidirectional Provability Fingerprinting: BPF）

本研究の中核となる貢献は、候補の「帰結近傍（consequence neighborhoods）」を比較することで忠実性を保証する、リファレンスフリー（参照不要）のフレームワークである**双方向証明指紋法（BPF）**である。

2.1. コアメカニズム

BPFは、「ある記述の意味は、それが何を含意するか、および何がそれを含意するかによって定義される」という洞察に基づいている。

• 前方指紋 ($\Phi^+_F$): 候補 $F$ によって含意されるプローブ（探査項目）の集合。
• 後方指紋 ($\Phi^-_F$): $F$ を含意するプローブの集合。
• 同値性: 2つの記述は、十分に豊かなプローブの集合において、その前方指紋と後方指紋が一致する場合、意味的に同値である。

パイプラインは以下の通りである：

1. プローブ生成: NL記述 $N$ から意味的なプローブ（$P$）を合成する。
2. 自動形式化: これらのプローブを形式的な記述へと変換する。
3. 含意チェック: 証明助手（Lean 4 + mathlib4）をオラクルとして使用し、$F$ とプローブ間の含意関係を計算する。
4. 指紋比較: 候補の指紋を、$N$ から導出された予測指紋と比較する。

2.2. 主要コンポーネント

本フレームワークは、検出能力と効率を高めるために4つの新しいコンポーネントを導入している。

1. 反事実的プローブ生成 (Counterfactual Probe Generation: CPG):
   汎用的なサンプリングではなく、対照的な手順を用いる。CPGは、4つのドリフトクラス（例：量化子の入れ替え）に対して「ドリフトした双子（$N^D$）」を機械的に生成する。その後、LLMに対し、$N$ と $N^D$ を明確に区別できるプローブを生成するようプロンプトを出す。これにより、検定器が検出を目指す特定の失敗モードを標的にする。

2. 等価スペクトラム ($E(F, N)$):
   脆弱な二値判定（忠実/ドリフト）に代わり、$[0, 1]$ の連続的なスコアを用いる。このスコアは専門家の注釈に基づいて較正されており、以下の3つの決定領域を定義する：

   • ACCEPT (受理): $E \ge 0.93$
   • REVIEW (検討): $0.78 \le E < 0.93$ （人間の選別が必要）
   • REJECT (拒絶): $E < 0.78$

3. 適応的プローブ予算配分 (Adaptive Probe Budget Allocation: APBA):
   限られた「タクティク予算（時間/計算コスト）」を動的に割り当てる情報理論的なルーターである。APBAは、一様にサンプリングするのではなく、ドリフト状態に関するエントロピーの減少期待値を最大化するプローブを選択する。これにより、より少ないプローブ数で同等の検出精度を実現する。

4. 忠実性誘導デコーディング (Faithfulness-Guided Decoding: FGD):
   BPFスコアを自動形式化プロセス中の報酬信号として使用するフィードバックループである。サンプル・アンド・リランク（抽出と再ランク付け）の設定において、候補はBPFによってスコアリングされる。トップの候補が「REVIEW」または「REJECT」ゾーンに属する場合、最も高いスコアを持つ「証拠プローブ（エラーを明らかにした特定のプローブ）」が、エラーを修正するためのインコンテキスト・ヒントとしてLLMにフィードバックされる。

3. 理論的保証

本論文は2つの主要な理論的結果を提供している。

• ドリフト検出定理: 特定のドリフトクラス $D$ に対して、プローブ生成器が非ゼロの「証拠能力率（witnessability rate）」 $\alpha$ を持つ場合、BPFはプローブ予算 $k \ge \frac{1}{\alpha} \log(1/\delta)$ を用いて、確率 $1-\delta$ でドリフトを検出できることを証明している。
• PAC-Faithfulness: プローブ分布が到達可能なあらゆるドリフトを証拠立てられると仮定した場合、NL記述の同値類は $O(\log(1/\delta)/\epsilon)$ 個のプローブから学習可能であることを確立している。

また、著者らは以下の限界も認めている：BPFは慣習ドリフト（convention drift）（表記は変わるが論理的内容は同一である場合）を検出できず、また証明オラクルの完全性に依存している（不完全な証明は偽陰性を招く可能性がある）。

4. 実験結果

著者らは、制御されたドリフトラベルを持つ2,183組のNL/Lean 4ペアからなるベンチマーク DRIFTBENCH を公開した。

検出性能:

• BPF + CPG は、3.0%の偽陽性率において、89.6% のドリフトした形式化を検出した。
• これは以下のベースラインを大幅に上回っている：
  • 型チェックのみ: 11.4% 検出
  • 証明可能性（証明不能フラグ）: 41.2% 検出
  • LLM-judge（直接的な忠実性チェック）: 63.3% 検出
  • バックトランスレーション（逆翻訳）: 58.9% 検出
• APBA は、検出率を維持しながら、一様サンプリングと比較して計算コスト（ウォールクロックタイム）を 3.2倍 削減した。

FGDの影響:
最先端の自動形式化器にポストプロセッシングとして適用した場合、FGDはドリフトした記述の放出率を 19.4% から 10.3% へ（47%の相対的減少）減少させた。これは主に、仮定の欠落および結論の一般化エラーに対する再プロンプトによって達成された。

5. 意義と主張

本論文は、忠実性のギャップこそが、完全な数学ライブラリの規模での信頼できる自動形式化における主要なボトルネックであると主張している。本研究の意義は以下の点にある：

1. リファレンスフリーの認証: 「ゴールドスタンダード」となる形式化を必要とせずに、忠実性を検証する方法を提供している（ゴールドスタンダードは通常入手困難である）。
2. 意味論の運用化: 評価パラダイムを、構文的な重複（BLEU）や証明可能性から、推論的意味論（inferential semantics）（帰結近傍）へとシフトさせている。これは証明論的意味論と一致する。
3. スケーラビリティ: APBAと等価スペクトラムを導入することで、人間による専門的なレビューを置き換えるのではなく、優先順位を付けるための実用的かつ費用対効果の高いトリアージツールを提供している。
4. ベンチマーク: DRIFTBENCHは、制御されたドリフトラベルを持つ初のベンチマークとして提示されており、証明能力ではなく忠実性を体系的に評価することを可能にしている。

著者らは、BPFを（特に慣習ドリフトに関する制限を注記した上で）完璧な解決策としてではなく、忠実性のギャップを埋め、AIが生成した形式的な数学を厳密なライブラリへ安全に統合するための具体的な一歩として位置づけている。