DeepSeek强势回归，开源IMO金牌级数学模型

机器之心报道

机器之心编辑部

突破级推理模型来了，DeepSeek 打开了自我验证的数学推理方向。

The whale is back!

就在刚刚，DeepSeek 又悄咪咪在 Hugging Face 上传了一个新模型：DeepSeek-Math-V2。

顾名思义，这是一个数学方面的模型。它的上一个版本 ——DeepSeek-Math-7b 还是一年多以前发的。当时，这个模型只用 7B 参数量，就达到了 GPT-4 和 Gemini-Ultra 性能相当的水平。相关论文还首次引入了 GRPO，显著提升了数学推理能力。

那时隔一年半，这个基于 DeepSeek-V3.2-Exp-Base 开发的 DeepSeek-Math-V2 又带来了哪些惊喜？

DeepSeek 表示，它的性能优于 Gemini DeepThink，实现了 IMO 金牌级的水平。

• 论文标题：DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
• 模型地址：https://huggingface.co/deepseek-ai/DeepSeek-Math-V2
• 论文地址：https://github.com/deepseek-ai/DeepSeek-Math-V2/blob/main/DeepSeekMath_V2.pdf
• 核心作者：邵智宏、Yuxiang Luo、Chengda Lu、Z.Z. Ren

论文开篇，DeepSeek 就指出了当前 AI 在数学推理方面的研究局限：以正确的最终答案作为奖励，过于追求最终答案准确度。

这种做法虽然能让推理模型在 AIME 和 HMMT 等基准上达到更高水平，乃至达到饱和，但 DeepSeek 表示这并不能解决核心问题：正确答案并不保证推理过程正确。此外，许多数学任务（如定理证明）需要严谨的逐步推导，而不仅仅是数值答案，这使得基于最终答案的奖励方法不适用。

为了推动深度推理的极限，DeepSeek 认为有必要验证数学推理的全面性和严谨性。

他们指出：「自我验证在扩展测试时的计算规模时尤为重要，特别是对于没有已知解的开放性问题。」

为了实现可自我验证的数学推理，DeepSeek 研究了如何训练一个准确且可信赖的基于 LLM 的定理证明验证器。然后，他们使用该验证器作为奖励模型来训练证明生成器，并激励生成器在最终完成证明前尽可能发现并解决自身证明中的问题。

为了在生成器能力增强时保持生成 - 验证差距，DeepSeek 提出扩展验证计算能力，以自动标注新的难以验证的证明，从而生成训练数据进一步提升验证器性能。

简单来说，DeepSeek 这篇论文的核心目标不仅仅是让 AI 做对题，而是让 AI 「不仅会做，还能自己检查，甚至能诚实地承认自己哪里做错了」。

为了实现这一点，他们设计了一套由三个关键角色组成的系统，我们可以用一个「学生 — 老师 — 督导」的类比来理解：

首先，培养合格的「阅卷老师」（Proof Verification）。

过去训练 AI 数学模型，通常只看最后的答案对不对。但在高等数学证明题（如奥数）中，过程严谨比答案更重要。因此，DeepSeek 团队首先训练了一个专门的验证器（Verifier），也就是「阅卷老师」。这个老师不只是打钩打叉，而是学会了像人类专家一样把证明过程分为三档 ：

• 1 分：完美，逻辑严密。
• 0.5 分：大体正确，但有小瑕疵或细节遗漏。
• 0 分：有根本性的逻辑错误或严重缺失。

不仅给分，还要写评语：模型被要求在打分前，先写一段分析，指出哪里好、哪里有问题 。

接下来，给老师配个「督导」（Meta-Verification）。

DeepSeek 发现了一个问题：阅卷老师有时候会胡乱扣分，它可能给了个低分，但指出的错误其实根本不存在（也就是产生了幻觉）。

为了解决这个问题，他们引入了元验证（Meta-Verification）机制，相当于给老师配了个「督导」。督导的任务不是看考卷，而是专门检查老师写的「评语」是否合理。这样可以双重确认：督导会检查老师指出的错误是否真实存在，以及扣分是否符合逻辑。效果上，通过训练模型既能当老师又能当督导，AI 评估证明的准确性和可信度大幅提升。

然后，培养会「自省」的学生（Proof Generation with Self-Verification）。

有了好的阅卷系统，接下来就是训练做题的「学生」（生成器）。这里有一个非常关键的创新：诚实奖励机制。也就是说，它不仅做题，还要自评：模型在输出解题过程后，必须马上跟上一段「自我评价」，自己给自己打分（0、0.5 或 1）。

它会对诚实进行奖励：

• 如果模型做错了，但它在自评中诚实地指出了自己的错误，它会得到奖励 。
• 相反，如果它做错了却硬说自己是对的（盲目自信），或者试图「蒙混过关」，就会受到惩罚（得不到高奖励）。

这样做的目的是可以迫使 AI 在输出答案前进行深度思考，试图发现并修正自己的错误，直到它认为自己真的做对了为止 。

最后，形成自动化闭环（Synergy）。

人类专家没法给成千上万道奥数题写详细的步骤评分，所以 DeepSeek 设计了一套自动化流程，让系统「左右互搏」来自我进化 ：

• 海量生成：让「学生」对同一道题生成很多种解法。
• 集体投票：让「老师」对这些解法进行多次评估。如果大多数评估都认为某个解法有问题，那就判定为有问题；如果没有发现任何漏洞，才判定为正确 。
• 以战养战：通过这种方式，系统自动筛选出那些很难判卷或很难做对的题目，变成新的教材，重新训练「老师」和「学生」。这样，随着「学生」解题能力变强，「老师」的眼光也越来越毒辣 。

总之，DeepSeekMath-V2 的方法本质上是从「结果导向」转向了「过程导向」。它不依赖大量的数学题答案数据，而是通过教会 AI 如何像数学家一样严谨地审查证明过程（包括审查它自己），从而在没有人类干预的情况下，也能不断提升解决高难度数学证明题的能力 。

最终，他们得到了 DeepSeekMath-V2 模型，其展现出了强大的定理证明能力：在 IMO 2025 和 CMO 2024 上取得金牌级成绩，并在 Putnam 2024 中以扩展测试计算实现了接近满分的 118/120。

下图展示了 DeepSeekMath-V2 在 IMO-ProofBench 基准（这是 IMO Bench 的一个子集，其中包含 60 道证明题）上的表现，可以看到，在其中的 Basic 基准上，DeepSeekMath-V2 不仅远胜过其它模型，甚至达到了近 99% 的惊人高分。而在更难的 Advanced 子集上，DeepSeekMath-V2 略逊于 Gemini Deep Think (IMO Gold)。

DeepSeek 表示：「虽然仍有大量工作需要推进，但这些结果表明，可自我验证的数学推理是一个可行的研究方向，有望推动更强大数学 AI 系统的发展。」

这一自我验证的数学推理框架可以说突破了传统强化学习（RL）的限制，让模型不再依赖最终答案正确性作为唯一奖励，而是关注推理过程的严谨性。此外，DeepSeekMath-V2 中的验证器 - 生成器协同的双向改进循环带来了全面和严谨的数学推理能力，大幅减少了大模型幻觉。

在论文中，DeepSeek 介绍了更多技术细节，感兴趣的同学可以去仔细阅读。返回