梁文锋和杨植麟再“撞车”
摘要：
继 2 月论文 " 撞车 " 之后，梁文锋和杨植麟又在另一个大模型赛道上相遇了。4 月 30 日，DeepSeek 上线新模型 DeepSeek-Prover-V2，这是一个数学定... 继 2 月论文 " 撞车 " 之后，梁文锋和杨植麟又在另一个大模型赛道上相遇了。
4 月 30 日，DeepSeek 上线新模型 DeepSeek-Prover-V2，这是一个数学定理证明专用模型。
Prover-V2 的参数规模进一步扩展到 671B（6710 亿规模参数），相较于前一代 V1.5 版本的 7B 规模增加了近百倍，这让其在数学测试集上的效率和正确率更高，比如，该模型的 miniF2F 测试通过率达到 88.9%，它还解决了 PutnamBench（普特南测试）的 49 道题。
巧合的是，4 月中旬，月之暗面也曾推出一款用于形式化定理证明的大模型 Kimina-Prover，这是 Kimi 团队和 Numina 共同研发的大模型，该产品也开源了 1.5B 和 7B 参数的模型蒸馏版本。该模型的 miniF2F 测试通过率为 80.7%，PutnamBench 测试成绩为 10 道题。
两者相比较，在 miniF2F 测试通过率以及普特南测试上，DeepSeek-Prover-V2 的表现超过了 Kimina-Prover 预览版。
值得注意的是，两家公司在技术报告中都提到了强化学习。比如 DeepSeek 的题目为《DeepSeek-Prover-V2：通过子目标分解的强化学习推进形式数学推理》，而月之暗面的题目为《Kimina-Prover Preview：基于强化学习技术的大型形式推理模型》。
在 2 月的两篇 " 撞车 " 论文中，梁文锋和杨植麟都在作者行列，两家公司都关注 Transformer 架构最核心的注意力机制，即如何让模型更好地处理长上下文。
作为中国大模型领域最受瞩目的创业者，两人也正在面临不同的挑战。
对于梁文锋而言，在 R1 模型推出三个多月后，外界对 DeepSeek" 魔法 " 的痴迷程度正在下降，阿里巴巴的开源模型正在迅速赶上以及超过 DeepSeek，外界热切期待其发布 R2 或 V4 模型，以加强领先优势。
对于杨植麟和月之暗面，Kimi 正在遭受来自字节跳动的豆包和腾讯元宝的挑战，它也需要保持持续创新。
编程与数学，实现 AGI 的两条路径
对于 AGI 的实现路径，2024 年，DeepSeek 创始人梁文锋在接受《暗涌》采访时曾说，他们确实押注了三个方向：一是数学和代码、二是多模态、三是自然语言本身。数学和代码是 AGI 天然的试验场，有点像围棋，是一个封闭的、可验证的系统，有可能通过自我学习就能实现很高的智能。另一方面，多模态需要参与到人类真实世界里学习。他们对一切可能性都保持开放。
此次 Prover-V2 模型的推出，让 DeepSeek 的各个模型矩阵保持了同步进化。
Prover 系列模型于 2024 年 3 月开始被发布，2024 年 8 月被更新为 DeepSeek-Prover-V1.5（后简称为 Prover-V1.5），2025 年 4 月再被更新至 DeepSeek-Prover-V2。
DeepSeek 代码系列模型 Coder 从 2024 年 4 月开始更新，6 月升级为 Coder-V2-0614，7 月再次升级，9 月，DeepSeek-V2-Chat 和 DeepSeek-Coder-V2 合并，升级后的新模型为 DeepSeek-V2.5，2024 年 12 月，该模型更新至 V3，今年 3 月，升级至 V3-0324。
通用推理大模型，以 1 月 20 日发布的 R1 模型为代表，价格低廉，自然语言推理性能强劲，在数学、代码、自然语言推理等任务上，性能比肩 OpenAI o1 正式版。
从 Prover-V2 的技术报告上看，其与 DeepSeek 的其他模型进化有关联，其中，DeepSeek-Prover-V2-671B 是以 DeepSeek-V3 作为基础模型来做微调，如在冷启动阶段，DeepSeek-V3 将复杂问题分解为一系列子目标，而后，已解决子目标的证明被合成到一个思维过程链中，结合 DeepSeek-V3 的逐步推理，为强化学习创建一个初始冷启动。
算法工程师、知乎用户 " 小小将 " 告诉《中国企业家》，推理模型在进行推理时，要进行复杂的思考，代码与数学模型可以检验推理大模型能力进展，因为数学与代码的结果是可验证的。
他认为，Prover-V2 的推出与新模型 R2 或 V4 的上线没有必然联系，它更像是一个独立模型的更新。
他预测，R2 模型更像是 GPT-o1 到 o3 的过程，比如在提高强化学习的能力方面，DeepSeek 可以基于 V3，提升后训练效果，因此 R2 的研发周期可能会比较短。但 V4 就是一个大版本的更新，其研发周期有可能更长，因为预训练的工程量以及训练方法可能都会发生变化。
目前市场已经对 DeepSeek 的新模型充满了想象和期待。
市场上传言，R2 模型将基于华为昇腾系列 GPU 芯片而推出，但一位行业人士说，这个消息不太可靠，在英伟达 H20 芯片被限之后，昇腾系列芯片在市场上也是一卡难求，" 对于昇腾来说，如果用于大模型研发，可能鲁棒性没那么强 "。
另有创业公司相关人士告诉《中国企业家》，华为昇腾芯片用于大模型的训练，效果一般，原因在于生态系统没那么完善，但用于大模型的推理与部署，是没有问题的。
DeepSeek 与 Kimi 还能保持领先吗？
DeepSeek 与月之暗面作为明星初创公司，正在遭受大公司的追赶和超越。
以月之暗面旗下的 Kimi 为例，据 QuestMobile 数据，Kimi 上线不足 1 年，在 2024 年 11 月，月活突破 2000 万，仅次于豆包的 5600 万。
QuestMobile 数据显示，截至 2025 年 2 月底，AI 原生 APP 月活规模前三名从豆包、Kimi、文小言更迭为 DeepSeek、豆包、腾讯元宝，规模分别是 1.94 亿、1.16 亿、0.42 亿。
2 月中旬，腾讯元宝宣布接入 DeepSeek，随后，在一个多月时间内，腾讯元宝利用超级产品微信引流加上疯狂买量投流，在用户数量上已经超过了 Kimi，成为排名第三的 AI 产品。据 AppGrowing 数据，在今年一季度，腾讯元宝的投流费用为 14 亿元，远远超过 Kimi 的 1.5 亿元规模。
目前，Kimi 最新的举动是内测社区功能，增加用户粘性。
DeepSeek 同样也避免不了被大公司追赶甚至超越的挑战。近期，阿里巴巴在大模型方面展现出了强劲的竞争力。
4 月 29 日，阿里巴巴发布新一代通义千问模型 Qwen3，该模型被称作首个 " 混合推理模型 "，是 " 快思考 " 和 " 慢思考 " 集成的一个模型，参数量仅为 DeepSeek-R1 的 1/3，性能全面超越 R1、OpenAI o1 等同行产品。
此前，蔡崇信评价 DeepSeek，它告诉了我们开源的价值。根据公开数据，阿里通义已开源 200 余个模型，全球下载量超 3 亿次，千问衍生模型数超 10 万个，已超越美国 Llama，成为全球第一开源模型。
一位 AI 创业者告诉《中国企业家》，DeepSeek 受到了过多的关注，被赋予过多光环，中国大模型产业需要两三个世界领先的大模型，而不是一个，这时候应鼓励这个领域的竞争和创业。
另一个重要玩家是百度。4 月 25 日，百度发布文心 4.5 Turbo 和深度思考模型 X1 Turbo，这两款模型性能更强大，成本更低，李彦宏更是数次提到 DeepSeek，他说，DeepSeek 也不是万能的，它只能处理单一的文本，还不能理解声音、图片、视频等多媒体内容，同时幻觉率比较高，很多场合不能放心使用。
"DeepSeek 最大的问题是慢和贵，中国市场上绝大多数大模型 API 的价格都更低，而且反应速度更快。" 李彦宏在发布会上说。
尽管如此，百度仍决定学习 DeepSeek，今年 2 月，百度决定在 6 月 30 日开源文心大模型 4.5 系列。
越来越多的玩家参与大模型开源竞赛，但只有技术最先进的玩家才能定义标准。
