本文转载自微信公众号：中信建投证券研究
文｜于芳博
1. 4月30日，DeepSeek在 Hugging Face 上发布名为 DeepSeek-Prover-V2-671B 的新模型，此模型是专为“数学AI推理”中的形式化定理证明打造的开源大语言模型，目前在定理证明赛道上实现了业内最佳性能。
2. DeepSeek-Prover-V2通过递归定理证明流程，首次实现自然语言推理与形式化验证的闭环协同，通过生成人类可理解的思维链（CoT）与机器可执行的Lean4代码（Non-CoT）的协同互补，标志AI在数学推理领域实现直觉思维与符号逻辑的双向对齐。
3. 通过32k上下文强化学习轨迹迁移与Non-CoT/CoT数据混合蒸馏，团队将671B模型的数学推理能力高效迁移至7B轻量模型，为边缘计算场景下的高效形式化验证提供新思路。
点击小程序查看报告原文
DeepSeek开源DeepSeek-Prover-V2
4月30日，深度求索（DeepSeek）在 AI 开源社区 Hugging Face 上，发布名为 DeepSeek-Prover-V2-671B 的新模型，随后在 GitHub 等平台上公布了技术论文信息。据论文介绍，DeepSeek-Prover-V2是一个专为“数学AI推理”Lean 4中的形式化定理证明打造的开源大语言模型，目前在定理证明赛道上实现了业内最佳性能：DeepSeek-Prover-V2-671B在 MiniF2F 测试中达到了 88.9% 的通过率，并成功解决了 PutnamBench 数据集中 658 道题中的 49 道，在 AIME 24、25 上也取得较高分数。
此次，DeepSeek 团队发布了两个版本的 DeepSeek-Prover-V2 模型，参数规模分别为 7B 和 671B。其中，DeepSeek-Prover-V2-671B 是在DeepSeek-V3-Base 基础上训练而成，而 DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5-Base 构建，并支持最长 32K tokens 的上下文长度扩展。
在数据初始化阶段，DeepSeek-Prover-V2通过 DeepSeek-V3 驱动的递归定理证明流程完成原始数据采集。在冷启动过程中，首先通过分层推理引导，提示引导 DeepSeek-V3将复杂数学命题拆解为高层次的证明草图，并在此过程中同时将这些推理步骤用 Lean 4 语言形式化，最终生成一系列结构清晰、逻辑严密的子目标。为了降低计算开销，DeepSeek团队使用了更小的 7B 模型来完成每个子目标的证明搜索，从而降低计算负担。每个子问题的求解结果会被编码为结构化逻辑单元，进而组合成具备因果关联的推理思维链，并融合 DeepSeek-V3 的分布推导路径，最终将两类数据融合构建强化学习的初始训练数据。在对证明模型进行合成冷启动数据的微调后，研究团队进一步引入强化学习阶段，进一步提升模型将非形式化推理转化为形式化证明的能力。在训练过程中，遵循推理模型的通用目标，采用「对 / 错」二值反馈作为主要的奖励信号。
通过此训练方法，可以将非形式化和形式化的数学推理融合到一个统一的模型中，使模型同时具备人类数学家的直觉化能力，以及形式化验证系统所需的符号逻辑执行能力，在保持思维弹性的同时满足数学证明的严格性要求。
DeepSeek-Prover-V2 经历两阶段训练，在证明生成模式建立上形成互补：
1. 高效非思维链（non-CoT）模式：系统基于专家迭代框架构建极速验证模式——通过课程学习策略，利用扩展数据集（融合自动形式化问题与子目标分解新题）训练non-CoT模型，使其直接生成无中间推理的Lean4代码，显著提升高复杂度问题的响应效率。
2. 高精度思维链（CoT）模式：引入认知增强引擎，将DeepSeek-V3的数学直觉提炼为结构化思维链，结合GRPO强化学习算法进行策略优化，通过二值验证反馈驱动模型对齐形式化验证的严格逻辑约束。
与PPO不同，GRPO 强化学习算法通过为每个定理提示采样一组候选证明并根据它们的相对奖励优化策略，消除对单独批评模型的需求。采用二元奖励机制，每个生成的 Lean 证明如果被验证为正确则获得 1 个奖励，否则为 0。模型在每次迭代中采样 256 个不同的问题，为每个定理生成 32 个候选证明，最大序列长度为 32768 个 token。
在模型蒸馏阶段，研究人员将 DeepSeek-Prover-V1.5-Base-7B 的最大上下文长度从 4096个 token 扩展到了 32768 个，并基于 DeepSeek-Prover-V2-671B 强化学习阶段收集的rollout 数据对扩展上下文模型进行微调。除了 CoT 推理模式外，研究人员还整合了专家迭代过程中收集的非 CoT 证明数据，以实现一种成本效益高的证明选项，该选项能够生成简洁的形式化输出，并且模型规模较小。此外，7B 模型也采用了与 671B 模型训练相同的强化学习阶段以提升性能。
研究人员对DeepSeek-Prover-V2 在形式定理证明的各种基准数据集上进行了系统评估，涵盖了高中竞赛题目和本科水平的数学问题。结果表明，671B 版的模型实现了前所未有的准确率，效率领先于业内其他先进模型。
北美经济衰退预期逐步增强，宏观环境存在较大的不确定性，国际环境变化影响供应链及海外拓展；芯片紧缺可能影响相关公司的正常生产和交付，公司出货不及预期；下游需求不及预期影响公司正常生产和交付，导致收入及增速不及预期；信息化和数字化方面的需求和资本开支不及预期；市场竞争加剧，导致毛利率快速下滑；主要原材料价格上涨，导致毛利率不及预期；汇率波动影响外向型企业的汇兑收益与毛利率；人工智能技术进步不及预期；汽车与工业智能化进展不及预期。
于芳博：中信建投人工智能组首席分析师，北京大学空间物理学学士、硕士，2019年7月加入中信建投，主要覆盖人工智能等方向，下游重点包括智能汽车、CPU/GPU/FPGA/ASIC、EDA和工业软件等方向。
证券研究报告名称：《DeepSeek开源Prover-V2强推理模型：递归强化学习提升数学能力》
对外发布时间：2025年5月8日
报告发布机构：中信建投证券股份有限公司
本报告分析师：
于芳博 SAC 编号:S1440522030001