藏师傅代理一图帮了解 DeepSeek 新模型！

Deepseek 放出了 DeepSeek-Prover-V2 的详细论文

藏师傅做了 DeepSeek-Prover-V2 一图流帮你了解这个模型

详细总结分析一下：

Prover-V2 是一个专为 Lean 4 形式化定理证明设计的开源大型语言模型。
其核心目标是利用强化学习进行子目标分解，从而提升形式化数学推理能力。

核心方法与创新：

1️⃣递归定理证明流水线:
利用通用的 DeepSeek-V3 模型将复杂问题分解为一系列子目标
DeepSeek-V3 同时生成自然语言的证明草图 和对应的 Lean 4 形式化语句框架。

2️⃣子目标解决与合成 :
使用一个较小的 7B 参数的 Prover 模型递归地解决由 DeepSeek-V3 分解出的子目标。
将已解决的子目标证明组合起来，构建原始复杂问题的完整形式化证明。

3️⃣冷启动数据生成:
将 DeepSeek-V3 生成的链式思考过程与最终合成的完整形式化证明配对。
这种方法生成了高质量的、结合了非形式化推理和形式化证明的初始训练数据。

4️⃣强化学习:
在冷启动数据微调的基础上，使用 GRPO 算法进行强化学习。
奖励机制：主要使用二元奖励（证明正确为 1，错误为 0）。在早期训练中加入一致性奖励，鼓励模型生成的证明结构与 CoT 中的子目标分解保持一致。

5️⃣课程学习:
利用分解出的子目标生成不同难度的定理，逐步增加训练任务的难度，引导模型学习。

模型与训练：

主要模型: DeepSeek-Prover-V2-671B (6710亿参数)
小型模型: DeepSeek-Prover-V2-7B (70亿参数，通过蒸馏 671B 模型的 RL 数据得到)
基础模型: DeepSeek-V3 (用于初始分解和 CoT)
训练流程:
第一阶段 (非 CoT 模式): 使用专家迭代 (Expert Iteration) 和课程学习训练非 CoT 模型，侧重于快速生成简洁的 Lean 代码，同时通过子目标分解解决难题并收集数据。
第二阶段 (CoT 模式): 使用合成的冷启动 CoT 数据进行监督微调 ，然后进行强化学习，重点提升模型的推理过程和最终证明能力。

项目地址：github.com/deepseek-ai/DeepSeek-Prover-V2