DeepSeek-Prover-V2 通过子目标分解强化学习推进形式化数学推理

这份技术报告要回答的是，大语言模型能否在 Lean 4 中完成形式定理证明，以及怎样通过子目标分解和强化学习把这件事做得更系统。材料给出的核心线索是 DeepSeek-Prover-V2：一个面向 Lean 4 的开源大语言模型，其初始化数据来自由 DeepSeek-V3 驱动的递归定理证明流水线。值得现在看的地方在于，它不是只讲最终证明器，而是把“复杂问题如何拆成子目标”“子目标证明如何变成训练数据”这两个环节写进了方法主线。换句话说，读这份材料可以先抓住一条完整的训练链条，而不是零散的模型介绍。

覆盖范围集中在模型定位、数据收集和冷启动训练流程。模型定位是开源、面向 Lean 4 的形式定理证明；数据来源是用 DeepSeek-V3 驱动的递归定理证明流水线收集初始化数据；冷启动则从提示 DeepSeek-V3 分解复杂问题开始。方法上，报告把已解决子目标的证明合成为思维链过程，再与 DeepSeek-V3 的逐步推理结合，用来创建强化学习的初始冷启动。需要说明的是，可见材料是摘要和开篇摘录，重点在方法框架，不是完整实验章节。

第一个关键点是子目标分解被放在训练流程的前端。冷启动训练不是直接要求模型证明整个复杂定理，而是先让 DeepSeek-V3 把复杂问题拆成一系列子目标。随后，已经解决的子目标证明会被合成为思维链过程，作为强化学习开始前的初始冷启动。这意味着，训练数据不只来自最终定理是否被证出，也来自中间子目标的可解证明；更准确地说，材料展示的是一种把“拆题”和“解题”连起来的冷启动构造方式。

第二个关键点是形式与非形式推理的合并。报告明确说，这一过程使非形式数学推理和形式数学推理被整合进一个统一模型。形式部分对应 Lean 4 中的定理证明，非形式部分对应 DeepSeek-V3 的逐步推理和由子目标证明合成的思维链。换句话说，模型不是只在形式证明语料上学习，也不是只做自然语言推理，而是试图让两种推理在训练流程中互相供给。材料还给出项目地址，说明模型和代码入口是公开的；但可见摘录没有给出证明成功率、基准对比或数据规模等性能数字。

这些做法对实践的含义，需要从训练流程而不是单点结果来看。子目标分解把复杂定理变成多个可处理的小问题，已解决子目标的证明又转成思维链，等于为强化学习准备了一个更细粒度的起点。解读来说，这种设计可能降低冷启动阶段对完整长证明的依赖，让模型先学“怎样拆”和“怎样证中间步骤”，再在强化学习中优化整体证明。它也可能让非形式推理成为形式证明的辅助材料，而不是两套彼此分离的能力。材料没有展开强化学习的具体奖励设计，因此这里只能判断流程方向，不能推断实际效果。

适合读这份材料的人，是关心 Lean 4 形式化、LLM 数学推理和强化学习训练流程的读者，尤其是想了解“强模型生成子目标—子目标证明合成思维链—冷启动强化学习”这条链路的人。读完可以拿走一个清晰的方法框架：用 DeepSeek-V3 做子目标分解，用已解决子目标的证明构造思维链，再把非形式推理与形式证明放进同一个模型。边界也很明确：可见材料只有摘要和开篇，没有完整实验数据、基准结果和消融分析，不能据此判断 DeepSeek-Prover-V2 的实际证明能力。若需要核对细节，材料给出的入口是 DeepSeek-AI 的 GitHub 项目页；进一步结论应回到完整技术报告。

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition Z.Z. Ren*, Zhihong Shao*, Junxiao Song*, Huajian Xin†, Haocheng Wang†, Wanjia Zhao†, Liyue Zhang, Zhe Fu Qihao Zhu, Dejian Yang, Z.F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao Daya Guo, Chong Ruan DeepSeek-AI https://github.com/deepseek-ai/DeepSeek-Prover-V2 Abstract We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem prov- ing pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3’s step-