論文の概要: IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation

• arxiv url: http://arxiv.org/abs/2509.26076v1
• Date: Tue, 30 Sep 2025 10:50:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-01 14:45:00.108026
• Title: IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation
• Title（参考訳）: IMProofBench: 研究レベルの数学的証明生成のためのベンチマークAI
• Authors: Johannes Schmitt, Gergely Bérczi, Jasper Dekoninck, Jeremy Feusi, Tim Gehrunger, Raphael Appenzeller, Jim Bryan, Niklas Canova, Timo de Wolff, Filippo Gaia, Michel van Garrel, Baran Hashemi, David Holmes, Aitor Iribar Lopez, Victor Jaeck, Martina Jørgensen, Steven Kelk, Stefan Kuhlmann, Adam Kurpisz, Chiara Meroni, Ingmar Metzler, Martin Möller, Samuel Muñoz-Echániz, Robert Nowak, Georg Oberdieck, Daniel Platt, Dylan Possamaï, Gabriel Ribeiro, Raúl Sánchez Galán, Zheming Sun, Josef Teichmann, Richard P. Thomas, Charles Vial,
• Abstract要約: IMProofBenchは、専門家数学者によって開発された39のピアレビューされた問題からなるプライベートベンチマークである。 それぞれの問題は詳細な証明を必要とし、最終的な答えを持つサブプロブレムと組み合わせられる。 以前のベンチマークとは異なり、評価設定は現実的な研究環境をシミュレートする。
• 参考スコア（独自算出の注目度）: 4.991157581428135
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As the mathematical capabilities of large language models (LLMs) improve, it becomes increasingly important to evaluate their performance on research-level tasks at the frontier of mathematical knowledge. However, existing benchmarks are limited, as they focus solely on final-answer questions or high-school competition problems. To address this gap, we introduce IMProofBench, a private benchmark consisting of 39 peer-reviewed problems developed by expert mathematicians. Each problem requires a detailed proof and is paired with subproblems that have final answers, supporting both an evaluation of mathematical reasoning capabilities by human experts and a large-scale quantitative analysis through automated grading. Furthermore, unlike prior benchmarks, the evaluation setup simulates a realistic research environment: models operate in an agentic framework with tools like web search for literature review and mathematical software such as SageMath. Our results show that current LLMs can succeed at the more accessible research-level questions, but still encounter significant difficulties on more challenging problems. Quantitatively, Grok-4 achieves the highest accuracy of 52% on final-answer subproblems, while GPT-5 obtains the best performance for proof generation, achieving a fully correct solution for 22% of problems. IMProofBench will continue to evolve as a dynamic benchmark in collaboration with the mathematical community, ensuring its relevance for evaluating the next generation of LLMs.
• Abstract（参考訳）: 大規模言語モデル(LLM)の数学的能力が向上するにつれて、数学的知識の最前線における研究レベルのタスクにおいて、それらの性能を評価することがますます重要になる。 しかし、既存のベンチマークは、最終回答の質問や高校の競争問題にのみ焦点を絞っているため、制限されている。 このギャップに対処するために、専門家数学者によって開発された39のピアレビュー問題からなるプライベートベンチマークIMProofBenchを紹介する。 それぞれの問題は詳細な証明を必要とし、最終回答を持つサブプロブレムと組み合わせて、人間の専門家による数学的推論能力の評価と、自動階調による大規模定量的分析の両方をサポートする。 さらに、以前のベンチマークとは異なり、評価設定は現実的な研究環境をシミュレートする:モデルがエージェントフレームワークで動作し、Web検索による文献レビューやSageMathのような数学的ソフトウェアが動作する。 以上の結果から,現在のLSMはよりアクセスしやすい研究レベルの問題に成功できるが,課題の解決には大きな困難が伴うことが示唆された。 Grok-4はファイナル・アンサー・サブプロブレムで52%の精度を達成し、GPT-5は22%の問題の完全正解を達成している。 IMProofBenchは、数学的コミュニティとのコラボレーションにおいて、動的ベンチマークとして進化を続け、次世代のLLMを評価することの関連性を保証する。

関連論文リスト

• RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics [21.453837660747844]
  大規模言語モデル(LLM)における数学的推論を評価するための既存のベンチマークは、主に競合問題、公式な証明、人工的な問題に依存している。 論文や数理フォーラムから直接派生した新しいベンチマークであるRealMathを導入し,実数理タスクにおけるLLMの能力を評価する。
  論文  参考訳（メタデータ） (2025-05-18T23:32:46Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATHは、LLMの複雑な推論能力を厳格にテストするために設計された、Olympiadレベルの新しい数学ベンチマークである。 OlymMATHは200の厳密にキュレートされた問題があり、それぞれが手動で検証され、英語と中国語の並行バージョンで利用可能である。
  論文  参考訳（メタデータ） (2025-03-27T11:20:17Z)
• HARDMath: A Benchmark Dataset for Challenging Problems in Applied Mathematics [1.5716764919736026]
  本稿では,解析的近似技術を必要とする応用数学問題に挑戦するデータセットであるHARDMathを紹介する。 本フレームワークは,数値基底真理に対して検証された解を用いて,多数の問題を自動生成する。 HARDMath-miniは,366問題からなるサブサンプルテストセットであり,応用科学の文脈で定式化された40の単語問題に対して,オープンソースLLMとクローズドソースLLMの両方を評価する。
  論文  参考訳（メタデータ） (2024-10-13T20:09:41Z)
• ErrorRadar: Benchmarking Complex Mathematical Reasoning of Multimodal Large Language Models Via Error Detection [60.297079601066784]
  エラー検出におけるMLLMの能力を評価するために設計された最初のベンチマークであるErrorRadarを紹介する。 ErrorRadarはエラーステップ識別とエラー分類という2つのサブタスクを評価している。 2500の高品質なマルチモーダルK-12数学問題で構成され、実世界の学生相互作用から収集される。 GPT-4oの優れた性能は、まだ人間の評価に約10%遅れているため、大きな課題が残っている。
  論文  参考訳（メタデータ） (2024-10-06T14:59:09Z)
• Evaluating Mathematical Reasoning Beyond Accuracy [50.09931172314218]
  推論ステップの品質を評価するための新しい方法論であるReasonEvalを紹介します。 ReasonEvalはメタ評価データセットのベースライン手法よりも一貫して優れていることを示す。 我々は、ReasonEvalがデータ選択において重要な役割を果たすことを観察する。
  論文  参考訳（メタデータ） (2024-04-08T17:18:04Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。