DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

📄 arXiv: 2504.21801v2 📥 PDF

作者: 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

分类: cs.CL, cs.AI

发布日期: 2025-04-30 (更新: 2025-07-18)

💡 一句话要点

DeepSeek-Prover-V2：强化学习分解子目标，提升形式化数学推理能力

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化定理证明 大型语言模型 强化学习 子目标分解 Lean 4 神经定理证明 思维链 数学推理

📋 核心要点

  1. 现有神经定理证明方法在处理复杂数学问题时，缺乏有效的子目标分解策略，导致推理效率和成功率受限。
  2. DeepSeek-Prover-V2利用DeepSeek-V3进行问题分解和思维链合成，为强化学习提供高质量的冷启动数据，融合非形式化和形式化推理。
  3. DeepSeek-Prover-V2-671B在MiniF2F-test上达到88.9%的通过率，并在PutnamBench和ProverBench上取得了显著成果，缩小了形式化与非形式化推理的差距。

📝 摘要（中文）

DeepSeek-Prover-V2是一个开源的大型语言模型，专为Lean 4中的形式化定理证明而设计。其初始化数据通过DeepSeek-V3驱动的递归定理证明流程收集。冷启动训练过程首先提示DeepSeek-V3将复杂问题分解为一系列子目标。已解决子目标的证明被合成为思维链过程，并结合DeepSeek-V3的逐步推理，为强化学习创建一个初始冷启动。这个过程使我们能够将非形式化和形式化数学推理集成到一个统一的模型中。最终模型DeepSeek-Prover-V2-671B在神经定理证明方面达到了最先进的性能，在MiniF2F-test上达到了88.9%的通过率，并解决了PutnamBench中的658个问题中的49个。除了标准基准之外，我们还引入了ProverBench，这是一个包含325个形式化问题的集合，以丰富我们的评估，包括来自最近AIME竞赛（24-25年）的15个精选问题。对这15个AIME问题的进一步评估表明，该模型成功解决了其中的6个。相比之下，DeepSeek-V3使用多数投票解决了其中的8个问题，突显出大型语言模型中形式化和非形式化数学推理之间的差距正在大幅缩小。

🔬 方法详解

问题定义：论文旨在提升大型语言模型在形式化定理证明方面的能力，特别是在Lean 4证明器中的表现。现有方法，尤其是基于大型语言模型的神经定理证明方法，在处理复杂数学问题时，往往难以有效地分解问题为可管理的子目标，导致推理过程效率低下，最终证明成功率不高。此外，如何将非形式化的数学推理能力（例如解决奥数题的直觉）迁移到形式化的定理证明环境中，也是一个挑战。

核心思路：论文的核心思路是利用大型语言模型（DeepSeek-V3）的强大问题分解能力，将复杂的定理证明问题分解为一系列更易于解决的子目标。然后，通过合成已解决子目标的证明过程，构建思维链，并将其与DeepSeek-V3的逐步推理相结合，为后续的强化学习过程提供高质量的冷启动数据。这种方法旨在融合非形式化和形式化的数学推理能力，从而提升模型在形式化定理证明方面的整体性能。

技术框架：DeepSeek-Prover-V2的整体框架包含以下几个主要阶段：1) 问题分解：利用DeepSeek-V3将复杂问题分解为子目标。2) 思维链合成：将已解决子目标的证明过程合成为思维链。3) 冷启动训练：利用问题分解和思维链合成的结果，为强化学习提供初始数据。4) 强化学习：使用强化学习算法对模型进行训练，提升其定理证明能力。5) 模型评估：在MiniF2F-test、PutnamBench和ProverBench等基准数据集上评估模型的性能。

关键创新：该论文最重要的技术创新点在于利用大型语言模型进行子目标分解，并将其与强化学习相结合，从而实现了形式化定理证明能力的显著提升。与现有方法相比，该方法能够更有效地处理复杂问题，并能够将非形式化的数学推理能力迁移到形式化的证明环境中。

关键设计：论文中关于参数设置、损失函数和网络结构的具体技术细节未详细描述，属于未知信息。但可以推测，强化学习部分的奖励函数设计至关重要，需要能够有效地引导模型学习正确的证明策略。此外，DeepSeek-V3作为问题分解器的性能直接影响后续流程，其prompt工程也至关重要。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

DeepSeek-Prover-V2-671B在MiniF2F-test上达到了88.9%的通过率，成为该基准上的SOTA。在PutnamBench上解决了658个问题中的49个。此外，在ProverBench的15个AIME问题中，DeepSeek-Prover-V2成功解决了6个，而DeepSeek-V3使用多数投票解决了8个，表明形式化和非形式化推理之间的差距正在缩小。

🎯 应用场景

DeepSeek-Prover-V2在形式化验证、软件工程、数学研究等领域具有广泛的应用前景。它可以用于验证软件和硬件系统的正确性，辅助数学家进行定理证明，并为AI安全提供更强的保障。该研究有助于推动可信AI的发展，并促进人机协作在数学和计算机科学领域的应用。

📄 摘要（原文）

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 proving 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-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model. The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions (years 24-25). Further evaluation on these 15 AIME problems shows that the model successfully solves 6 of them. In comparison, DeepSeek-V3 solves 8 of these problems using majority voting, highlighting that the gap between formal and informal mathematical reasoning in large language models is substantially narrowing.