五一劳动节到了，DeepSeek 的新消息可没停下来。

前些天到处都在流传着 DeepSeek-R2 即将发布的传言，DeepSeek 确实有新动作，不过大家没等来 R2，等来的是 DeepSeek-Prover-V2，它当然也是开源的。

Prover-V2 在定理证明赛道上实现了业内最佳性能，在 MiniF2F 测试中达到了 88.9% 的通过率，在 AIME 24、25 上也有不错的分数。

4 月 30 日晚，机器学习协作平台 HuggingFace 上就更新了 DeepSeek-Prover-V2 的一些技术细节。

这次 DeepSeek 团队发布了两个版本的 DeepSeek-Prover-V2 模型，参数规模分别为 7B 和 671B。

其中，DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基础上训练而成，而 DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5-Base 构建，并支持最长 32K tokens 的上下文长度扩展。

要一句话总结 DeepSeek-Prover-V2 到底是什么？ 它是一款专为“数学 AI 编程语言”Lean 4 打造的开源大语言模型，专注于形式化定理证明。

它的初始化数据通过一个由 DeepSeek-V3 驱动的递归定理证明流程收集而来。在冷启动训练阶段，首先通过提示 DeepSeek-V3 将复杂问题分解成一系列可以解决的子目标。每解决一个子目标就会将这些证明整合成“思维链”。融合 DeepSeek-V3 的逐步推理轨迹，共同构建出用于强化学习的初始训练数据。

这一策略的精妙之处在于：它能够将非形式化和形式化的数学推理融合到一个统一的模型中，让模型既能像人一样灵活思考，也能像机器一样严谨论证，实现了数学推理的一体化融合。

这次，DeepSeek 还发布了 ProverBench，这是一个包含 325 道题目的基准数据集。其中，15 道题来自最近两届 AIME 数学竞赛（AIME 24 和 25）中的数论与代数题目，经过形式化处理，具备真实的高中竞赛难度。其余 310 道题则精选自教材示例和教学教程，覆盖内容多样，涉及高中竞赛题和本科数学题。

在社交网络上有人表示，将复杂问题分解再处理的方式像极了人们教给初级工程师的技巧，DeepSeek-Prover-V2 处理数学问题的思路对于代码等问题来说应该也是毫无问题。

不过，大家似乎对 DeepSeek-R2 有着更大的热情！敲敲这头小蓝鲸，R2 到底什么时候发出啊！

（本文选自《机器之心》微信公众号，《DeepSeek开源Prover-V2强推理模型，网友：奥数从没这么简单过》，编发有删减）