本文提出DeepSeek-Prover-V2，通过子目标分解和强化学习统一非正式和正式数学推理，显著提升了神经定理证明的性能，在多个基准上达到最先进水平。
Reinforcement Learning, Reasoning, Large Language Model, Pre-training, Fine-tuning
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
Generated by grok-3-mini-latest
Background Problem
大型语言模型（LLMs）在非正式数学推理中表现出色，能够处理自然语言中的推理任务，但正式定理证明需要严格的逻辑结构和无歧义的证明步骤，这与LLMs的启发式和近似方法存在显著差距。本文的工作起点是桥接这一差距，通过利用非正式推理指导正式证明，解决的关键问题是提升神经定理证明的性能，特别是针对复杂定理的分解和求解，以实现更高效和准确的自动定理证明。
Method
- 核心思想： 通过将复杂定理分解为子目标，并结合强化学习，统一非正式数学推理和正式证明结构，旨在在不牺牲推理能力的情况下提升定理证明的准确性和效率。
- 工作原理： 首先，使用DeepSeek-V3生成自然语言证明草图并将其形式化为Lean 4中的子目标序列；然后，采用递归求解策略，通过一个较小的7B模型解决这些子目标；接着，通过课程学习框架生成合成数据，包括子目标定理的变体；最后，应用强化学习（使用Group Relative Policy Optimization算法）来优化模型，使其更好地桥接非正式推理和正式证明。
- 主要步骤： 1. 子目标分解：提示DeepSeek-V3生成证明草图和Lean语句；2. 递归求解：使用小型模型解决分解后的子目标；3. 冷启动数据合成：将解决的子目标证明与DeepSeek-V3的推理链结合；4. 强化学习阶段：基于二元奖励和一致性奖励训练模型，以改进证明结构。
Experiment
- 数据集和实验设置： 本文在多个基准上评估模型，包括MiniF2F（高中竞赛问题）、ProofNet（本科数学问题）、PutnamBench（大学竞赛问题）、CombiBench（组合问题）和新提出的ProverBench（包括AIME问题）。实验使用不同模型大小（7B和671B），并比较Chain-of-Thought (CoT) 和非CoT模式。设置合理全面，包含了从监督微调到强化学习的训练流程，以及与基线模型的对比（如Kimina-Prover、STP等）。
- 结果分析： 模型在MiniF2F-test上达到88.9%的Pass@8192准确率，显著优于现有方法；在ProofNet和PutnamBench上也表现出色，解决了49个PutnamBench问题。结果符合预期，证明了子目标分解和强化学习的有效性，尤其是在CoT模式下性能提升明显。实验还展示了模型在不同难度和主题下的泛化能力，以及较小模型在特定问题上的独特技能发现。
- 是否匹配预期： 是，实验结果显示方法改进明显，证明了通过强化学习和子目标分解可以显著提升正式定理证明的性能，且实验设计考虑了计算开销和可扩展性。
Further Thoughts
本文的方法展示了如何通过强化学习和子目标分解来桥接非正式和正式推理，这可能启发其他领域如代码验证或逻辑推理任务的应用；此外，随着模型规模的增加，推理能力的提升表明未来可以探索更复杂的证明策略，例如结合符号方法或多模态数据，以进一步缩小AI在数学推理中的人类水平差距，并可能扩展到其他证明助手如Coq或Isabelle中。