刚刚，DeepSeek 开源了全新的数学模型 DeepSeekMath-V2，专注可自验证的数学推理框架。
DeepSeek-Math-V2 在 IMO-ProofBench 和 IMO 2025（6 道题中的 5 道）和 Putnam 2024（接近完美的 118/120 分）等比赛中表现出色。
新模型可以通过验证器-生成器循环进行自验证推理，代表自主数学发展取得重大飞跃。
邵智宏为此篇论文一作，也是之前提出 GRPO 的 DeepSeekMath 7B 一作。
自验证模型
实验表明，正确的答案并不能保证推理过程的正确性。此外，许多数学任务需要严谨的逐步推导，这使得最终答案奖励不再适用。
为了突破深度推理的极限，DeepSeek 认为有必要验证数学推理的全面性和严谨性。自验证对于扩展测试时间计算能力尤为重要，特别是对于那些尚无已知解决方案的开放性问题。
为了实现可自验证的数学推理，团队研究了如何训练一个基于大型语言模型的定理证明验证器，再以验证器为奖励模型训练一个证明生成器，并激励生成器在最终定稿前尽可能多地识别和解决自身证明中的问题。
为了在生成器性能提升的同时保持生成与验证之间的差距，DeepSeek 团队提出扩展验证计算能力，以自动标记新的难以验证的证明，从而创建训练数据以进一步改进验证器。
DeepSeekMath-V2 展现了强大的定理证明能力，在 IMO 2025 和 CMO 2024 上取得了金牌水平的成绩，并在 Putnam 2024 上取得了接近完美的 118/120 分（测试时间计算量已扩展）。
这些结果表明，可自我验证的数学推理是一个可行的研究方向，可能有助于开发更强大的数学人工智能系统。
验证方法
团队还引入了元验证：这是一个辅助评估过程，用于评估验证者识别出的问题是否确实存在，以及这些问题是否根据评估标准在逻辑上证明了预测的证明分数。
该元验证器会生成一份分析中发现问题的摘要，并给出一个质量评分，用于衡量验证器分析的准确性和合理性。
利用训练好的元验证器 ??，研究人员通过将元验证反馈整合到奖励函数中来增强验证器的训练。
证明验证器和生成器形成了一个协同循环：验证器改进生成器，而随着生成器的改进，它会生成新的证明，从而挑战验证器当前的性能。
为了提高标注效率，研究人员对每个证明生成多个验证器分析，以便发现潜在问题供人工审核。
通过人工智能辅助标注过程，团队发现了两个事实：
扩大验证器样本规模可以提高发现有缺陷证明中真正问题的概率；
审查验证者发现的问题实际上就是元验证，对于语言学习来说，掌握元验证也更节省样本成本。
这两个发现使得进一步提高自动化程度成为可能。
实验结果
在所有 CNML 级别问题类别（代数、几何、数论、组合数学和不等式）中，DeepSeekMath-V2 的性能始终优于GPT-5-Thinking-High 和 Gemini 2.5-Pro ，展现了其在各个领域卓越的定理证明能力。
通过对 IMO 2024 短名单题目进行顺序精炼，模型可以提升证明质量的过程。每个题目有 32 个独立的精炼线程。用户自行选出的最佳证明的验证得分显著高于线程平均水平，这表明生成器能够准确评估证明质量。
自验证能够有效地指导迭代改进。生成器能够区分高质量证明和有缺陷的证明，并利用这种自我感知能力系统地改进其数学推理能力。
模型解决了 IMO 2025 的 6 道题中的 5 道，以及 CMO 2024 的 4 道题，并在另一道题上获得了部分分数，在这两项顶尖高中数学竞赛中均取得了金牌成绩。
在 Putnam 2024（顶尖的本科生数学竞赛）中，模型完全解决了 12 道题中的 11 道，剩余的 1 道题也仅有少量错误，最终得分118/120，超过了人类最高分 90 分。
模型的方法在基础数据集上优于 DeepMind 的 DeepThink（IMO 金牌得主），在高级数据集上也保持竞争力，同时显著优于所有其他基线模型。但是，IMO 级别最难的问题仍然具有挑战性。
值得注意的是，对于尚未完全解决的问题，生成器通常能够识别出其证明中存在的真实问题，而完全解决的问题则通过了全部 64 次验证尝试。这表明基于 LLM 的验证器能够自动评估以前被认为难以验证的证明。
参考资料：
https://github.com/deepseek-ai/DeepSeek-Math-V2/blob/main/DeepSeekMath_V2.pdf
【免责声明】本站所刊内容仅代表作者本人观点，与机器人网站无关。机器人网站对文中陈述、观点判断保持中立。本网转载自其它媒体的信息，转载目的在于传递更多信息，并不代表本网赞同其观点和对其真实性负责。如有侵权，请联系我们删除。
本文地址：http://www.jiqiren.org.cn/tt/1265.html