技術要約: IMProofBench

問題提起

数学における大規模言語モデル（LLM）を評価するための現在のベンチマークは、研究レベルの能力を査定するには不十分である。既存のデータセットは主に高校や大学レベルの競技数学（例：AIME、MATH）に焦点を当てており、これらは最先端のモデルによって容易に解かれつつあり、真の証明能力をテストできていない。さらに、FrontierMathやHumanity's Last Exam (HLE) のような高度な数学を対象としたベンチマークは、多くの場合、最終回答の正誤性に評価を限定している。この制限により、モデルが論理的に健全な議論を構築することなく、ショートカットを利用したり正解を推測したりすることが可能になってしまい、厳密な数学的証明を生成するという極めて重要なスキルを見落とす原因となっている。現実的なツール拡張環境において、研究レベルの証明生成を評価する標準化されたプライベート・ベンチマークが不足している。

メソドロジー

ベンチマーク構築 (IMProofBench)

IMProofBenchは、44名以上の専門数学者との協力により開発された、77件の査読済み問題で構成されるプライベート・ベンチマークである。問題作成のパイプラインは以下の通りである：

• 執筆: 問題は、大学院レベルの口頭試験問題から未解決の研究問題に至るまで、それぞれの専門領域内の研究者によって執筆される。
• 査読: 各提出物は、数学的正当性、適切な難易度、および明快さを確保するために、コアチームのメンバーと該当分野の外部専門家による厳格なレビュープロセスを経る。
• 構造: 各問題は、メインの証明記述タスクと、自動採点可能な一意の回答を持つフォローアップのサブクエスチョンで構成されている。この二重構造により、証明に対する人間による専門的な評価と、最終回答に対する自動的な定量的分析の両方をサポートする。
• 動的な性質: 本ベンチマークは継続的なプラットフォームとして設計されている。問題は随時追加され、新しい研究によって解けるようになった問題については、ベンチマークの飽和を防ぐために著者が問題を退役させることが推奨される。

評価フレームワーク

評価は、Inspectフレームワーク上に構築されたエージェント型フレームワークを用いて、現実的な研究環境をシミュレートする。モデルは以下へのアクセス権を持つ：

• 計算ツール: Python (NumPy, SciPy, SymPy)、Bash (Arch Linux)、および数学用特殊ソフトウェア（SageMath, GAP, Maxima, PARI/GP, Singularを含む）。
• 文献検索: 関連する定理、論文、またはデータ（例：OEIS）を特定するためのウェブ検索機能。
• インタラクション: モデルはマルチターン・インタラクションを行い、推論ステップと最終出力を区別するために submit ツールを利用する。

採点プロセス

評価は2段階で行われる：

1. 自動採点: フォローアップのサブクエスチョンは、モデルの出力を正解（グラウンドトゥルース）と比較することで採点される。
2. 人間による専門家採点: メインの証明は、問題の著者が0〜3のスケールを用いて評価する：
   • 0/3: 進展なし。
   • 1/3: わずかな進展（限定的な前進）。
   • 2/3: 大きな進展（実質的な作業の完了）。
   • 3/3: 完全な解決。
     採点者はまた、特定の誤りタイプ（論理的誤り、ハルシネーション、計算エラー、概念的な誤解）と達成指標（理解、正しい結果、洞察、有用性）を注釈する。バイアスを防ぐため、採点中はモデルの識別子は隠蔽される。

主な貢献

1. IMProofBench: 数学コミュニティとの直接的な協力を通じて開発された、研究レベルの数学的証明生成に特化した、プライベートで進化し続けるベンチマーク。
2. 体系的な分析: 単なる最終回答の正確性を超え、人間による専門家の判断に基づいた、証明生成に関する最先端LLMの包括的な評価。
3. 定性的洞察: 最終回答の正確性と真の証明能力との間のギャップ、および研究ツールとの相互作用を浮き彫りにする、モデルの強みと失敗モードの詳細な分析。

実験結果

パフォーマンス概要

著者らは、証明ベースの部分について10種類のLLMを評価した：

• トップパフォーマー: GPT-5.4 が最も高い性能を示し、タスクの 49% で完全な解決策（3/3）を生成した。GEMINI-3.1-PRO が 46% で僅差でこれに続いた。
• 低パフォーマンス: CLAUDE-OPUS-4.6 は、完全な解決策を提供できたのは 32% のタスクのみであった。
• 未解決問題: ベンチマーク内の23の未解決研究問題のうち、GPT-5は2025年12月に1つを解決した。

最終回答 vs. 証明生成

フォローアップのサブクエスチョンを含む45問のサブセットにおいて、GPT-5.4は最終回答の正確性で 75% を記録した。サブクエスチョンのスコアと人間が採点した証明の進捗との相関関係は 0.51 であり、これは最終回答の正確性が有用なプロキシ（代理指標）ではあるものの、推論プロセスの質を評価するために必要な精緻さに欠けていることを示唆している。

エラーおよびツール分析

• エラータイプ: 論理的エラー（例：根拠のない仮定）が最も一般的な失敗モードであり、特に CLAUDE-OPUS-4.6 において顕著であった（回答の40%）。存在しない定理のハルシネーションも観察された。
• ツール利用: モデル間でツール利用に大きな差が見られた。GEMINI-3.1-PRO は他のモデルの約4倍のツールコールを行ったが、出力トークン数は最も少なかった。
• アブレーション研究: エージェント設定に関するアブレーションにより、ツールへのアクセスは一般的に性能を向上させることが明らかになった（例：GROK-4 で +14.4%）。ただし、一部のモデル（例：GEMINI-2.5-PRO）では、ツールの選択が最適でないこと（例：数学的推論に対してコードインタープリタを使いすぎる等）により、性能がわずかに低下した。

定性的観察

• 文献知識: 指導的なモデルは専門的な数学文献に対して強い習熟度を示したが、私的な講義ノートのような非常にマイナーなソースには苦戦した。
• ハルシネーションと自信: モデルは答えを出すために結果をハルシネーション（捏造）することが多く、行き詰まった場合でも回答を控えることはほとんどなかった。しば_多くの場合、誤った議論を高い自信を持って提示した。
• 洞察: エラーはあるものの、モデルは頻繁に人間にとって有用となり得る洞察や部分的な進展を提供しており、GPT-5.4 は試みの約60%において意味のある貢献を行った。

意義と主張

本論文は、IMProofBenchが、焦点を集団競技スタイルの問題から研究レベルの証明生成へとシフトさせることで、AI評価における決定的なギャップを埋めるものであると主張している。著者らは以下の通り述べている：

1. 現在の能力: 最先端のLLMはすでに研究レベルの問題の有意義なサブセットを解決できており、これは数学的コラボレーターとしての潜在能力を示している。
2. 限界: 現在のモデルは依然として不完全であり、論理的エラーやハルシネーションを起こしやすく、正しい最終回答と妥当な証明を区別する能力に欠けることが多い。
3. 評価の必要性: 本ベンチマークは、最終回答の指標が数学的能力を測定するには不十分であることを示しており、推論プロセスの評価には人間の専門家による評価が不可しくは不可欠である。
4. 今後の方向性: 本研究は、現実的な研究環境におけるLLMの継続的かつ動的な評価のための枠組みを確立し、AIがいかに効果的に数学的ワークフローに統合され得るかの研究を促進するものである。

著者らは、本ベンチマークが現在進行形で開発中であり、問題数も77件と限定的であることを認めつつも、この規模であってもAIの数学研究における軌跡に関する貴重な洞察を提供できると主張している。