DeepSeek-Prover-V2：一种用于形式定理证明的统一非形式与形式推理大语言模型 / DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
1️⃣ 一句话总结
本文提出了DeepSeek-Prover-V2，一个通过创新的子目标分解与强化学习冷启动训练方法，将非形式数学推理与形式化定理证明能力统一在单一模型中的开源大语言模型，在多个数学定理证明基准上达到了新的最先进性能。
2️⃣ 论文创新点
1. 基于子目标分解的强化学习冷启动训练
- 创新点：提出一种冷启动训练程序，利用通用大模型DeepSeek-V3将复杂问题分解为子目标，并将已解决的子目标证明与模型的逐步推理结合，合成为思维链，为强化学习创建高质量的初始训练数据。
- 区别/改进：该方法避免了从零开始的强化学习，通过整合非形式推理（DeepSeek-V3的分解与推理）与形式证明（子目标的形式化证明）来初始化模型。
- 意义：实现了非形式与形式数学推理在单一模型中的统一，为训练高性能形式定理证明模型提供了有效的数据生成和初始化策略。
2. 非形式到形式化的定理证明范式
- 创新点：利用大型语言模型生成自然语言证明草图，并指导形式化证明步骤的分解与生成，借鉴了DSP框架和分层强化学习中的子目标概念。
- 区别/改进：将复杂定理分解为可独立解决的中间命题或引理，使形式化定理证明能够利用非形式数学推理的优势。
- 意义：提高了证明搜索的模块化、可重用性和效率，弥合了非形式推理与形式化证明构建之间的差距。
3. 基于子目标分解的递归证明搜索
- 创新点：利用DeepSeek-V3作为统一工具，将复杂定理的证明分解为一系列更小的引理（子目标），并生成包含
sorry占位符的Lean形式化语句草图。 - 区别/改进：将人类数学家的分层证明策略形式化，通过将复杂问题分解为可管理的子目标，提高了证明搜索的效率。
- 意义：弥合了非形式数学推理与形式化证明构建之间的差距，为从非形式推理冷启动进行强化学习训练奠定了基础。
4. 基于子目标的课程学习框架
- 创新点：通过生成两种类型的子目标定理来扩展用于模型训练的形式陈述范围，并将其整合到专家迭代阶段，建立一个逐步引导证明模型解决挑战性问题的课程。
- 区别/改进：解决了因大量计算尝试未能成功证明而导致训练信号稀疏的问题，生成了更密集的训练信号。
- 意义：增强了模型解决IMO级别挑战性问题的能力，其底层原理与AlphaProof测试时强化学习相同。
5. 双模式证明生成
- 创新点：设计了高效非CoT模式和高精度CoT模式两种证明生成方式，分别针对快速生成简洁证明和透明逻辑推理的不同需求。
- 区别/改进：非CoT模式加速训练迭代和数据收集，CoT模式通过强化学习增强推理能力。
- 意义：提供了灵活高效的证明生成策略，平衡了推理速度与证明质量。
6. 两阶段训练流程
- 创新点：第一阶段在课程学习框架下通过专家迭代训练非CoT证明器并合成难题证明，第二阶段利用冷启动CoT数据增强推理能力。
- 区别/改进：结合了专家迭代的高效性和CoT推理的透明性，通过强化学习进一步提升性能。
- 意义：系统化地整合了不同训练方法的优势，提升了模型在形式化证明任务上的综合能力。
7. 引入ProverBench评估基准
- 创新点：提出了一个包含325个形式化问题的新评估基准ProverBench，其中特别包含了15个来自近期AIME竞赛的精选问题，用于更全面地评估模型在形式定理证明上的能力。
- 区别/改进：补充了现有的标准基准（如MiniF2F、PutnamBench），提供了更多样化、更具挑战性的评估集。
- 意义：丰富了形式定理证明领域的评估体系，有助于更准确地衡量模型在解决复杂、新颖数学问题上的实际性能。
3️⃣ 主要结果与价值
结果亮点
- DeepSeek-Prover-V2-671B在MiniF2F-test基准上达到88.9%的通过率，创造了新的最先进水平。
- 在PutnamBench上解决了47/658个问题，在ProofNet和FormalMATH等多个本科数学基准上均展现出强大的泛化能力。
- 在ProverBench基准上，671B模型在CoT模式下使用512个样本取得了59.1%的最高性能，并成功解决了6个AIME 24&25难题。
- 7B参数版本也表现出色，超越了所有现有开源定理证明器，提供了参数效率高的选择。
- 实验验证了推理时缩放现象在形式定理证明领域成立，即更大的模型即使在非CoT模式下也会生成更长的输出，隐式地外化中间推理步骤。
实际价值
- 提供了一个开源的、高性能的形式定理证明模型，可促进自动推理和形式化验证领域的研究与应用。
- 证明了将非形式推理与形式化证明统一在单一模型中的可行性，为开发更智能的数学助手和自动证明系统提供了新思路。
- 提出的子目标分解、课程学习和冷启动训练等方法，为训练其他领域的复杂推理模型提供了可借鉴的框架。
- 模型在解决AIME、IMO等竞赛级别数学问题上展现的能力，表明其在辅助数学教育、竞赛训练和数学研究方面具有潜在应用价值。
4️⃣ 术语表
- DeepSeek-Prover-V2：一个由DeepSeek-AI开发的开源大语言模型，专门设计用于在Lean 4交互式定理证明器中进行形式定理证明。它通过两阶段训练流程开发，建立了两种互补的证明生成模式：高效非链式思维模式和高精度链式思维模式。
- DeepSeek-Prover-V2-671B：本文提出的神经定理证明模型，通过在子目标分解的非形式推理基础上进行强化学习训练，在多个定理证明基准上达到了新的最先进水平。
- MiniF2F：一个用于评估形式定理证明模型性能的标准基准测试集，包含488个形式化问题陈述，涵盖AIME、AMC、IMO等数学竞赛题目以及MATH数据集中的问题，分为miniF2F-valid和miniF2F-test两个子集。
- Lean：一种形式化证明辅助系统（如Lean 4），要求所有证明步骤都必须被明确构造和形式化验证，不允许任何模糊性。
- 子目标 (subgoal)：在形式化定理证明中，指有助于证明更大定理的中间命题或引理，是实现分层任务分解的关键概念。
- 子目标分解：将复杂定理的证明目标分解为一系列更小、更易处理的引理（子目标）的策略，是人类数学家常用的方法，本文利用DeepSeek-V3模型自动化了这一过程。
- CoT (Chain-of-Thought)：思维链生成模式，是DeepSeek-Prover-V2的一种生成策略，与non-CoT模式相对，通过引导模型生成推理步骤来提升证明能力。
- ProofNet：一个包含371个Lean 3问题的本科数学基准，涵盖实分析与复分析、线性代数、抽象代数、拓扑学等主题，分为ProofNet-valid和ProofNet-test两部分。
- PutnamBench：一个包含658个（评估时使用649个）用Lean 4形式化的大学水平数学问题的基准，涵盖分析、线性代数、组合数学等多个领域，用于评估定理证明模型。
- CombiBench：一个包含100个（评估时使用77个）用Lean 4形式化的组合数学竞赛问题的基准，在“带解答”设置下评估模型的证明生成能力。
- FormalMATH-Lite：一个包含66个本科水平问题的数学定理证明基准子集，用于在计算资源有限的情况下进行系统评估。
- ProverBench：一个用于评估定理证明器性能的基准测试，包含
All类别和AIME 24&25难题。 - 专家迭代：一种形式化定理证明器开发框架，当前最佳证明策略用于生成未解决问题证明的尝试，成功证明被纳入SFT数据集以训练改进模型。
- Group Relative Policy Optimization (GRPO)：一种强化学习算法，通过为每个定理提示采样一组候选证明并基于相对奖励优化策略，无需单独的批评模型。