报告行业投资评级 - 推荐（维持），预期未来 3 - 6 个月内该行业指数涨幅超过基准指数 5%以上 [4][20] 报告的核心观点 - 4 月 30 日，DeepSeek 发布 DeepSeek - Prover - V2 - 671B 新模型、DeepSeek - Prover - V2 - 7B 增强模型及 DeepSeek - ProverBench 数据集并公布论文信息 [2] - 新模型专注数学定理证明，采用特定架构、参数和技术，实现形式化与非形式化数学证明融合，创新推理训练流程，定理证明达业内最佳 [7] - 国内 AI 数学推理达新高度，建议关注国产算力、AI 应用与 AI 安全等领域投资机遇，并列出多领域建议关注公司 [7] 根据相关目录分别进行总结 行业基本数据 - 股票家数 336 只，占比 0.04%；总市值 42,657.40 亿元，占比 4.41%；流通市值 36,398.85 亿元，占比 4.74% [4] 相对指数表现 - 1 个月绝对表现 - 5.3%，相对表现 - 1.6%；6 个月绝对表现 2.3%，相对表现 5.4%；12 个月绝对表现 27.0%，相对表现 22.4% [5] 新模型特点 - DeepSeek - Prover - V2 - 671B 采用和 DeepSeek V3 - 0324 相同架构，参数 6710 亿，用 MoE 模式，有 61 层 Transformer 层等，支持超长上下文及多种计算精度，用 safetensors 格式优化训练部署，通过 FP8 量化技术提高推理效率 [7] - 自 2024 年 3 月以来，DeepSeek - Prover 系列已推出 3 款模型，DeepSeek - Prover - V2 进一步提出“子目标分解的强化学习”，基础模型升级到 DeepSeek - V3 [7] - 采用“递归定理证明流程”和两阶段训练策略，减轻计算负担，构建最终形式证明 [7] - DeepSeek - Prover - V2 - 671B 在神经定理证明领域创新高，7B 模型解决部分大模型未攻克问题，形式与非形式数学能力差距缩小 [7] 投资建议 - 建议关注国产算力、AI 应用与 AI 安全等领域投资机遇，涉及办公、金融、大模型等 18 个领域多家公司 [7] 受益标的梳理 - 报告列出海光信息、寒武纪 - U 等多家公司 2024A、2025E 的营收、归母净利润、PE、PS 等数据 [8][9]

DeepSeek-Prover-V2发布 - 公司发布DeepSeek-Prover-V2模型，包含7B和671B两个参数版本，专注于形式化定理证明，专为数学AI编程语言Lean 4打造 [3] - DeepSeek-Prover-V2-671B基于DeepSeek-V3-Base训练，7B版本基于DeepSeek-Prover-V1.5-Base构建，支持32K tokens上下文长度 [3] - 模型在MiniF2F测试中达到88.9%通过率，解决PutnamBench数据集中658道题中的49道，性能达到业内最佳 [15] 技术实现 - 采用递归定理证明流程，使用DeepSeek-V3分解复杂问题为子目标并生成形式化推理步骤，融合非形式化与形式化数学推理 [9][4] - 通过7B模型完成子目标证明以降低计算开销，整合子目标证明与DeepSeek-V3生成的思维链构建冷启动数据 [11] - 采用两阶段训练：非思维链（non-CoT）模式优化快速生成Lean代码，思维链（CoT）模式强调透明推理步骤 [17] 性能与基准测试 - DeepSeek-Prover-V2-671B在ProofNet-test上通过率37.1%（1024样本），PutnamBench解决49/658题，显著优于Goedel-Prover-SFT和STP等竞品 [23] - 7B版本在ProofNet-test通过率29.6%（1024样本），PutnamBench解决11/658题，展示小模型的高效性能 [23] - 发布ProverBench基准数据集，包含325道题目，涵盖AIME竞赛题及本科数学内容，支持高中至本科难度评估 [25][26] 行业影响 - 模型开源并公开技术细节，HuggingFace平台提供7B和671B版本下载链接，推动数学AI领域发展 [6][16] - 用户实测显示模型效果优于o4-mini和Grok-3，尤其在数学奥林匹克问题解决中表现突出 [31] - 子目标分解与推理融合的设计被类比为初级工程师问题解决技巧，潜在适用于代码生成等场景 [32]

模型发布与版本 - DeepSeek在Hugging Face正式发布DeepSeek-Prover-V2，同步上线模型卡及示例代码，共推出两个版本：7B和671B [1][4] - DeepSeek-Prover-V2-7B基于上一代V1.5模型，支持最长32K上下文输入 [4] - DeepSeek-Prover-V2-671B在DeepSeek-V3-Base基础上训练，推理性能最强 [4] 训练方法与技术 - 训练核心采用"递归+强化学习"组合，由DeepSeek-V3拆解复杂定理生成子目标和推理思路，再通过GRPO算法从候选方案中学习最优解 [3] - 训练分为两阶段：第一阶段采用"专家迭代"方法，模型通过解决难题反哺自身 [5]；第二阶段迁移DeepSeek-V3数学知识并引入形式化数据，构建复杂推理路径 [6] - GRPO强化学习算法引导模型在32个候选证明方案中选择被Lean验证系统判定为正确的答案（奖励1分，否则0分） [8][9] 模型能力与特点 - 671B模型能力被"蒸馏"到7B模型，使小模型在资源有限设备上获得接近大模型的数学推理能力 [10][11] - 提供两种解题风格：快速模式（non-CoT）直接生成精炼答案；逻辑模式（CoT）详细展示推理过程 [12] - DeepSeek-V3负责拆解定理生成推理草图，7B模型完成子证明并拼接完整推理，形成"模糊思考+精确证明"机制 [14][15] 性能评估与数据集 - DeepSeek-Prover-V2-671B在MiniF2F测试中通过率达88.9%，成功解出PutnamBench数据集49道难题 [17] - 推出全新数学形式化数据集ProverBench，包含325道题目，涵盖AIME竞赛题、数论、代数、微积分等10个领域 [18][19] - 在15道AIME竞赛题中，DeepSeek-Prover-V2解出6道，DeepSeek-V3通过多数投票解决8道 [20] 行业趋势与方向 - 大型语言模型在"非正式数学推理"与"正式数学推理"间的表现差距明显缩小，逐步学会写出规范可验证的数学证明 [21][22] - 模型从生成内容迈向生成结构化逻辑，可能最早触碰通用人工智能的底层结构，推理能力成为知识系统边界的关键 [32][33][34] 商业化与部署 - 新模型遵循公开许可证，可通过Hugging Face平台免费下载并支持Transformers接口部署 [23][24] - Novita AI成为首批上线Prover-V2-671B推理服务的第三方提供商 [24]