技術的サマリー：CAM-Bench

問題定義

大規模言語モデル（LLM）向けの既存の形式定理証明ベンチマークは、主にオリンピックスタイルの問題や代数的領域（例：MiniF2F、PutnamBench、ProofNet）に焦点を当てている。これらのベンチマークは形式的推論の進展を促してきたが、応用数学および計算数学の領域は著しく過小評価されたままとなっている。

応用数学の問題（最適化、数値線形代数、数値解析など）は、孤立した定理の記述とは根本的に異なる。これらは文脈に依存しており、以下に依存することが多い：

• 局所的に導入された定義、記法、アルゴリズム。
• 章固有の慣習と初等的な結果。
• 演習問題に明示されていないが、忠実な形式化に必要とされる、継承された仮定。

現在のベンチマークは、モデルがこれらの局所的な仮定を追跡できるか、教科書の文脈に基づいて証明を分解できるか、Mathlib4 などの形式ライブラリで標準的な補題としてまだ利用できない初等的な結果を適用できるかを評価することに苦慮している。「局所的文脈」が定理の記述自体と同様に重要である、応用数学の問題を対象としたベンチマークが必要とされている。

手法

著者らは、最適化、数値線形代数、数値解析の教科書演習 778 題から導出された 1,000 の証明ターゲットを含む Lean 4 定理証明ベンチマークCAM-Benchを導入する。このベンチマークの構築は、文脈依存の演習問題を自己完結型で機械検証可能なターゲットに変換するように設計された、新規の依存関係回復および形式化パイプラインに依存している。

1. 依存関係回復および充実パイプライン

教科書演習の非自己完結性を解決するため、著者らは再帰的依存関係拡張手順（アルゴリズム 1）を開発した：

• 再帰的拡張： 生（raw）の演習問題から開始し、システムは参照（定理、方程式、アルゴリズム）を抽出し、それらの定義と依存関係を有界な深さまで再帰的に取得する。
• ボトムアップ自然化： 依存関係ツリーをボトムアップで処理する。LLM 自然化器は、充実された表現をマージし、局所的な参照を解決し、記法を標準化し、遷移を滑らかにすることで、より高次の依存関係が使用される前に低次の定義が組み込まれるようにする。
• 暗黙的条件の回復： システムは、元の問題または回復された文脈によって支持される場合にのみ、必要な仮定（例：定義域の制限、正性、凸性）を明示化する。この充実はソースに基づくものであり、欠落した依存関係を推測するのではなく、回復できない場合はそれらを除外する。
• 多ラウンドレビュー： 充実された記述は、欠落した仮定、タスクの逸脱、Lean への適合性を確認するための検証ループを経る。修正は、数学的目標を変更したり、サポートされていない依存関係を創作したりすることなく、局所的な欠陥を修正する範囲に制限される。

2. モジュール化駆動型 Lean 形式化

非形式的なターゲットが確立されると、システムは凍結された文脈、ブロックごとの構築戦略を用いて、それを Lean 4 コードに変換する：

• 意味的ブロック分解： 異質な演習問題は、定義、最適化問題、アルゴリズム、定理ターゲットといった、型付けされた意味的ブロックに分解される。これにより、最終的な定理の目標から支援的な文脈が分離される。
• インクリメンタル翻訳： システムはブロックを逐次翻訳する。以前に承認された宣言は、凍結された読み取り専用文脈として保持される。これにより、連鎖的なエラーを防ぎ、失敗を現在のブロックに局所化できる。
• コンパイラ主導および意味的修復：
  • コンパイル修復： ブロックがコンパイルに失敗した場合、フィクサーはコンパイラ診断を用いてローカルなパッチ（構文、型注釈、名前空間の解決）を生成する。
  • 意味的レビュー： レビュアーは、コンパイル可能な候補を非形式的なブロックと比較し、意味的な忠実性（変数、仮定、結論の保持）を確認する。不一致が発生すると、意味的な書き換えがトリガーされる。
• 履歴Aware制御： システムは、失敗した試行と拒絶理由の履歴を維持し、振動を防ぎ、後続の修復を以前に失敗した方向から遠ざけるように導く。

3. ベンチマーク構築と検証

最終データセットには、生演習問題、回復された文脈、正規化された非形式的定理、および最終的な Lean ターゲットが含まれる。検証は 2 つのレベルで行われる：

