不是R2不是V4DeepSeek却悄悄放了个6710亿参数的狠活

好消息，DeepSeek 发布新模型了！

坏消息，不是小可爱们心心念念的 DeepSeek-R2 和 DeepSeek-V4 。

而是一个专注于数学证明和复杂推理的模型： DeepSeek-Prover-V2-671B 。

此次新模型的发布并开源延续了 DeepSeek 一如既往的低调。

没有任何预热和宣传，Hugging Face 上的 DeepSeek 开源社区悄然上线了这个名为 DeepSeek-Prover-V2-671B 的新模型。

而时间，正好是五一假期的前一刻。

那么，这个新模型是什么来头？

首先划重点， DeepSeek-Prover-V2-671B 不是给你用来聊天、或者运行一般任务的 AI 模型。

实际上， DeepSeek-Prover-V2 可以看作是上一代 Prover-V1.5 的升级版 —— 参数量从 70 亿一下跃升到 6710 亿，重点还是放在 Lean 4 语言下的形式化数学定理证明任务上。

这次升级的一个核心变化，是引入了一个比较特别的冷启动训练流程：用 DeepSeek-V3 作为“引导者”，先把复杂的问题拆解成一个个子目标，再逐步构建对应的证明思路。这个过程中形成的“推理链条”，既包含了问题的分解过程，也保留了完整的数学逻辑路径，最终为大模型提供了一套兼顾非形式化与形式化的训练语料。

不出意外， DeepSeek-Prover-V2 是目前全球最大规模的数学定理证明模型，当然性能也是遥遥领先。

从上面这张对比图可以看出， DeepSeek-Prover-V2 在多个数学评测数据集上都做到了“降维打击”。

不论是针对形式化数学的 MiniF2F-test ，还是涵盖北美数学竞赛难题的 PutnamBench ，亦或是面向高中竞赛题的 ProverBench-AIME ，这个新模型几乎都是碾压式的存在。

简单说几组数字感受一下：

MiniF2F-test：88.9% 通过率 ，远高于同类模型的 70~82%；

PutnamBench：一次性解决 49 道题 ，而前一代 7B 才解出 23 题；

AIME 竞赛题子集 也能搞定 6 道，仅次于非形式化大模型 DeepSeek-V3 的表现。

DeepSeek-Prover-V2 值得关注吗？

如果你是普通用户，大概率不会也不应该直接用它。

但如果你是对数学 AI 感兴趣的开发者或研究者，它的潜力非常具体：

对数学论文进行形式化验证 ，尤其是那些长达数十页、细节繁杂的证明；

辅助教材开发 ：把传统题目变成可验证、可推演的 Lean 格式代码，有助于数学教育；

数学研究助理 ：在探索过程中给出结构合理的“子问题分解 + 初步猜想”。

这里附上 DeepSeek-Prover-V2 模型的 Hugging Face 链接。

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

此外，OpenRouter 这个大模型集散地也第一时间上线了免费可用的 DeepSeek-Prover-V2 模型 API 服务。

有需要的小伙伴可以自行“食用”。