一个能够自我验证的 AI 系统，正离攻克研究级数学问题更近一步。
11 月 27 日，DeepSeek 正式开源了其全新模型 DeepSeekMath-V2，这是一款具备“奥数金牌级”定理证明能力的 AI 系统。
DeepSeekMath-V2 在 2025 国际数学奥林匹克（IMO 2025）和 2024 中国数学奥林匹克（CMO 2024）中展现了金牌水准的表现。更令人瞩目的是，它在 2024 普特南数学竞赛中取得了 118/120 的几乎满分成绩，远远超过目前已知的人类最高分 90 分。
从性能评测来看，DeepSeekMath-V2 在 IMO-ProofBench 等关键证明测试中，以 10% 的明显优势击败了谷歌的 IMO 金奖模型 DeepThink。
这些成果揭示了一个突破性的结论：自我可验证的数学推理不仅是可能的，而且可能是打造更强数学 AI 系统的关键道路。
按照 DeepSeek 一贯做法，该模型在发布后立即上线可用。在初步测试中，DeepSeekMath-V2 能迅速给出经典题目的正确证明，例如“证明 √2 是无理数”。当输入“奇数和偶数哪个更多？”时，它也给出了严谨且结构清晰的证明过程，即使非专业人士也能理解。当然，奥数级的证明题要复杂得多，高水平数学读者可以自行尝试更深入的体验。
回顾模型背后的研究思路，传统强化学习（RL）在只需要最终答案的竞赛（如 AIME 或 HMMT）中可以获得高分，但 DeepSeek 指出这种方法天然存在两个关键局限：
首先，仅凭最终答案不能可靠反映推理正确性。模型可能通过逻辑漏洞或侥幸路径获得正确结果。
其次，它不适用于定理证明场景，因为此类问题考察的核心不是最后答案，而是严谨的推导过程本身。
为解决这个问题，DeepSeek 专注于在大语言模型中建立显式证明验证能力。基于 DeepSeek-V3.2-Exp-Base，DeepSeekMath-V2 被训练为理解奖励机制，并通过有意识的推理而非盲目试错来优化证明质量。
DeepSeek 为证明评估建立了一套高级评分标准，使模型能够模拟数学专家的判断方式。以 DeepSeek-V3.2-Exp-SFT 为基础版本，通过强化学习训练模型生成证明分析，并采用格式奖励和评分奖励两种核心机制。
训练数据集包括 17503 道数学竞赛题目、模型生成的候选证明，以及人工专家评分的证明样本，形成了极大的强化学习训练语料库。DeepSeek 随后为生成器和验证器分别定义了强化学习目标。虽然这一机制让分析能力更强，但研究人员发现了一个潜在漏洞：验证器可能通过生成看似合理的分数来“操纵系统”，而并未真正理解证明问题。
为修复这一点，DeepSeek 引入了“元验证”（meta-verification）机制，通过第二层分析模型，大幅提高判断证明质量的可信度。
在证明生成阶段，模型被训练为循序检查推理过程，而不是直接宣称证明正确。这样可以防止模型在验证器指出错误后仍坚持自己没有错误。
最终，DeepSeek 的验证器与生成器形成了一个协同循环：验证器帮助生成器改进，而生成器不断产生新的证明挑战验证器；这些挑战又成为训练验证器的宝贵数据。简单来说：验证器逐步检查推理，生成器从错误中自我修正。
实验结果表明，在 CNML 的所有数学类别（代数、几何、数论、组合数学、不等式）中，DeepSeekMath-V2 始终优于 GPT-5-Thinking-High 和 Gemini 2.5-Pro，展现出更卓越的定理证明能力。
在带自我验证的顺序优化中，DeepSeekMath-V2 在 2024 IMO 备选题上的证明质量显著提升，并显示其能够准确区分高质量与有缺陷的证明，并自主优化推理。
在高计算量推理实验中，该系统成功解决了 IMO 2025 中 6 题中的 5 题，以及 CMO 2024 中 4 题 + 1 题部分分数的解答，取得了金牌水准成绩。不仅在基础测试集上超过了 DeepMind 的 DeepThink，而且在高级测试集上依然保持竞争力。
不过 DeepSeek 也指出，最难的 IMO 级题目仍对模型构成挑战。
值得注意的是，对于未完全解决的问题，DeepSeekMath-V2 通常能在自己的证明中识别出真正的推理障碍；而对完全解决的问题，其证明能通过 64 轮验证尝试而无冲突。这表明验证器已经能够评估那些此前被认为几乎不可能自动验证的证明。
通过在推理阶段提升计算投入，DeepSeek 的模型能够解决那些需要人类耗费数小时才能完成的题目。
结论：一个能够自我验证的 AI 架构，可能是攻克研究级数学的核心突破。
总的来说，DeepSeek 打造了一个既能生成又能审查数学证明的模型。团队突破了基于最终答案的奖励机制局限，迈向了真正的自我验证数学推理时代。
这一成果表明，大语言模型能够发展出适用于复杂推理任务的元认知能力。尽管仍有挑战，但这一研究方向已经让 AI 更接近目标：构建真正能够自我验证的 AI 系统，解决研究级数学问题。
