请务必阅读正文之后的免责条款和声明。

请务必阅读正文之后的免责条款和声明。

目录

TOC\o1-1\h\z\u一、 行业变化 1

二、相关标的 3

三、行情回顾 4

四、产业要闻 5

五、重要公告 6

六、风险分析 6

一、行业变化

DeepSeek开源DeepSeek-Prover-V2

4月30日，深度求索（DeepSeek）在AI开源社区HuggingFace上，发布名为DeepSeek-Prover-V2-671B的新模型，随后在GitHub等平台上公布了技术论文信息。据论文介绍，DeepSeek-Prover-V2是一个专为“数学AI推理”Lean4中的形式化定理证明打造的开源大语言模型，目前在定理证明赛道上实现了业内最佳性能：DeepSeek-Prover-V2-671B在MiniF2F测试中达到了88.9%的通过率，并成功解决了PutnamBench数据集中658道题中的49道，在AIME24、25上也取得较高分数。

此次，DeepSeek团队发布了两个版本的DeepSeek-Prover-V2模型，参数规模分别为7B和671B。其中，DeepSeek-Prover-V2-671B是在DeepSeek-V3-Base基础上训练而成，而DeepSeek-Prover-V2-7B则基于DeepSeek-Prover-V1.5-Base构建，并支持最长32Ktokens的上下文长度扩展。

图表1：模型性能对比

DeepSeek，

请务必阅读正文之后的免责条款和声明。在数据初始化阶段，DeepSeek-Prover-V2通过DeepSeek-V3驱动的递归定理证明流程完成原始数据采集。在冷启动过程中，首先通过分层推理引导，提示引导DeepSeek-V3将复杂数学命题拆解为高层次的证明草图，并在此过程中同时将这些推理步骤用Lean4语言形式化，最终生成一系列结构清晰、逻辑严密的子目标。为了降低计算开销，DeepSeek团队使用了更小的7B模型来完成每个子目标的证明搜索，从而降低计算负担。每个子问题的求解结果会被编码为结构化逻辑单元，进而组合成具备因果关联的推理思维链，并融合DeepSeek-V3的分布推导路径，最终将两类数据融合构建强化学习的初始训练数据。在对证明模型进行合成冷启动数据的微调后，研究团队进一步引入强化学习阶段，进一步提升模型将非形式化推理转化为形式化证明的能力。在训练过程中，遵循推理模型的通用目标，采用「对/错」二值反馈作为主要的奖励信号。

请务必阅读正文之后的免责条款和声明。

通过此训练方法，可以将非形式化和形式化的数学推理融合到一个统一的模型中，使模型同时具备人类数学家的直觉化能力，以及形式化验证系统所需的符号逻辑执行能力，在保持思维弹性的同时满足数学证明的严格性要求。

图表2：DeepSeek-Prover-V2使用冷启动数据收集过程概览

DeepSeek，机器之心，

DeepSeek-Prover-V2经历两阶段训练，在证明生成模式建立上形成互补：

高效非思维链（non-CoT）模式：系统基于专家迭代框架构建极速验证模式——通过课程学习策略，利用扩展数据集（融合自动形式化问题与子目标分解新题）训练non-CoT模型，使其直接生成无中间推理的Lean4

代码，显著提升高复杂度问题的响应效率。

高精度思维链（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证明数据，以实现一种成本效益高的证明选项，该选项能够生成简洁的形式化输出，并且模型规模较小。此