【华鑫证券】计算机行业周报：DeepSeek-Prover-V2创数学推理新高，阿里通义千问推出Qwen3模型-250507（15页）.pdf

1、 20252025 年年 0505 月月 0707 日日 DeepSeekDeepSeek-ProverProver-V2 V2 创数学推理新高，创数学推理新高，阿里通阿里通义千问推出义千问推出 Qwen3Qwen3 模型模型 计算机计算机行业周报行业周报 推荐推荐(维持维持)投资要点投资要点 分析师：宝幼琛分析师：宝幼琛 S1050521110002 行业相对表现行业相对表现 表现 1M 3M 12M 计算机(申万)14.6-4.4 27.8 沪深 300 6.1-2.2 4.1 市场表现市场表现 资料来源：Wind，华鑫证券研究 相关研究相关研究 1、计算机行业周报：豆包 1.5 模型发布

2、，微信 AI 助手“元宝”上线2025-04-23 2、计算机行业周报：ChatGPT 升级长期记忆功能，谷歌发布跨平台AI 协作协议 A2A2025-04-16 3、计算机行业周报：Llama4 多版本参数亮眼，DeepSeek 公布推理时Scaling 新论文2025-04-08 算力：算力租赁价格平稳，DeepSeek-Prover-V2 创数学推理新高 4 月 30 日，DeepSeek 发布名为 DeepSeek-Prover-V2 的数学推理模型，提供 7B 和 671B 两种参数规模。在多个标准基准测试中，DeepSeek-Prover-V2-671B 都取得了神经定理证明领域的

3、最先进性能水平。并且，面对从著名的 AIME 竞赛（2024-2025 年）中挑选的 15 个问题，该模型成功解出了其中的 6 个。DeepSeek-Prover-V2 通过两阶段训练流程开发，建立了两种互补的证明生成模式：（1）高效非思维链（non-CoT）模式：此模式针对快速生成形式化 Lean 证明代码进行了优化，专注于在不显示中间推理步骤的情况下生成简洁的证明。（2）高精度思维链（CoT）模式：此模式在构建最终形式化证明之前，系统地阐述中间推理步骤，强调透明度和逻辑进展。与 DeepSeek-Prover-V1.5 一致，DeepSeek-Prover-V2 的两种生成模式由两个不同的

4、引导提示控制。在第一阶段，DeepSeek 团队在课程学习框架内使用专家迭代范式来训练非思维链证明模型，同时通过基于子目标的递归证明为难题合成证明。选择非思维链生成模式是为了加速迭代训练和数据收集过程，因为它提供了明显更快的推理和验证周期。在此基础上，第二阶段利用了通过将 DeepSeek-V3 复杂的数学推理模式与合成形式证明相结合而生成的冷启动链式思维链数据。CoT 模式通过进一步的强化学习阶段得到增强，遵循推理模型常用的标准训练流程。在性能测评环节中，DeepSeek 团队用定理证明基准数据集，对 DeepSeek-Prover-V2 进行系统评估，测试覆盖高中竞赛和本科数学知识。结果显

5、示，即便训练数据多为高中数学题，该模型仍能良好泛化到大学水平问题，体现出强大的形式化推理能力。AI 应用：Gemini 平均停留时长环比+3.45%，阿里通义千问推出 Qwen3 模型 4 月 29 日，阿里通义千问宣布推出 Qwen 系列大型语言模型的最新成员Qwen3。阿里通义千问的旗舰模型 Qwen3-235B-40-200204060(%)计算机沪深300证证券券研研究究报报告告 行行业业研研究究 证券研究报告证券研究报告 请阅读最后一页重要免责声明 2 诚信、专业、稳健、高效 A22B 在代码、数学、通用能力等基准测试中，与 DeepSeek-R1、o1、o3-mini、Grok-3

6、 和 Gemini-2.5-Pro 等顶级模型相比，表现出极具竞争力的结果。此外，小型 MoE 模型 Qwen3-30B-A3B 的激活参数数量是 QwQ-32B 的 10%，表现更胜一筹，甚至像 Qwen3-4B 这样的小模型也能匹敌 Qwen2.5-72B-Instruct 的性能。Qwen3 模型支持两种思考模式：思考模式：在这种模式下，模型会逐步推理，经过深思熟虑后给出最终答案。这种方法非常适合需要深入思考的复杂问题。非思考模式：在此模式中，模型提供快速、近乎即时的响应，适用于那些对速度要求高于深度的简单问题。这种灵活性使用户能够根据具体任务控制模型进行“思考”的程度。例如，复杂的问题