技術要約: MathAdv

問題提起

形式的な定理証明は、数学的推論を評価するための厳密かつ機械検証可能な枠組みを提供するが、既存のベンチマークには、モデルの能力に関する微細な理解を妨げる3つの決定的な限界がある。

1. 診断解像度の不足: 現在のベンチマークは通常、集計された証明精度のみを報告する。これは、失敗の原因が数学的背景知識の欠如によるものか、非形式的な推論のエラーによるものか、あるいは妥当な議論を形式的な証明へと翻訳する能力の欠如によるものかを区別できない。
2. ドメイン・カバレッジの狭さ: 既存のデータセットは、高校および学部レベルの数学における競技数学に大きく偏っており、代数や数論に重点が置かれている。位相幾何学（トポロジー）、フーリエ解析、関数解析といった高度な領域は十分に代表されていない。
3. 堅牢性評価の欠如: 評価は一般的に、単一の固定された問題定式化に依存している。これは、問題提示の些細な変化に対する言語モデルの感受性を無視しており、成功が堅牢な推論によるものか、あるいは記憶されたパターンや表面的な手がかりへの依存によるものかを判断することを困難にしている。

手法

著者らは、コンポーネントごとの評価フレームワークを通じてこれらの課題に対処するために設計された診断ベンチマーク、MathAdvを導入する。

データセット構築

• 範囲: MathAdvは、学部から大学院レベル（例：抽象代数学、微積分学、位相幾何学、関数解析、論理学）にわたる13の数学ドメインに及ぶ321の問題で構成されている。
• 形式化: 298の問題はLean 4で形式化された。残りの23問は補助タスクのために保持されたが、Mathlibライブラリのギャップ（例：ビショップ・グロモフ不等式のようなリーマン幾何学の概念の定義の欠如）により、形式化は保留された。
• ヒューマン・イン・ザ・ループ・パイプライン: セマンティックな忠実性とコンパイル可能性を確保するため、著者らは人間による専門家レビューを伴うLLM支援型パイプラインを採用した。このプロセスには以下が含まれる：
  1. 初期オートフォーマライゼーション: LLMがLean 4のステートメントをドラフトする。
  2. 構文修正: Leanコンパイラが、コードが型チェックされるまで反復的な修正のためのフィードバックを提供する。
  3. 二重セマンティック検証: 独立したLLMとドメイン専門家が、形式的なステートメントが元の数学的意図と一致していることを検証する。
  4. 最終エキスパートレビュー: 第二の専門家が最終的な検証を行う。

診断タスク設計

各問題に対して、MathAdvは特定の能力を分離するために最大3つの補助タスクを構築する：

1. 形式的証明 (コア): 機械検証可能なLean 4の証明を構築するという標準的なタスク。
2. 知識 (多肢選択式): 関連する定理、概念、または戦略を妥当な選択肢から特定することをモデルに求める質問。これは、証明の構築を必要とせずに背景知識を調査する。
3. 非形式的推論 (穴埋め式): 自然言語でターゲットとなる量や式を計算することを要求する直接回答問題であり、数学的推論を形式化の制約から分離する。
4. 堅牢性 (専門家による変種): ドメイン専門家が、基礎となる数学を保持しつつ、提示方法を大幅に変更して（例：言い回しや構造の変更）問題を再定式化する。これは、モデルが特定の定式化に依存しているのか、それとも汎用的な推論能力を持っているのかをテストする。

主な貢献

1. 広範で専門家レビュー済みのベンチマーク: MathAdvは、位相幾何学や関数解析のような未代表な領域を含む、形式的および補助的なタスクを組み合わせた、13の高度な数学ドメインにわたる包括的なベンチマークである。
2. コンポーネントごとの診断フレームワーク: 形式的な証明構築を知識の想起および非形式的な推論から切り離すことで、このフレームワークは研究者が特定の失敗モード（例：知識の欠如 vs 形式化のボトルネック）を特定することを可能にする。
3. 定理証明器の体系的な特性評価: 著者らは、現代のモデルの包括的な評価を提供し、ドメイン間の性能の格差や、自然言語によるガイダンスの効果の変動を明らかにしている。

結果

様々な定理証明器（DeepSeek-Prover、Goedel-Prover、InternLM、およびGPT-5.4やDeepSeek-R1のような汎用LLMを含む）の評価により、4つの主要な知見が得られた：

1. 形式化が主要なボトルネックである: モデルはしばしば有望な証明の方向性を特定し、基礎となる数学を解決する（穴埋め式および多肢選択式タスクで高い精度を示す）が、それらの洞察を有効なLean 4の証明へと翻訳することに失敗する。例えば、DeepSeek-Prover-V1.5 RLは、形式的証明では11.25%の精度であったが、直接回答問題では37.0%の精度を達成した。
2. ドメイン固有の性能分散: 性能は数学的ドメインによって大きく異なる。競技数学（例：Goedel-Prover-V2）を重点的に学習したモデルは、数論や線形代数において優れているが、位相幾何学では0%の精度を記録した。これは、学習データのバイアスと、現在のライブラリにおける高度な概念の形式化の難しさを示唆している。
3. 自然言語ヒントの文脈依存的な有用性: 自然言語による推論ヒント（多肢選択式の回答から派生したもの）を提供することは、汎用LLM（DeepSeek-V3.2, DeepSeek-R1）の性能を向上させたが、証明特化型モデル（Goedel-Proverの変種）の性能を低下させた。これは、特化型モデルが、非形式的なガイダンスによって妨げられる学習済みの形式的パターンに依存している可能性があることを示している。
4. 再定式化に対する脆弱性: モデルは「堅牢性のギャップ」を示す。ほとんどのモデルは、専門家によって作成された変換後の変種よりも、元の問題を大幅に多く解いた（例：Goedel-Prover-V2は、6つの元の問題を解いたが、変換された問題は0であった）。これは、真の数学的理解ではなく、表面的なパターンや特定の問題定式化への依存を示唆している。

重要性

本論文は、集計された定理証明の精度は、現代のAIシステムの能力を診断するには不十分であると主張している。MathAdvを導入することで、著者らはコンポーネントごとの評価が以下の明確な失敗モードを明らかにすることを実証している：

• 知識の欠如: モデルがそのドメインに必要な特定の定理を欠いている可能性がある。
• 推論のエラー: モデルが自然言語においても問題を解決できない可能性がある。
• 形式化の困難: モデルは数学を理解しているが、証明助手（proof assistant）の厳密な構文で表現できない可能性がある。
• 提示への感受性: 問題が言い換えられるとモデルが失敗する場合があり、これは真の汎化能力の欠如を示している。

著者らは、将来の形式的定理証明の進展には、より優れた数学的推論だけでなく、証明助手とのより良い相互作用、より広範な高度な数学ライブラリ（Mathlib）のカバー、および特定の定式化の暗記よりも問題の再定式化に対する堅牢性を優先する学習戦略が必要であると結論付けている。データセットおよび評価スクリプトは、さらなる研究を促進するために公開されている。