DeepSeek Prover-v2发布，英伟达盘前暴跌

北京时间，4月30日 16:15，DeepSeek 在huggingface上发布了 DeepSeek Prover-v2

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

截至20:25，DeepSeek官方尚未有关联的论文、benchmark或说明文章一同发布

同一时间NVDA快速下跌，目前-2.7%（这事太搞笑了，无声屁更臭，无形威胁更为致命）

下图中107.76那个位置就是模型发布的时间

由于官方尚未披露任何技术细节，因此本文会分成两部分：已知信息梳理+不负责任推测

已知信息梳理

1. Prover-v1发布时间在 24年5月23日，利用了独特的Self-instruct机制。DeepSeek针对原始Prover模型（或者说未经微调的原始基座模型）进行形式化推理数据生成，然后通过Lean4进行正确性验证。验证通过后视为高质量数据，再对模型进行训练，从而产生Prover-v1。
2. Prover-v1.5发布于2024年8月15日，在这个版本中额外引入了Cot过程数据及Lean4编辑器状态来进行训练。两个版本训练数据的区别，可以用这个通俗但不恰当的例子：教科书答案数据 VS 教科书答案数据+学霸做题思路+名师实时批改反馈。
3. 值得一提，Prover-v1.5还提出了RMaxTS，一种蒙特卡洛树变体方法，用以解决形式化推理中分步骤求解的搜索问题。这种方法后来尝试用在DeepSeek-R1中，但失败了——但可以视为Prover系列作者是具备很强的能力和意愿在试图用强化学习解决推理问题的。

关于整个Prover系列所致力解决的数学形式化推理问题是什么，或者其他更详细的细节，可以参考过去的飞书文档，我不再额外说明。

《#7 DeepSeek-Prover：自我飞升，数学推理》

《#9 DeepSeek-Prover-V1.5: CoT数据强有力的证明》

不负责任推测

1. 模型参数671B，毫无疑问来自V3的原始基座模型
2. 模型参数从过去的Prover系列的7B级别，跃升到671B，如果不是任务表现上的极度超越，很难相信DeepSeek会贸然这样发布。
3. Prover-v1以及V1.5中的数据构造方法应该继续沿用了，其效果类似R1基于V3构造的数据而从R1-Zero上超脱一样。
4. 整个项目中可以说算力成本不会很高，因为毕竟只是微调。我很关心这种将超级通用模型转化为垂直模型后涉及的能力跃升、成本消耗、数据方法、训练细节等方向DeepSeek会做哪些公开。
5. 我能想象到最极端的利好消息是：① 提了一嘴用国产芯片（毕竟只是微调，用国产是讲得通的）；② 表现出非常好的通用→垂直的能力提升幅度，那么这会推动所有AI的估值，事实上专业&AGI在过去的两年里一直螺旋循环，但专业的声音始终不如AGI的大；③ 是否会较为详细说明相关的数据构造方法和训练细节。这三点都达成的话我的持仓要炸了。
6. 总结而言，我不太关心形式化数学推理的进展（离我太远），但我对超大参数的通用模型转为垂直模型后的能力表现、构造方法很关心，这意味着比通用模型更广阔的市场。