技術要約：Construction–Verification: Lean 4における応用数学の形式化のためのベンチマーク

1. 問題提起

MiniF2FやProofNetといった現在の自動定理証明用ベンチマークは、主に宣言的な命題の論理的検証（すなわち、解の存在の証明）に焦点を当てている。このパラダイムは、応用数学においては不十分である。なぜなら、応用数学における主要な目的は、単なる存在証明ではなく、具体的な値、実行可能なアルゴリズム、あるいは構造的な変換を導出することにあるからである。

既存のデータセットには、この領域において2つの決定的な限界がある：

1. スコープの乖離： 凸解析、最適化、数値代数、高次元確率論を含む、学部レベルおよびそれ以上の応用数学のカバー範囲が不足している。
2. 構成的欠陥： 「構築（Construction）と検証（Verification）」というワークフローの強制に失敗している。応用数学では、モデルはその正当性を証明する前に、明示的に解（例：アルゴлоズムや特定の数値）を合成しなければならない。現在のベンチマークは、モデルが非構成的なタクティクス（例：極値定理を用いて特定の最適値を計算せずに存在を証明する）を使用してこれを回避することを許しており、計算的推論を行う能力を誤って表現してしまっている。

2. 方法論

Construction–Verification フレームワーク

著者らは、Lean 4における形式化パラダイムとして、「構築（Construction）」に続く「検証（Verification）」という二段階のワークフローを構造的に強制する手法を提案している。このフレームワークは、定義を事前に行うことを要求することで、エージェントによる非構成的なショートカットの利用を防ぐ。このフレームワークは、以下の3つの具体的な応用数学タスクのカテゴリに対処する：

• 評価問題（Evaluation Problems）： エージェントは $\exists x, Q(x)$ を証明するのではなく、パラメータ $V$ に基づいて解 $x(V)$ を計算する関数 def x (V) := ... を定義し、続いて $Q(x(V), V)$ を証明する。関数のシグネチャは入力を生のパラメータのみに厳格に制限しており、モデルが対象となる性質を利用して構築プロセスを「ズル」することを防いでいる。
• アルゴリズム設計問題（Algorithm Design Problems）： エージェントは、反復プロセス（例：勾配降下法）を表す再帰関数を定義しなければならない。タスクは、$n$ ステ目から $n+1$ ステ目への遷移規則（ループ本体）を埋めることと、それに続く収束性や単調性などの性質の証明を要求する。
• 表現変換（Representation Transformation）： エージェントは、生の数学的問題をターゲットとなる標準形（例：グラフカット問題をスペクトルクラスタリングの定式化へと変換する）へとモデル化しなければならない。これには、新しいドメイン、制約、および目的関数の定義が含まれ、ソース問題とターゲット問題の間の緩和または等価関係の証明を伴う。
• 定理証明（Theorem Proving）： 純粋な論理的推論能力を、構成的合成とは別に測定するために、伝統的な演繹的タスクのベースライン・サブセットが含まれている。

ベンチマークのキュレーション (AMBER)

著者らは、以下の4つのコアドメインを網羅するAMBER（Applied Mathematics BEnchmark for Reasoning）を導入する：

1. 凸解析
2. 最適化
3. 数値代数
4. 高次元確率論

データソースと難易度： 問題は古典的な教科書（例：Boyd & Vandenberghe, Vershynin）から収集され、難易度（Easy：標準的な演習問題、Hard：博士課程の資格試験レベル）によって分類されている。
形式化と検証： 50個の各分野の問題が、経験豊富なLeanユーザーによって形式化された。検証には、LLMベースのセマンティック・チェックと、元の数学的記述との厳密な整合性を確保するためのMathlibコントリビューターによる厳格な手動クロスバリデーションの二段階プロセスが用いられた。
複雑性指標： 本ベンチマークは高いセマンティック依存密度によって特徴付けられる。依存グラフ分析（$k=3$）を用いた結果、AMBERは平均依存密度 164.21 を示し、これはMiniF2F (29.72)、ProofNet (33.95)、FATE (53.14) よりも著しく高く、複雑な数学的概念の検索と推論に対する深い要求があることを示している。