• ソースレベル： 非形式的ターゲットが教科書演習に忠実であり、自己完結型であることを保証する。
• Lean レベル： 形式的宣言がレビューされた非形式的ターゲットを保持することを保証する。意味的検証の後、候補宣言の 92.5% だけが使用可能と判断され、忠実な自動形式化の難しさが浮き彫りになった。

主要な貢献

1. CAM-Bench データセット： 最適化、数値線形代数、数値解析にまたがる 1,000 の Lean 証明ターゲットからなるキュレーションされたベンチマーク。生演習問題から機械検証済みの Lean ターゲットまでの追跡可能なアーティファクトを提供し、応用数学の評価におけるギャップを埋める。
2. 依存関係回復パイプライン： 文脈依存の演習問題から忠実な Lean ターゲットを構築するための新規手法。再帰的依存関係拡張、ソースに基づく充実、および制約付き修復を組み合わせ、Mathlib4 の標準的な補題として存在しない局所的な定義や仮定を処理する。
3. 包括的な評価とエラー分析： 本論文は、CAM-Bench 上で最先端の LLM と形式化エージェントを評価する。特定の失敗モードを特定する：
   • ライブラリ/API 接地： モデルは利用可能な Mathlib インフラに証明を接地できず、API を幻覚させたり、橋渡し結果を見落としたりする。
   • 形式的表現： 型の規律、次元/インデックスの不一致、強制変換の失敗におけるエラー。
   • 証明分解： 長期的な証明を補助的な補題に分解すること、または複雑な最適化/数値的論理を制御することの inability。

結果

ベースライン性能

• 非エージェントモデル： 最強の非エージェントベースライン（例：Deepseek-v4-pro、Claude-sonnet-4-6）でさえ、検証済み Lean 精度は低く、最高でも19.67%（Pass@32）にとどまった。
• 非形式と形式のギャップ： 非形式的な正しさ（Pass@1 非形式精度は約 70–84%）と、検証済み Lean の正しさ（20% 未満）の間には大きな不一致がある。モデルは高次の論理を捉えるが、厳格な Lean 構文、型の規律、ライブラリの制約を満たすことができない。
• エージェントによる改善： 反復的修復とツールの使用を備えたエージェント型証明探索システム（例：GPT-5.4）は、性能を大幅に向上させ、**44.00%**の検証精度に達した。ただし、これは高いトークンコスト（ベースラインの約 0.26–0.70M に対し、約 1.96M トークン）を伴った。

外部エージェント評価

2 つの外部エージェントシステム、M2FとAristotleを、8 時間の時間予算でサンプリングされた 200 のインスタンスで評価した：

• M2F： 200 件中 143 件（71.5%）を解決。
• Aristotle： 200 件中 125 件（62.5%）を解決。
• これらの改善にもかかわらず、ベンチマークは飽和していない。多くの失敗は、欠落した数学的インフラ、長い補助補題の連鎖、および最適化固有の推論に起因していた。

意義と主張

本論文は、CAM-Bench が、教科書的な概念と初等的な定理に依存する応用数学の問題を対象とすることで、既存の形式ベンチマークに対する重要な補完として機能すると主張する。その意義は以下の点にある：

1. 文脈依存推論の評価： 局所的な仮定を追跡し、文脈を再構築するモデルの能力をテストする。これは実世界の形式化に不可欠な能力であるが、孤立した定理ベンチマークではしばしば回避されてきた。
2. システム的ボトルネックの診断： 結果は、現在の LLM ベースの証明者が構文だけでなく、Mathlib 接地、型の規律、および長期的な証明分解においても苦労していることを浮き彫りにする。
3. インフラ開発の推進： ベンチマークは、形式応用数学の進展には、より強力な Mathlib インフラ（行列、スペクトル、凸性など）と、長期的な証明軌跡を管理できるより能力の高いエージェントが必要であることを示唆している。

著者らは謙虚な立場を維持しており、エージェントシステムが性能を向上させるものの、ベンチマークは依然として挑戦的であり、結果は解決された問題というよりも、現在の能力の見積もりとして見るべきであると指摘している。このベンチマークは、数学的推論システムのより広範な評価スイートの一部として意図されている。