DeepSeekMath-V2 发布，在 IMO 2025 题目上达到金牌水平

背景

许多数学基准过去只看最终答案是否正确。定理证明则不同：证明必须在每一步都严格成立，模型也可能通过有缺陷的论证得出正确结论。深度求索在数学推理方面的工作，目标是检查推理过程本身，而不只是最终答案。该模型以 DeepSeek-V3.2-Exp-Base 为基础构建^[1]。

发生了什么

2025 年 11 月 27 日，深度求索发布了 DeepSeekMath-V2^[1][2]。维基百科将其列为采用 Apache 2.0 许可证^[2]。该模型被定位为可自我验证的推理模型，即严格证明定理，而不只是给出答案^[1]。

关键细节

该设计的核心是一对角色。深度求索训练了一个基于大语言模型的定理证明验证器，并把它用作证明生成器的奖励模型^[1]。生成器通过找出并修正自己证明中的问题，在定稿前获得奖励^[1]。

深度求索还扩大了验证阶段的计算量，使验证器能跟上生成器的进步。额外的计算被用来为难以验证的新证明加上标签，这些标签随后成为验证器的训练数据^[1]。

成绩以竞赛题目报告。深度求索称，该模型在 IMO 2025 和 CMO 2024 的题目上达到金牌水平^[1]。在大学生竞赛 Putnam 2024 中，模型借助扩大后的推理计算量取得了 120 分中的 118 分^[1]。推理计算量指模型处理题目时额外投入的计算。

影响

这次发布表明，模型自身的验证可以成为训练过程的一部分，而验证器充当奖励信号。对读者而言，关键在于评价标准的变化：系统被评判的是论证是否成立，而不只是最终答案是否与标准答案一致^[1]。