3. 主な貢献

1. パラダイムシフト： 論文は、存在命題の検証から構成的解の合成へのシフトを提案しており、形式的なタスクを応用数学の計算的直感に適合させている。
2. AMBERベンチマーク： 単なる定理証明だけでなく、アルゴリズム設計や表現変換のような複雑なタスクを特徴とし、異なる難易度レベルを持つ、コアな応用ドメインをカバーする包括的なデータセット。
3. 形式化パターン： 非構成的な推論に対する厳格な構文的障壁を設ける、評価、アルゴリズム設計、および表現変換のための特化したLean 4テンプレート。
4. 実証的分析： 現在のニューロ・シンボリック・システムにおける根本的なトレードオフ、すなわち局所的なタクティクス習熟度（特化したプルーバー）と高レベルなアルゴリズム合成（汎用モデル）の間の緊張関係を明らかにする体系的な評価。

4. 実験結果

モデルの性能

著者らは、汎用的な推論エージェント（DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro）と、特化した定理プルーバー（Goedel Prover-32B, Kimina Prover-72B）を含む多様なモデルを評価した。

• 全体的な難易度： すべてのモデルにおけるパフォーマンスは著しく低い。 「Hard」サブセットにおいて、ほとんどのモデルの成功率はほぼゼロであった。
• 汎用 vs 特化： 純粋数学のベンチマークにおける傾向とは対照的に、汎用的な推論モデルは一貫して特化した定理プルーバーを上回っている。
  • Pass@16 (Full AMBER): 汎用モデルは4.50%–6.00%を達成したが、特化型プルーバーは4.00%であった。
  • Pass@16 (Hard Subset): 汎用モデルは0%–0%（Easyサブセットには多少の変動あり）であり、特化型プルーバーも同様に大きく苦戦した。
• アブレーション研究： Construction-verification プロンプト戦略は、100問のサブセットに対して8%の成功率を達成し、標準的なコード補完（6%）および従来の証明のみのプロンプト（5%）を上回った。証明のみのプロンプトは、モデルが非構成的なショートカット（例：Classical.choice）を使用する原因となることが頻繁に確認された。

エラー分析

DeepSeek-R1モデルによる3,189個のエラーメッセージの分析により、以下が判明した：

1. ハルシネーション (47.3%): 最も一般的な失敗モードであり、モデルが存在しない定理や定義（例：convexHull eq sInter）を呼び出すケース。
2. 形式化能力の不足 (32.7%): 有効なタクティクスの誤用、またはサイド条件の解消の失敗。
3. 不完全な出力 (15.2%): 完全な実行可能コードを提供できず、複雑な帰納ステップにおいて sorry プレースホルダーを残してしまうケース。
4. フォーマット/構文 (4.8%): 基本的なマークダウンまたは構文エラー。

5. 意義と主張

本論文は、現在の形式化の現状が「タクティカル・オーバーフィッティング（戦術的過学習）」現象に直面していると主張している。数学的コーパス上で集中的に微調整された特化型モデルは、一般的な指示追従能力が低下しているように見受けられる。彼らはあらゆる構造的な課題を純粋な定理証明タスクとして扱い、応用数学の多段階の要件（例：関数を定義してから証明する）を無視することが多い。

対照的に、汎用モデルは、非形式的な意図と形式的な構文の架け橋となるために必要な汎用性を保持しており、検証段階に入る前に数学的オブジェクトを正常に合成することができる。著者らは、形式化された応用数学を進展させるためには、純粋な証明探索を超えて、高レベルなアルゴリズム推論と厳格な形式的検証を統合するニューロ・シンボリック・システムへと移行する必要があると結論付けている。AMBERベンチマークは、単なる論理的妥当性ではなく、構成的合成を要求する基準を提供することで、形式化された応用数学の境界を拡張するための将来の研究の基礎となるものである。