深夜突袭，DeepSeek-Prover-V2加冕数学王者！671B数学推理逆天狂飙

96 0 0

文章摘要

DeepSeek-Prover-V2的发布标志着数学推理领域的一次重大突破。该模型通过递归+强化学习的训练方法，显著提升了其在形式化定理证明中的表现。DeepSeek-Prover-V2提供了两种模型尺寸：7B和671B参数，其中671B模型在推理性能上表现尤为突出。模型的训练核心在于将复杂定理分解为一系列子目标，并通过GRPO算法从多种候选方案中自动选择最优解。这一方法不仅优化了算法，还揭示了AI“黑盒”行为的洞见，设计出更好的架构，无需无尽的试错，从而加速了数据分析的突破。

递归证明搜索方法是DeepSeek-Prover-V2的一大亮点。团队开发了一个简单而有效的递归定理证明流程，利用DeepSeek-V3进行子目标分解和形式化。通过将定理分解为高层次的证明草图，并在Lean 4中形式化这些证明步骤，生成一系列子目标。较小的7B模型用于处理每个子目标的证明搜索，降低计算负担。一旦分解步骤得到解决，完整的逐步形式化证明与DeepSeek-V3产生的思维链过程相结合，生成冷启动推理数据。

强化学习进一步提升了模型的性能。团队精心挑选了一个具有挑战性的问题子集，通过整合所有子目标的证明，为原始问题构建了一个完整的形式化证明。将此证明附加到DeepSeek-V3的思维链中，将非正式推理与形式化过程有机结合。在合成冷启动数据上微调prover模型后，执行强化学习阶段，进一步增强其连接非正式推理与形式化证明构建的能力。最终，DeepSeek-Prover-V2-671B在神经定理证明方面实现了当前最优的性能，在MiniF2F-test上达到了88.9%的通过率，并解决了PutnamBench中658个问题中的49个。

ProverBench是一个包含325道题目的基准数据集，其中15道题目源自最近AIME竞赛中的数论和代数题目，提供了极具挑战性的高中竞赛级别题目。剩余的310道题目则来自精选的教科书例题和教学教程，构建了一个多样化的、具有教学意义的形式化数学题目集合。这一基准更全面地评估高中竞赛和本科阶段的数学水平。

DeepSeek-Prover-V2的训练采用了两阶段策略，建立了两种互补的证明生成模式：高效率非思维链（non-CoT）模式和高精度思维链（CoT）模式。non-CoT模式优化用于快速生成Lean形式化代码，而CoT模式注重系统化表达推理过程，逐步构建逻辑清晰的中间步骤，最后生成完整的形式化证明。专家迭代方法在训练中得到了广泛应用，每轮训练中，当前性能最好的模型会尝试解决前几轮未成功证明的难题，成功的证明结果经Lean系统验证后被加入监督微调（SFT）数据集中，用于训练下一代更强的模型。

在MiniF2F基准测试中，DeepSeek-Prover-V2-671B取得了SOTA性能，当采用CoT生成策略时，仅用32个样本便达到了前所未有的82.4%的准确率。参数效率更高的DeepSeek-Prover-V2-7B也展现出了很强的竞争力，超越了现有文献中的所有开源定理证明器。子目标引导的课程学习框架在难题证明中得到了有效应用，通过巧妙的子目标分解，模型将难题分解为一系列可处理的步骤，从而有效连接非正式推理与形式化证明构建。

在本科水平基准测试中，DeepSeek-Prover-V2在ProofNet和PutnamBench中展现了强大的泛化能力，解决了49道题目，并显著优于其non-CoT版本。7B模型在PutnamBench数据集上采用non-CoT生成模式时，也表现出了卓越的性能，成功解决了671B模型仍未能解决的13道题。这表明，CoT推理方法已经可以有效处理极有挑战性的大学数学问题。

CombiBench是一个综合性的基准测试集，其中包含了100道用Lean 4形式化表示的组合竞赛题。尽管该Prover模型主要在数论和代数领域进行训练，但在组合问题上也展现出了良好的泛化潜力，成功解决了12道题。ProverBench数据集进一步增强了现有基准，涵盖了高中竞赛和本科阶段的数学水平。

DeepSeek-Prover-V2的成功不仅在于其技术上的创新，更在于其将非形式化推理与形式化证明有机结合的能力。通过递归证明搜索和强化学习，模型在数学推理领域取得了显著进展，为未来的自动定理证明研究奠定了坚实的基础。