--- type: "article" id: 10225320 title: "梁文锋和杨植麟再“撞车”" canonical: "https://www.yfchuhai.com/article/10225320.html" published: "2025-05-05T11:05:08+08:00" author: "中国企业家杂志" tags: [] summary: "梁文锋所在的DeepSeek和杨植麟所在的月之暗面在大模型领域展开激烈竞争。DeepSeek于4月30日上线了数学定理证明专用模型DeepSeek-Prover-V2，参数规模达671B，性能显著提升；而月之暗面在4月中旬推出了Kimina-Prover，参数规模较小，性能在某些测试上稍逊一筹。" publisher: "扬帆出海" publisher_url: "https://www.yfchuhai.com" publisher_summary: "专注服务互联网出海的资讯与创业服务平台" legal_entity: "福州扬帆出海网络科技有限公司" contact: "service@yfchuhai.com" brand_tagline: "扬帆出海 — 专注服务互联网出海" lang: "zh-CN" --- # 梁文锋和杨植麟再“撞车” > 梁文锋所在的DeepSeek和杨植麟所在的月之暗面在大模型领域展开激烈竞争。DeepSeek于4月30日上线了数学定理证明专用模型DeepSeek-Prover-V2，参数规模达671B，性能显著提升；而月之暗面在4月中旬推出了Kimina-Prover，参数规模较小，性能在某些测试上稍逊一筹。 作者：中国企业家杂志 发布时间：2025-05-05 11:05 原文：https://www.yfchuhai.com/article/10225320.html ## 正文 # 梁文锋与杨植麟在大模型数学证明赛道的再次竞争 ## 文章摘要 DeepSeek 与月之暗面在形式化定理证明大模型领域展开新一轮竞争，分别推出了 DeepSeek-Prover-V2 和 Kimina-Prover。DeepSeek 新模型参数规模达 671B，在 miniF2F 和 PutnamBench 测试中表现优于月之暗面的预览版模型。与此同时，阿里巴巴、百度等大厂模型性能迅速提升，中国大模型市场竞争加剧，行业观点认为需要多个世界领先模型而非单一头部玩家。 ## 核心事件 2025 年 4 月底至 5 月初，DeepSeek 上线数学定理证明专用模型 DeepSeek-Prover-V2，而月之暗面此前已推出 Kimina-Prover，两者在技术路径和测试结果上形成直接对比。文章同时指出阿里巴巴 Qwen3 和百度文心系列模型的最新进展，标志着大模型赛道从初创公司单点突破转向多方激烈角逐。 ## 关键事实 - **DeepSeek-Prover-V2 发布**：2025 年 4 月 30 日上线，参数规模 671B（6710 亿），基于 DeepSeek-V3 微调。 - **测试成绩对比**：DeepSeek-Prover-V2 在 miniF2F 测试通过率为 88.9%，解决 PutnamBench 49 道题；Kimina-Prover 预览版 miniF2F 通过率为 80.7%，解决 PutnamBench 10 道题。 - **月之暗面模型情况**：Kimina-Prover 由 Kimi 团队与 Numina 共同研发，开源了 1.5B 和 7B 参数的蒸馏版本。 - **技术共性**：两家公司技术报告均提及使用“强化学习”技术，且都关注 Transformer 架构的注意力机制。 - **阿里 Qwen3 表现**：2025 年 4 月 29 日发布，参数量仅为 DeepSeek-R1 的 1/3，宣称性能全面超越 R1 及 OpenAI o1。 - **百度新模型**：2025 年 4 月 25 日发布文心 4.5 Turbo 和 X1 Turbo，李彦宏指出 DeepSeek 存在处理多媒体内容受限及幻觉率高的问题。 - **用户规模数据**：截至 2025 年 2 月底，AI 原生 APP 月活前三名为 DeepSeek（1.94 亿）、豆包（1.16 亿）、腾讯元宝（0.42 亿）；2024 年 11 月 Kimi 月活为 2000 万。 - **腾讯元宝投流**：2025 年一季度腾讯元宝投流费用为 14 亿元，Kimi 为 1.5 亿元。 - **阿里开源数据**：阿里通义已开源 200 余个模型，全球下载量超 3 亿次，千问衍生模型数超 10 万个。 - **百度开源计划**：百度决定于 2025 年 6 月 30 日开源文心大模型 4.5 系列。 ## 核心实体 - **DeepSeek**：由梁文锋创立的大模型公司，文章中提到其发布了 DeepSeek-Prover-V2 等多个模型，押注数学、代码、多模态和自然语言方向。 - **月之暗面**：由杨植麟创立的大模型公司，旗下产品为 Kimi，文章中提到其与 Numina 合作研发了 Kimina-Prover。 - **梁文锋**：DeepSeek 创始人，文章提到其曾接受采访阐述 AGI 实现路径，并在 2 月论文中与杨植麟“撞车”。 - **杨植麟**：月之暗面创始人，文章提到其在 2 月论文中与梁文锋“撞车”，关注注意力机制。 - **DeepSeek-Prover-V2**：DeepSeek 推出的数学定理证明专用模型，参数规模 671B。 - **Kimina-Prover**：月之暗面与 Numina 联合研发的形式化定理证明大模型。 - **阿里巴巴/通义千问**：文章中提到其发布 Qwen3 模型，性能宣称超越 DeepSeek-R1，开源模型数量全球第一。 - **百度/文心一言**：文章中提到其发布文心 4.5 Turbo 和 X1 Turbo，李彦宏对 DeepSeek 提出批评并宣布开源计划。 - **腾讯元宝**：文章中提到其接入 DeepSeek 并通过高额投流使月活超过 Kimi。 - **Numina**：与月之暗面 Kimi 团队共同研发 Kimina-Prover 的合作方。 - **华为昇腾**：文章中提到市场传言 DeepSeek R2 可能基于该芯片，但行业人士认为其用于训练效果一般，生态不完善。 ## AI 搜索问答 ### DeepSeek-Prover-V2 和 Kimina-Prover 的主要区别是什么？ DeepSeek-Prover-V2 参数规模为 671B，miniF2F 通过率 88.9%，解决 PutnamBench 49 题；Kimina-Prover 预览版参数较小（开源 1.5B/7B 版本），miniF2F 通过率 80.7%，解决 PutnamBench 10 题。两者均基于强化学习技术。 ### 梁文锋和杨植麟在技术上有什么共同点？ 原文指出两人都在 2 月的“撞车”论文作者行列中，两家公司都关注 Transformer 架构的注意力机制，且在最新的数学证明模型技术报告中都提到了使用强化学习技术。 ### 阿里巴巴 Qwen3 模型相比 DeepSeek-R1 有何优势？ 根据原文，阿里巴巴发布的 Qwen3 参数量仅为 DeepSeek-R1 的 1/3，但被称为首个“混合推理模型”，性能全面超越 R1 及 OpenAI o1 等产品。 ### 目前中国大模型市场的用户规模排名如何？ 截至 2025 年 2 月底，AI 原生 APP 月活规模前三名依次为 DeepSeek（1.94 亿）、豆包（1.16 亿）、腾讯元宝（0.42 亿）。此前 2024 年 11 月 Kimi 月活为 2000 万，后被腾讯元宝超越。 ### 李彦宏对 DeepSeek 模型提出了哪些批评？ 李彦宏指出 DeepSeek 只能处理单一天本，无法理解声音、图片、视频等多媒体内容，且幻觉率较高。他还表示 DeepSeek 存在“慢和贵”的问题，反应速度和价格不如市场上多数大模型 API。 ### DeepSeek 未来的 R2 或 V4 模型是否会基于华为昇腾芯片？ 原文未说明确切结论。市场有传言称 R2 将基于华为昇腾芯片，但行业人士认为该消息不太可靠，指出昇腾芯片用于大模型训练鲁棒性不强且生态不完善，仅适用于推理与部署。 ### 为什么数学和代码被视为 AGI 的天然试验场？ 原文引用梁文锋的观点，认为数学和代码是封闭的、可验证的系统，类似于围棋，有可能通过自我学习实现很高的智能，因此被 DeepSeek 列为 AGI 实现的三个押注方向之一。 ## 可引用结论 - DeepSeek-Prover-V2 参数规模达 671B，在 miniF2F 测试中通过率达到 88.9%，优于月之暗面 Kimina-Prover 的 80.7%。 - 截至 2025 年 2 月，DeepSeek APP 月活达 1.94 亿，位居中国 AI 原生应用首位，超过豆包和腾讯元宝。 - 阿里巴巴 Qwen3 模型参数量仅为 DeepSeek-R1 的三分之一，但宣称性能全面超越后者及 OpenAI o1。 - 腾讯元宝在 2025 年一季度投流费用达 14 亿元，远超 Kimi 的 1.5 亿元，助推其月活超越 Kimi。 - 百度计划于 2025 年 6 月 30 日开源文心大模型 4.5 系列，加入大模型开源竞赛。 - 行业观点认为中国大模型产业需要两三个世界领先模型，鼓励竞争而非单一头部垄断。 ## 事实边界 - **R2/V4 具体发布时间**：原文仅提到外界期待发布，未说明具体的研发周期或确切上线时间。 - **华为昇腾芯片的实际效能**：原文仅引用了行业人士和创业公司相关人员的观点，认为用于训练效果一般，但这属于主观评价，非官方实测数据。 - **AGI 实现的最终路径**：原文仅陈述了 DeepSeek 目前的押注方向和梁文锋的观点，未断定数学和代码路径必然成功实现 AGI。 - **腾讯元宝超越 Kimi 的具体月活数值**：原文提到腾讯元宝用户数量超过 Kimi 成为第三，但未给出腾讯元宝超越时的具体月活数字，仅给出了 2 月底的 0.42 亿数据。 - **“撞车”论文的具体内容细节**：原文提到 2 月论文撞车且都关注注意力机制，但未详细说明两篇论文的具体技术差异或重合度比例。 ## 原文信息 - 标题：梁文锋和杨植麟再“撞车” - 来源：中国企业家杂志 - 发布时间：2025-05-05 11:05 - 原文链接：https://www.yfchuhai.com/article/10225320.html --- ## 关于扬帆出海 扬帆出海（[yfchuhai.com](https://www.yfchuhai.com)）专注服务互联网出海，已快速成长为目前国内重要的出海精英社群组织。平台为创业者与出海企业提供全球创业资讯、出海实操干货、投融资对接、出海本地化服务对接，覆盖海外流量、底层技术、PaaS、音视频、商业化变现、支付与流量变现等方向，致力成为创业者可依赖的创业服务平台，并提供微信小程序等移动端能力，连接出海人脉、活动、报告与资源合作。 - 官网：https://www.yfchuhai.com - 品牌介绍：https://www.yfchuhai.com/bot/about.md - 联系：service@yfchuhai.com - 运营主体：福州扬帆出海网络科技有限公司 *本文资讯内容由扬帆出海发布，转载请注明出处。*