就在刚刚，DeepSeek-Prover-V2正式发布。
此次DeepSeek-Prover-V2提供了两种模型尺寸：7B和671B参数。
DeepSeek-Prover-V2-671B：在DeepSeek-V3-Base基础上训练，推理性能最强。
DeepSeek-Prover-V2-7B：基于DeepSeek-Prover-V1.5-Base构建，上下文长度扩展至高达32Ktoken。
Hugging Face：
GitHub：
同时，技术报告也放出了。
论文链接：
昨天，DeepSeek突然在Hugging Face上开源了671B模型，果然很快就有后续了。
数学证明大提升
此次DeepSeek-Prover-V2的训练核心，就是靠「递归+强化学习」。
首先，DeepSeek-V3会拆解复杂定理，生成一系列子目标和推理思路。随后，GRPO算法就会从多种候选方案中自动学习如何选出最优解。
对于这次放出的技术，网友盛赞说，这将导致超越人类的数字AI，极大地推动AI研究。
方法可以总结如下：
· 优化算法，以实现更快、更智能的模型
· 揭示AI「黑盒」行为的洞见
· 设计更好的架构，无需无尽的试错
· 加速数据分析，以实现更快的突破
因此，这就导致我们通向AGI，产生超级智能。几年内，AI就将产生人类无法理解的高级数学。
具体来说，DeepSeek-Prover-V2专门用于Lean 4中的形式化定理证明。
其中，初始化数据是通过DeepSeek-V3驱动的递归定理证明流程来收集的。
冷启动训练过程中，会首先提示DeepSeek-V3将复杂问题分解为一系列子目标，然后将已解决子目标的证明合成为思维链过程，并结合DeepSeek-V3的逐步推理，为强化学习提供了一个初始冷启动。
通过这个过程，非正式和正式的数学推理就能集成到一个统一的模型中。
总结来说，亮点如下。
· 生成冷启动推理数据：递归证明搜索方法
为构建冷启动数据集，团队开发了一个简单而有效的递归定理证明流程，利用 DeepSeek-V3作为统一工具，进行子目标分解和形式化。
DeepSeek-V3会被提示，将定理分解为高层次的证明草图。同时，在Lean 4中形式化这些证明步骤，从而产生一系列子目标。
首先使用一个较小的 7B 模型来处理每个子目标的证明搜索，以此降低计算负担。
一旦具有挑战性的问题的分解步骤得到解决，就将完整的逐步形式化证明与DeepSeek-V3产生的相应思维链过程相结合，从而生成冷启动推理数据。
· 基于合成冷启动数据的强化学习
团队精心挑选了一个具有挑战性的问题子集——它们无法通过7B prover以端到端的方式解决，但分解后的所有子目标都已成功解决。
通过整合所有子目标的证明，团队为原始问题构建了一个完整的形式化证明。
然后，将此证明附加到DeepSeek-V3的思维链中，该思维链概述了相应的引理分解，从而将非正式推理与后续形式化过程有机结合。
在合成冷启动数据上微调prover模型后，团队执行了强化学习阶段，以进一步增强其连接非正式推理与形式化证明构建的能力。
根据推理模型的标准训练目标，采用二元正确/不正确反馈作为主要的奖励监督形式。
最终，模型DeepSeek-Prover-V2-671B在神经定理证明方面实现了当前最优的性能，在MiniF2F-test上达到了88.9%的通过率，并解决了PutnamBench中658个问题中的49个。
DeepSeek-Prover-V2为miniF2F数据集生成的证明：
· 针对AIME与教科书题目的形式化数据集ProverBench
ProverBench是一个包含325道题目的基准数据集。
其中，15道题目源自最近AIME竞赛（AIME 24&25）中的数论和代数题目，提供了极具挑战性的高中竞赛级别题目。
剩余的310道题目则来自精选的教科书例题和教学教程，构建了一个多样化的、具有教学意义的形式化数学题目集合。
因此，这项基准更全面地评估高中竞赛和本科阶段的数学水平。
DeepSeek-Prover-V2
在论文中，团队构建了用于子目标分解的推理模型，利用合成的冷启动数据和大规模强化学习技术来提升其性能。
通过子目标分解实现递归式证明搜索
将复杂定理的证明过程拆解为一系列较小的引理，作为中间步骤，是人类数学家普遍采用的一种高效策略。
近年来，分层式方法在神经定理证明领域得到了广泛应用。它的核心思路是借助现代大型语言模型（LLM）擅长的非形式化推理能力，来提升定理证明搜索的效率。
这部分包括3阶段：从自然语言推理到形式化证明草图、子目标的递归求解、基于子目标的定理证明中的课程学习。
首先提示DeepSeek-V3，同时生成自然语言形式的证明草图，并将其形式化为Lean语言中的定理陈述，其中对于尚未证明的部分使用sorry占位。
接着，7B证明模型用于递归地求解被分解出的各个子目标。通过组合这些子目标的证明内容，团队可以构建出原始复杂问题的完整形式化证明。
冷启动数据收集流程概览
DeepSeek利用子目标来扩展可用于模型训练的形式化定理范围。
他们生成了两种类型的子目标定理：一种包含前序子目标作为前提条件（对应图 3(b)），另一种则不包含前提条件（对应图 3(a)）。
这两种类型的子目标都被纳入到专家迭代阶段，形成一个渐进式的课程体系，引导证明模型逐步掌握解决精选难题的方法。
这一流程的核心思想与AlphaProof 在测试阶段采用的强化学习策略类似：生成目标问题的多种变体，提升模型解决高难度的IMO级别问题的能力。
将分解后的子目标转化为一系列引理（lemma）陈述
首先执行步骤 (a)：将原始目标状态替换为当前子目标。
接着进行步骤 (b)：将之前的子目标作为前提条件纳入当前引理中。
类型 (b) 的陈述用于递归求解复杂问题，而类型 (a) 和 (b) 的陈述都被纳入课程学习流程中，用于训练模型逐步掌握推理能力。
最后，将这个组合后的正式证明附加到 DeepSeek-V3最初生成的「思维链」之上，形成高质量的冷启动训练数据，用于支持形式化数学推理的学习。
统一非形式化推理与形式化证明
算法框架包括两个阶段，分别依赖两个互补模型：用于引理分解的 DeepSeek-V3，以及用于补全具体形式化证明细节的7B证明模型。
这种方法巧妙地融合了高层次的自然语言推理和低层次的精确证明过程，为构建可用于训练的形式化推理数据提供了重要基础。
· 用合成数据实现冷启动
在研究过程中，DeepSeek挑选出一些特别难解决的问题。
这些问题很棘手，即便用7B证明模型，也没办法从头到尾直接解决。
不过有意思的是，把这些问题拆解成一个个小目标后，每个小目标都能被成功证明。就像拼拼图一样，把这些小目标的证明过程按顺序组合起来，就能得到原始难题的完整证明，而且这个证明是非常严谨、规范的形式化证明。
接着，DeepSeek把这个完整的证明，添加到 DeepSeek-V3 生成的 「思维链」 里。
这里的 「思维链」 就像是解题的思路草稿，详细记录了把难题分解成小目标的过程。
这样一来，DeepSeek就得到了一份特殊的证明样本，它既有像日常思考那样的非形式化推理过程，又有严谨的形式化证明步骤，两者完美结合。
通过这种方式，团队成功收集到了几百条高质量的数据。
它们非常重要，是训练 DeepSeek-Prover-V2模型的基础。
这里方法的核心是把日常语言描述的证明过程，直接转化成有逻辑结构的形式化框架。
· 用强化学习提升推理能力
用冷启动合成数据对证明模型进行初步优化后，就进入了强化学习阶段。
强化学习阶段目的是让模型更好地把日常语言的推理过程，转化成严谨的形式化证明。
在这个过程中，按照标准的推理模型训练要求，用 「正确」 或 「错误」 这两种简单的反馈，作为主要的奖励监督信号。也就是说，如果模型给出的证明是对的，就奖励它；如果错了，就不给奖励。
但训练有个问题：模型生成的证明结构，经常和 「思维链」 里分解问题的思路对不上。
为了解决这个问题，在训练刚开始的时候，团队就加入了一种新的奖励机制，专门用来惩罚那些和分解结构不一致的输出结果。
在实际训练中，这个保证结构一致的方法效果非常好，大大提高了证明的准确率。尤其是在证明那些需要很多步骤、特别复杂的定理时，优势更加明显。
训练细节
DeepSeek-Prover-V2的训练采用了两阶段策略，建立了两种互补的证明生成模式：
这两个生成模式的设计延续了DeepSeek-Prover-V1.5的思路，区别在于不同的提示模板。
在第一阶段中，团队结合课程学习框架和专家迭代机制，训练non-CoT证明模型，并通过子目标分解递归地合成复杂问题的证明。
由于non-CoT模式推理速度快、验证成本低，因此非常适合快速迭代与数据采集。
在此基础上，第二阶段引入了冷启动的思维链数据，这些数据整合了DeepSeek-V3的高级数学推理能力与合成的形式化证明。
CoT模式随后进入强化学习阶段，以进一步提升模型在推理和形式化构造之间的衔接能力。
专家迭代（Expert Iteration）
DeepSeek-Prover-V2的non-CoT模型训练采用了「专家迭代」方法，这是目前形式化定理证明系统中广泛使用的训练范式。
论文链接：
每轮训练中，当前性能最好的模型会尝试解决前几轮未成功证明的难题。
成功的证明结果经Lean系统验证后被加入监督微调（SFT）数据集中，用于训练下一代更强的模型。
这个过程不仅让模型持续从初始演示数据中学习，还能提炼自身的成功推理路径，不断优化解决难题的能力。
DeepSeek-Prover-V2整体训练流程与V1和V1.5保持一致，只在训练问题的分布上做了两处改进：
监督微调（Supervised Fine-tuning）
团队在DeepSeek-V3-Base-671B的基础上进行微调，学习率设置为常数5e-6，最大上下文长度为16,384 token。