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