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

我们推出了 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 通过多数投票解决了这 15 个问题中的 8 个，这突出显示了大语言模型在形式化与非形式化数学推理之间的差距正在显著缩小。

该论文试图解决在形式化数学推理中，如何通过大型语言模型生成高质量的定理证明问题。这是一个相对较新的研究方向，特别是在结合非形式化和形式化推理方面。

论文的关键思路是通过递归定理证明管道从DeepSeek-V3收集初始化数据，并利用链式思维过程将复杂问题分解为子目标，从而实现冷启动训练。此外，通过强化学习整合非形式化和形式化推理，最终构建出高性能的形式化定理证明模型DeepSeek-Prover-V2-671B。

该模型在MiniF2F-test上达到88.9%的通过率，并成功解决了PutnamBench中的49个问题。论文还引入了ProverBench数据集，包括15个来自AIME竞赛的问题，其中DeepSeek-Prover-V2解决了6个问题，而DeepSeek-V3解决了8个。实验设计严谨，使用了多个标准基准测试，并开源了代码，这为未来的研究提供了宝贵的资源。

最近的相关研究包括：1) GPT-f，一种基于GPT架构的神经定理证明器；2) LeanDojo，一个用于形式化数学教育和研究的工具；3) MiniF2F，一个评估形式化定理证明的标准基准。其他相关工作还包括AlphaTensor（在张量分解中的应用）和Lamore（大规模形式化推理）。