DeepSeek-Prover-V2：通过强化学习实现子目标分解以提升形式化数学推理能力
计算与语言
2025-07-21 v2 人工智能
摘要
我们介绍了 DeepSeek-Prover-V2，这是一个用于形式定理证明的开源大型语言模型，其初始化数据通过基于 DeepSeek-V3 的递归定理证明管道收集。冷启动训练程序开始通过提示 DeepSeek-V3 将复杂问题分解为一系列子目标。将已解决子目标的证明与 DeepSeek-V3 的逐步推理相结合，形成链式思维过程，以创建强化学习的初始冷启动。这一过程使我们能够将非形式化和形式化数学推理整合到统一的模型中。所得模型 DeepSeek-Prover-V2-671B 在神经定理证明中实现了最先进的性能，MiniF2F-test 通过率达到 88.9%，并解决了 PutnamBench 中 49 个 658 个问题之一。除了标准基准测试之外，我们还引入了 ProverBench，这是一个包含 325 个形式化问题的集合，其中包括来自近期 AIME 竞赛（2024-2025 年）的 15 个精选问题。进一步评估这 15 个 AIME 问题显示，模型成功解决了其中 6 个。与此相比，DeepSeek-V3 使用多数投票解决了其中 8 个问题，凸显了大型语言模型中形式化与非形式化数学推理之间的差距正在显著缩小。
引用
@article{arxiv.2504.21801,
title = {DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition},
author = {Z. Z. Ren and Zhihong Shao and Junxiao Song and Huajian Xin and Haocheng Wang and Wanjia Zhao and Liyue Zhang and Zhe Fu and Qihao Zhu and Dejian Yang and Z. F. Wu and Zhibin Gou and Shirong Ma and Hongxuan Tang and Yuxuan Liu and Wenjun Gao and Daya Guo and Chong Ruan},
journal= {arXiv preprint arXiv:2504.21801},
year = {2025}
}