DeepSeek开源Prover-V2强推理模型，网友：奥数从没这么简单过

AIGC动态11小时前发布 almosthuman2014

90 0 0

文章摘要

DeepSeek团队在五一劳动节期间发布了DeepSeek-Prover-V2，这是一款专为数学AI编程语言Lean 4打造的开源大语言模型，专注于形式化定理证明。该模型在定理证明赛道上实现了业内最佳性能，在MiniF2F测试中达到了88.9%的通过率，并在AIME 24、25上也有不错的表现。DeepSeek-Prover-V2有两个版本，参数规模分别为7B和671B，其中671B版本在DeepSeek-V3-Base基础上训练而成，而7B版本则基于DeepSeek-Prover-V1.5-Base构建，并支持最长32K tokens的上下文长度扩展。

DeepSeek-Prover-V2的核心创新在于其递归定理证明流程，该流程通过DeepSeek-V3驱动的递归定理证明收集初始化数据。在冷启动训练阶段，模型首先通过提示DeepSeek-V3将复杂问题分解成一系列可以解决的子目标，每解决一个子目标就会将这些证明整合成“思维链”，并融合DeepSeek-V3的逐步推理轨迹，共同构建出用于强化学习的初始训练数据。这一策略将非形式化和形式化的数学推理融合到一个统一的模型中，实现了数学推理的一体化融合。

为了降低计算开销，DeepSeek团队使用一个更小的7B模型来完成每个子目标的证明搜索。当复杂问题被拆解的各个步骤都成功解决后，他们将完整的形式化逐步证明与DeepSeek-V3生成的思维链相对应，组合成冷启动推理数据。随后，研究团队进一步引入强化学习阶段，提升模型将非形式化推理转化为形式化证明的能力。最终得到的DeepSeek-Prover-V2-671B在神经定理证明任务中达到了当前最先进的性能，成功解决了PutnamBench数据集中658道题中的49道。

DeepSeek-Prover-V2的训练过程分为两阶段，建立了高效非思维链（non-CoT）模式和高精度思维链（CoT）模式。非CoT模式针对快速生成正式的Lean证明代码进行优化，而CoT模式则系统地阐述中间推理步骤，强调透明度和逻辑进展。研究人员在DeepSeek-V3-Base-671B上使用恒定的学习率5e-6，在16384个token的上下文中进行监督微调。训练语料库由两个互补来源组成：通过专家迭代收集的非CoT数据和冷启动CoT数据。

此外，DeepSeek还发布了ProverBench，这是一个包含325道题目的基准数据集，旨在支持对模型在高中竞赛题和本科数学题两个层面的综合评估。该数据集的15道题来自最近两届AIME数学竞赛中的数论与代数题目，其余310道题则精选自教材示例和教学教程。

DeepSeek-Prover-V2的发布引发了广泛关注，不少网友对其处理复杂问题的能力表示赞赏，并期待其在代码等领域的应用。尽管DeepSeek-R2的发布仍然备受期待，但DeepSeek-Prover-V2的推出无疑在数学推理和定理证明领域树立了新的标杆。