DeepSeek AI 发布 DeepSeek-Prover-V2，这是一个专为 Lean 4 形式化定理证明设计的大型语言模型。该模型的核心在于使用强化学习进行子目标分解，从而提升形式化数学推理能力。Prover-V2 采用了递归定理证明流水线，利用 DeepSeek-V3 将复杂问题分解为子目标，并生成自然语言证明草图和形式化语句框架。通过子目标解决与合成，以及冷启动数据生成和强化学习，最终实现对复杂定理的证明。该模型在训练过程中采用了课程学习，逐步增加训练难度，同时结合了专家迭代和 CoT 模式，以提升推理过程和证明能力。

💡 递归定理证明流水线：DeepSeek-Prover-V2 采用通用 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

跳转微信打开