DeepSeek-Prover-V2 是 DeepSeek 团队推出的专为 Lean 4 形式化定理证明设计的大型语言模型。该模型的核心在于利用强化学习进行子目标分解，从而提升形式化数学推理能力。通过递归定理证明流水线、子目标解决与合成、冷启动数据生成、强化学习和课程学习等创新方法，DeepSeek-Prover-V2 能够在解决复杂数学问题上取得显著进展。该模型分为 671B 和 7B 两个版本，训练流程包括非 CoT 模式和 CoT 模式，旨在提升模型的推理过程和最终证明能力。

💡 递归定理证明流水线：该模型使用 DeepSeek-V3 模型将复杂问题分解为一系列子目标，并同时生成自然语言的证明草图和 Lean 4 形式化语句框架，从而简化了证明过程。

🧩 子目标解决与合成：利用一个较小的 7B 参数 Prover 模型递归地解决由 DeepSeek-V3 分解出的子目标，并将已解决的子目标证明组合起来，构建原始复杂问题的完整形式化证明，提升了解决问题的效率。

📝 冷启动数据生成：通过将 DeepSeek-V3 生成的链式思考过程与最终合成的完整形式化证明配对，生成高质量的、结合了非形式化推理和形式化证明的初始训练数据，为模型的训练提供了坚实的基础。

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

📚 课程学习：利用分解出的子目标生成不同难度的定理，逐步增加训练任务的难度，引导模型学习，有助于模型逐步掌握更复杂的证明技能。

2025-05-01 11:49 北京

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

跳转微信打开