一句话总结

ulam.ai 的研究人员推出了 UnsolvedMath 数据集，作为研究级数学推理基准，并在文献检索、定理证明、证明检查和形式化方面评估了 GPT-5.2、Gemini 3 Pro、Grok 和 Opus 4.5，发现没有一个模型能够自动形式化，GPT-5.2 Extended Thinking 在较简单问题上达到博士生水平，扩展思考时间是推理质量的主要驱动因素，而全局心智图景、系统性自我验证和类比推理仍然缺失。

核心贡献

• 推出了 UnsolvedMath 数据集，这是一个公开基准，将开放数学问题组织成包含检索引理、可验证子目标、确定性测试和证明助手检查的评估回合。
• 定义了一个覆盖文献检索、定理证明、证明检查和形式化的四维评估协议，并将其应用于 GPT-5.2、Gemini 3 Pro、Grok 和 Opus 4.5；结果显示文献检索表现强劲，无法自动形式化，GPT-5.2 Extended Thinking 在较简单问题上达到博士生水平，并且扩展思考时间是推理质量的主要驱动因素。
• 识别出在全局心智图景、系统性自我验证和类比推理方面缺失的能力，通过 Erdős #728 证明支持人机协作范式，并提出类比提示，以区分受引导的推理与自主洞察。

引言

作者探讨了在开放数学问题上评估大型语言模型的挑战，在这种情况下，自信的编造可能产生带有虚构引理或循环推理的看似合理的证明，尤其对非专业用户而言。他们强调数学是一个理想的试验场，因为形式化证明助手提供了客观真值，并且他们认为验证必须内置到工作流中，而不是作为可选项处理。先前的评估往往使用单一难度分数，忽视行为效应，例如模型拒绝被标记为“开放”的问题，并且不区分文献检索、构造性推理和批判性推理。作者贡献了一个基于 UnsolvedMath 的回合协议，该协议包含可验证子目标、确定性代数与数值检查、证明助手片段、为检测测试注入的有缺陷证明，以及用于检索、证明生成、验证和形式化的多维评分标准。

方法

该评估框架将每个 UnsolvedMath 条目视为基准种子，而不是静态提示。针对每个种子，作者提炼出三个组成部分：问题陈述的短上下文版本、一组可检索的相关已知引理或结果，以及一组可验证子目标，例如玩具案例、参数情形或文献引理。这种分解支持同时评估最终定理证明和中间研究过程。

每个模型运行被组织为一个具有固定工具和时间预算的回合。一个回合包括文献检索、提出方法、中间引理尝试、对模型自身输出的证明检查，以及可选的形式化。该预算旨在实现跨系统的公平比较，同时反映一个有限的研究会话。

验证层是该协议的核心。子目标通过确定性测试进行检查，包括代数恒等式、数值计算和有限情形，并在适用时使用证明助手片段。证明检查项还包括注入的有缺陷证明，以衡量模型能否检测错误。该层旨在降低自信编造的风险；在这种编造中，模型生成带有虚构引理、循环推理或虚假参考文献的看似合理的证明。作者建议将开放问题回合与验证层和明确的不确定性量化相结合，尤其是对于没有专业数学训练的用户。

评分是多维的。文献检索按 0 到 5 分制评分，证明检查按 0 到 5 分制评分，形式化按 0 或 1 分制评分。证明按 0 到 5 分制评分，依据已验证子目标的数量和难度，并对超出检索模板的泛化给予额外加分。这一评分标准将搜索与综合、构造性推理和批判性推理区分开来，反映出问题难度可能来自缺失的概念性洞察、冗长的技术链条，或两者兼有。

提示框架也被视为协议的一部分。当问题被标记为开放时，模型往往表现更差或完全拒绝，这似乎源于过度谨慎或习得性无助。为解决这一问题，评估会移除这类标签，或提供候选策略供模型评估。“测试这种方法是否有效”的框架始终优于“解决这个开放问题”。这一设计选择区分了自主推理与受引导的推理，并有助于衡量模型性能在多大程度上依赖人类引导。

实验

在若干标准和竞赛级基准上，最佳模型目前已接近或超过人类基线，包括 GSM8K、MATH、AIME 2025 和 GPQA Diamond。相比之下，FrontierMath 和 PutnamBench 的分数仍然明显较低，表明更困难的研究级数学推理仍具挑战性。模型在 GSM8K、MATH 和 AIME 2025 上已接近饱和表现，并在 GPQA Diamond 上超过了所提供的博士基线。研究级基准显示出最大的剩余差距：FrontierMath 仅达到 40.3%，PutnamBench 达到 70.0%。

在所评估的前沿模型中，数学推理能力因任务而异。所有模型都擅长文献检索，但都无法生成机器可验证的 Lean 形式化。GPT-5.2 表现出最强的定理证明性能，而 Grok 在证明检查方面相对更好。所有模型都获得了文献检索的最高分，表明在检索和综合相关现有成果方面具有一致优势。没有模型生成机器可验证的 Lean 代码，这揭示了形式化方面的共同差距。GPT-5.2 在定理证明方面领先，Grok 位居第二，Gemini 3 Pro 和 Opus 4.5 紧随其后但略有差距。Grok 在识别所提证明中的重大漏洞或无效步骤方面最强，而其他模型得分明显较低。

第一项评估将前沿模型与人类基线在标准和竞赛数学基准上进行比较，结果显示在广泛使用的数据集上表现已接近饱和，而 FrontierMath 和 PutnamBench 等研究级基准仍暴露出显著差距。第二项实验测试了任务特定的数学能力，发现所有模型都一致擅长文献检索，但无法生成机器可验证的 Lean 形式化，其中 GPT-5.2 在定理证明方面最强，Grok 在证明检查方面最强。