技术摘要：IMProofBench

问题陈述

目前的数学评估基准在评估大规模语言模型（LLM）的研究级能力方面仍显不足。现有的数据集主要集中在高中或本科竞赛题目（如 AIME、MATH），这些题目正逐渐被最先进的模型所攻克，无法测试真正的证明编写能力。此外，针对高级数学的基准（如 FrontierMath 和 Humanity's Last Exam (HLE)）通常将评估限制在最终答案的正确性上。这种局限性使得模型能够利用捷径或通过猜测正确答案来完成任务，而无需构建逻辑严密的论证，从而忽略了生成严谨数学证明这一关键技能。目前缺乏一个标准化的、私有的基准，用于在真实的、工具增强的环境中评估 LLM 的研究级证明生成能力。

方法论

基准构建 (IMProofBench)

IMProofBench 是一个私有基准，包含 77 个经过同行评审的问题，由 44 位以上专业数学家协作开发。问题创建流程包括：

• 作者身份： 问题由其特定领域的研究人员编写，涵盖从研究生水平的口试题到开放式研究问题。
• 同行评审： 每项提交都经过核心团队成员和相关领域外部专家的严格评审，以确保数学正确性、难度适中以及表达清晰。
• 结构： 每个问题由一个主要的证明编写任务和若干具有唯一且可自动评分答案的后续子问题组成。这种双重结构既支持人类专家对证明过程的评估，也支持对最终答案的自动化定量分析。
• 动态特性： 该基准被设计为一个持续性的平台。问题会滚动添加，且鼓励作者在问题因新研究成果而变得可解时将其退役，以确保基准不会饱和。

评估框架

评估使用基于 Inspect 框架构建的**智能体框架（agentic framework）**来模拟真实的研究环境。模型可以使用以下资源：

• 计算工具： Python (NumPy, SciPy, SymPy)、Bash (Arch Linux) 以及专门的数学软件，包括 SageMath, GAP, Maxima, PARI/GP 和 Singular。
• 文献检索： 网络搜索能力，用于定位相关的定理、论文或数据（如 OEIS）。
• 交互： 模型进行多轮交互，并利用 submit 工具来区分推理步骤与最终输出。

评分过程

评估分为两个阶段：

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 月解决了一个问题。

最终答案 vs. 证明生成

在包含后续子问题的 45 个问题子集上，GPT-5.4 的最终答案准确率为 75%。子问题得分与人类评分的证明进度之间的相关性为 0.51，这表明虽然最终答案准确率是一个有用的代理指标，但它缺乏评估推理过程质量所需的细微差别。

错误与工具分析

• 错误类型： 逻辑错误是最常见的失败模式（例如，无根据的假设），尤其是在 CLAUDE-OPUS-4.6 中（占响应的 40%）。此外还观察到了对不存在定理的幻觉现象。
• 工具使用： 模型在工具使用方面差异显著。GEMINI-3.1-PRO 的工具调用次数几乎是其他模型的四倍，但使用的输出 Token 最少。
• 消融实验： 对智能体设置的消融研究显示，工具访问通常能提高性能（例如，GROK-4 提升了 14.4%），尽管某些模型（如 GEMINI-2.5-PRO）的表现略有下降，这可能是由于工具选择不当（例如，过度使用代码解释器进行数学推理）导致的。

定性观察

• 文献知识： 领先的模型展示了对专门数学文献的强大熟悉度，但在处理如私人讲义等晦涩来源时表现挣扎。
• 幻觉与置信度： 模型经常通过幻觉结果来强行得出答案，并且即使陷入困境也极少拒绝提供解决方案。它们经常以高置信度呈现错误的论证。
• 洞察力： 尽管存在错误，模型经常能提供对人类研究人员有用的见解和部分进展，GPT-5.4 在约 60% 的尝试中提供了有意义的贡献。

意义与主张

本文声称 IMProofBench 通过将关注点从竞赛类题目转向研究级证明生成，解决了评估中的关键空白。作者断言：

1. 当前能力： 最先进的 LLM 已经可以解决相当一部分研究级问题，表明了它们作为数学协作者的潜力。
2. 局限性： 当前的模型仍不完美，容易出现逻辑错误和幻觉，并且往往缺乏区分正确最终答案与有效证明的能力。
3. 评估必要性： 该基准证明，最终答案指标不足以衡量数学能力；对推理过程进行人类专家评估至关重要。
4. 未来方向： 这项工作建立了一个在现实研究场景中进行持续、动态评估 LLM 的框架，促进了研究如何将 AI 有效整合进数学工作流。

作者保持了谦逊的态度，指出该基准目前处于积极开发阶段，问题数量有限（77 个），但认为即便如此规模也提供了关于 AI 在数学研究轨迹方面的宝贵见解。