人工智能行业DeepSeek开源Prover-V2强推理模型：递归强化学习提升数学能力

本报告由中信建投证券股份有限公司在中华人民共和国（仅为本报告目的，不包括香港、澳门、台湾）提供。在遵守适用的法律法规情况下，本报告亦可能由中信建投（国际）证券有限公司在香港提供。同时请务必阅读正文之后的免责条款和声明。 证券研究报告·行业动态 DeepSeek 开源 Prover-V2 强推理模型：递归强化学习提升数学能力 核心观点 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 轻量模型，为边缘计算场景下的高效形式化验证提供新思路。 产业要闻 【百度发布文心大模型 4.5 Turbo 和 X1 Turbo】【Kimi 发布了开源项目 Kimi-Audio】【Qwen3 系列模型正式发布】【苹果计划在iPhone 17 系列中大规模应用 AI 技术】【荣耀 400 和荣耀 400 Pro 通过国家质量认证】【特斯拉启动 Robotaxi 业务测试】相关公司： GPU：英伟达、超威半导体、海光信息等； FPGA：安路科技-U 等； SoC：高通、全志科技等； 自然语言处理：科大讯飞等； 计算机视觉：格灵深瞳-U 等； 自动驾驶：德赛西威、中科创达、均胜电子、光庭信息； 智慧交通：千方科技、万集科技； AI+工业：中控技术、华大九天、广立微、概伦电子等。 风险提示：北美经济衰退预期逐步增强，宏观环境存在较大的不确定性，国际环境变化影响供应链及海外拓展；芯片紧缺 可能影响相关公司的正常生产和交付，公司出货不及预期。 维持 强于大市 于芳博 yufangbo@csc.com.cn 010-86451607 SAC 编号:S1440522030001 发布日期： 2025 年 05 月 08 日 市场表现 相关研究报告 -17%3%23%43%63%83%2024/4/222024/5/222024/6/222024/7/222024/8/222024/9/222024/10/222024/11/222024/12/222025/1/222025/2/222025/3/22计算机上证指数人工智能 计 算机设备 行业动态报告 请务必阅读正文之后的免责条款和声明。 目录 一、 行业变化 ................................................................................................................................................................................... 1 二、相关标的......................................................................................................................................................................................... 3 三、行情回顾......................................................................................................................................................................................... 4 四、产业要闻......................................................................................................................................................................................... 5 五、重要公告......................................................................................................................................................................................... 6 六、风险分析......................................................................................................................................................................................... 6 1 计 算机设备 行业动态报告 请务必阅读正文之后的免责条款和声明。 一、 行业变化 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 的上下文长度扩展。 图表1： 模型性能对比