IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation
作者: 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
分类: cs.CL
发布日期: 2025-09-30
💡 一句话要点
IMProofBench：用于评估AI在研究级数学证明生成能力的新基准
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 数学证明生成 大型语言模型 基准测试 研究级问题 AI评估
📋 核心要点
- 现有数学能力评估基准主要集中于最终答案或高中竞赛题，缺乏对研究级数学证明生成能力的有效评估。
- IMProofBench提供了一个包含同行评审研究级数学问题的基准，并模拟了真实研究环境，允许模型使用工具进行文献搜索和数学计算。
- 实验结果表明，当前LLM在较简单问题上表现良好，但在更复杂问题上仍面临挑战，Grok-4在子问题上准确率最高，GPT-5在证明生成上最佳。
📝 摘要（中文）
随着大型语言模型（LLMs）的数学能力不断提高，评估它们在数学知识前沿的研究级任务中的表现变得越来越重要。然而，现有的基准测试存在局限性，因为它们只关注最终答案问题或高中竞赛问题。为了解决这个问题，我们推出了IMProofBench，这是一个私有基准，包含由数学专家开发的39个同行评审问题。每个问题都需要详细的证明，并配有最终答案的子问题，从而支持通过人工专家评估数学推理能力，并通过自动评分进行大规模定量分析。此外，与之前的基准测试不同，评估设置模拟了真实的研究环境：模型在代理框架中运行，并使用诸如Web搜索进行文献综述和诸如SageMath之类的数学软件等工具。我们的结果表明，当前的LLM可以成功解决更容易的研究级问题，但在更具挑战性的问题上仍然遇到重大困难。在定量方面，Grok-4在最终答案子问题上实现了52％的最高准确率，而GPT-5在证明生成方面表现最佳，为22％的问题实现了完全正确的解决方案。IMProofBench将继续发展成为与数学界合作的动态基准，以确保其与评估下一代LLM的相关性。
🔬 方法详解
问题定义：论文旨在解决现有基准测试无法有效评估大型语言模型（LLMs）在研究级数学证明生成能力的问题。现有基准主要集中于最终答案或高中竞赛题，无法反映LLMs在复杂数学推理和证明方面的真实水平。此外，现有基准缺乏真实研究环境的模拟，限制了LLMs利用外部工具进行辅助推理的能力。
核心思路：论文的核心思路是构建一个更具挑战性和真实性的数学证明生成基准，即IMProofBench。该基准包含由数学专家设计的同行评审研究级问题，并模拟了真实的研究环境，允许LLMs使用Web搜索和数学软件等工具进行辅助推理。通过这种方式，可以更全面、准确地评估LLMs在数学研究方面的潜力。
技术框架：IMProofBench的整体框架包括以下几个主要组成部分：1) 问题集：包含39个同行评审的研究级数学问题，每个问题都需要详细的证明；2) 子问题：每个问题都配有最终答案的子问题，用于辅助评估和自动评分；3) 评估环境：模拟真实的研究环境，允许LLMs使用Web搜索进行文献综述，并使用SageMath等数学软件进行计算；4) 评估指标：包括最终答案的准确率和证明的完整性、正确性等指标。
关键创新：IMProofBench的关键创新在于其问题集的难度和真实性。与现有基准相比，IMProofBench的问题更具挑战性，更接近数学研究的前沿。此外，IMProofBench模拟了真实的研究环境，允许LLMs使用外部工具进行辅助推理，这更符合实际应用场景。
关键设计：IMProofBench的关键设计包括：1) 问题选择：问题由数学专家设计，并经过同行评审，确保其难度和质量；2) 评估环境：使用代理框架，允许LLMs自主选择和使用工具；3) 评分标准：采用人工评估和自动评分相结合的方式，全面评估LLMs的数学推理和证明能力。
🖼️ 关键图片
📊 实验亮点
实验结果显示，当前LLM在IMProofBench基准上表现参差不齐。Grok-4在最终答案子问题上取得了52%的最高准确率，表明其在解决特定数学问题方面具有一定潜力。GPT-5在证明生成方面表现最佳，为22%的问题生成了完全正确的解决方案，但仍有很大的提升空间。这些结果表明，LLM在研究级数学问题上仍面临挑战，需要进一步的研究和改进。
🎯 应用场景
IMProofBench的研究成果可应用于评估和提升AI在数学研究领域的应用能力，例如辅助数学家进行定理证明、发现新的数学规律等。该基准的建立有助于推动AI在科学发现领域的应用，并促进人机协作的数学研究模式。
📄 摘要（原文）
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.