Benchmarking Testing in Automated Theorem Proving

以下は、Jongyoon Kim、Hojae Han、Seung-won Hwang による論文「Benchmarking Testing in Automated Theorem Proving」の詳細な技術的サマリーです。

1. 問題提起

大規模言語モデル（LLM）の急速な進歩により、Lean などのシステムにおける形式的証明の生成能力は向上しました。しかし、現在の評価手法には致命的な欠陥が存在します：構文の妥当性と意味的な正しさを混同しているという点です。

• コンパイルの限界: 既存のベンチマーク（例：MiniF2F、ProofNet）は、生成された定理がコンパイルされるかどうかをチェックすることでモデルを評価しています。コンパイルはコードが構文的に妥当であり、単体で論理的に整合していることを検証しますが、その定理が意図した数学的意味を捉えていることを保証するものではありません。
• 「トートロジー」問題: モデルは、$a + b = a + b$ のような単純なトートロジーを生成し、コンパイルに成功させることができますが、$a + b = b + a$（交換法則）のような意図した非自明な命題の証明には失敗します。
• プロキシの不適切さ: 意味的正しさを測定しようとする既存の試みは、人間が注釈をつけた参照に対する語彙的重なり（BLEU スコア）や手動検査といった信頼性の低いプロキシに依存しています。これらの手法はノイズが多く、高価な人的労力を必要とするか、正しい意味と誤った意味を区別できないという問題があります。

2. 手法

著者は、ソフトウェア工学における結合テストに触発されたパラダイムシフトを提案します。定理を単体で評価するのではなく、コードベースの残りの部分とどのように相互作用するかに基づいて評価します。

中核概念：定理テスト（T2）

カーリー・ハワードの対応（証明はプログラムに対応する）に基づき、著者は生成された定理を関数として、それに依存する定理を「テストケース」として扱います。

• 依存グラフ: 対象定理（$t_{GT}$）が使用する定義や補題である先行者（predecessors）と、それを呼び出したり構築したりする定理である後継者（successors）を含む依存グラフを構築します。
• 結合テストのロジック: 生成された定理（$t_{fl}$）が意味的に誤っている場合（例えば、意図した性質の代わりにトートロジーを定義する場合）、それに依存する任意の後継定理はコンパイルに失敗します。
• カット除去の類比: このプロセスは、論理原則であるカット除去に形式的に根ざしています。証明の連鎖（$X \to Y \to Z \to W$）において、中間の補題（$Y$）を生成された候補に置き換えた際に失敗する場合、その候補は意味的に誤っていると判断されます。

T2 ベンチマーク

著者はこの評価を促進するために大規模ベンチマークT2を構築しました。

• ソース: 5 つの実際の Lean 4 リポジトリ（代数学、位相幾何学、数論などを網羅）から抽出。
• 規模: 2,206 の問題。各問題には平均41 の後継定理がペアリングされています。
• ハードサブセット: 与えられた命題に対する証明を埋めるだけでなく、命題（ステートメント）と証明の両方を生成しなければならない 389 の「Hard」問題のサブセット。
• 自動化: 抽出パイプラインは完全に自動化されており、依存構造の構築に人間の注釈を必要としません。自然言語（NL）記述は強力な LLM（Claude Sonnet 4.5）によって生成され、サンプルに対して手動検証が行われました。

指標：テスト精度（TA）

論文では、主要な評価指標として**テスト精度（Testing Accuracy: TA）**を導入しています。
$$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$$
生成された定理は、元の定理を生成されたものに置き換えた際に、すべての依存する後継定理が正常にコンパイルされる場合にのみ合格となります。

3. 主要な貢献

1. T2 ベンチマーク: 単体の問題を超えて実世界のリポジトリ文脈へ移行した、依存関係に富む初の大型形式的定理証明ベンチマーク。
2. テスト精度（TA）: 依存モジュールのコンパイルを通じて意味的正しさを直接検証する、新規かつ自動的な参照不要の指標。
3. 実証的ギャップ分析: 18 の最先端モデル（オープンソースおよびクローズドソースの両方）の包括的評価により、コンパイル成功と意味的正しさの間に巨大な乖離があることを明らかにしました。
4. 文脈に関する知見: 自然言語の証明のみを提供するのではなく、後継定理を文脈として提供することが意味的正しさを大幅に向上させることを実証しました。

4. 実験結果

著者は、T2 ベンチマーク上で GPT-5、Claude-Sonnet-4.5、Llama-3.1、DeepSeek-Prover などの専門数学モデルを含む 18 のモデルを評価しました。

• 意味的ギャップ:

  • コンパイル精度: モデルは高いコンパイル率を達成しました（例：Claude-Sonnet-4.5 はフルセットで80.3%）。
  • テスト精度（TA）: 同じモデルは TA スコアが劇的に低くなりました（例：Claude-Sonnet-4.5 はフルセットで38.9%、ハードセットでは4.5%）。
  • 偽陽性: コンパイル可能な定理の最大**93.1%**が、後継者に対するテストにおいて意味的に誤っていることが判明しました。

• 既存指標の失敗:

  • BLEU: 高い語彙的類似性（BLEU スコア）は、意味的正しさとほとんど相関を示しませんでした（相関：0.123）。モデルはテキスト的に類似しているが論理的に誤った証明を生成できました。
  • 専門モデル: 定理証明のために微調整されたモデルは、しばしば高いコンパイル率を達成しましたが、TA においては汎用モデルと同程度かそれ以下の性能しか発揮しませんでした。これは、意味ではなく構文に過剰適合していることを示唆しています。

• 文脈の影響:

  • 後継定理を入力文脈として提供することは、一貫して TA を向上させました（例：Claude-Sonnet-4.5 で +4.9%）。
  • 後継定理なしにNL 証明のみを提供しても性能は向上せず、場合によっては低下しました。
  • Few-shot プロンプティングや反復的改善（コンパイラフィードバックの使用）は、ハードセットにおいてほとんど改善をもたらさず、課題はタスクのフォーマットではなく、深い意味推論にあることを示しています。

5. 意義と結論

この論文は、形式的定理証明（ATP）評価の現状を根本から問い直しています。

• 成功の再定義: 「コンパイル」は定理生成にとって必要だが十分ではない条件であることを証明しました。モデルは構文的に完璧であっても、意味的には無用である可能性があります。
• 信頼性: T2 ベンチマークと TA 指標は、LLM が数学的概念を真に理解しているのか、それとも構文的に妥当なコードを単に幻覚（ハルシネーション）させているのかを評価するための厳格かつ自動的な方法を提供します。
• 将来の方向性: この研究は、将来の ATP システムは孤立したパズルを解く能力ではなく、既存のコードベースへの統合能力（依存関係を考慮した生成）に基づいて評価されるべきであることを示唆しています。また、生成中にモデルに「テストスイート」（後継定理）を提供することが、意味的整合性を向上させるための重要な戦略であることを浮き彫りにしました。

要約すると、この論文は、結合テストが形式的数学における LLM 評価の欠落した鍵であることを主張し、現在の最先端モデルが定理証明において信頼できる意味的正しさを達成するにはほど遠いことを明らかにしています。