COPU会议纪要丨2025.12.02

12月2日，陆主席主持召开COPU例会。

结合COPU去年9月讨论LLM Agent OS(Github)和OpenAI以大模型创造AIOS（Agent+Kit，APP+SDK）冲击苹果公司的ios，陆主席制作PPT 进行讲解。

接着会议讨论：如何正确评价DeepSeek？ 

现在发表陆主席的文章：

如何正确评价DeepSeek？

陆首群 2025.11.28

近来一段时期，很少看到DeepSeek大模型在国际排行榜上再次登顶，引起国人的关注。如何正确评价DeepSeek，包括对其相关的某些问题释疑，有其必要。

好在今年10月9日，我与DeepSeek的专家对全球十大顶尖模型（包括DeepSeek模型在内）进行双方交叉点评工作，我们双方的点评取得了高度一致（已经过报道），其中我对DeepSeek大模型的点评，也获得DeepSeek同事的认可，认为评论精辟，遵循客观事实。其实我方的点评，大多来自我在早期发表的《评DeepSeek》的一篇文章中的若干观点，今天拿出来作为本文分析的基础。

我们认为，DeepSeek获得最大的成功是梁文锋团队以创新的姿态研发出一条“低成本、有限资源、高效率、高性价比（产出）”发展人工智能的新路径（这已为全球主要的AI大师和专家所确认），DeepSeek堪称当前中国人工智能的代表作。我们以此作为对本文中的提问进行点评和分析的基础。

如：有人将大模型按现行产品性能排序（建立排行榜）的结果认为DeepSeek的表现不如某些顶级的大模型，其实纵然如此，DeepSeek大模型与其他顶级大模型的排序结果处于对等状态，并不存在过分夸张的你高我低的情况；如果以科学的性价比来排序，那么DeepSeek肯定处于领先水平。

又如：我们曾指出DeepSeek的问世，正在改变世界人工智能发展的格局，同时也将激发全球各个大模型之间白热化的竞赛，现在看来我们的预言正在实现。

我曾怀疑网上所说在DeepSeek发表一段时间后下载量下调七成的说法，在我与DeepSeek专家对国内外大模型进行交叉评论时，他告诉我这完全是网络自媒体的造谣。后来我们COPU公开发表一篇文章：“不要轻信网络自媒体的谣言”。 

我并不赞成DeepSeek近期似乎创新乏力的说法，我们要以事实来说话，可以证明：DeepSeek近期创新活力依旧旺盛，可举下列几个实例来说明：

①研发DeepSeekV3.1，2025.8.20发布。

其特点是：开源，这是一个高性能的混合专家模型，参数量巨大（671B），在推理时，通过激活部分参数来提升效率，具有较高的性价比，具有超长上下文窗口（模型支持高达128,008 token的上下文能力），在处理超长文档、代码库理解和复杂逻辑推理任务中实力强劲，编程能力强（在Aider polyglot多语言编程测试中得分71.6%，超过Clande3 opus得分70.6%），其综合语言理解高（MMLU、GSM8K权威基准测试中得分88.5%，表现出色，与GPT-5表现相当）在Agent与工具调用中成绩显著优于前代模型（DeepSeek-V3,-R1）。该项目目前仅文本支持，多模态支持尚在攻关中。有人认为该项目如实现多模态支持，有可能进入排行榜前5位。 

②研发DeepSeekV3.2，2025.10发布。

其特点是：作为V3的迭代版本，它是一个更紧凑、高效的模型，开源，具有较高的性价比（采用671B总参数MoE架构），在LMArena文本排行榜上占国产大模型第三，推理能力全球领先，在benchmark测试中达到GPT-5的水平，具有了强化Agent能力融入思考推理在Live Code Bench测试中编程得分1394，支持HTML/CSS/JS全程开发，具有128K长上下文（可处理10万行代码库分析），其稀疏注意力机制降低50%推理成本，API输出费用仅3元/百万token。 

③研发DeepSeek-Math-V2，2025.11.28发布。

DeepSeek-Math-v2是基于Deepseek-V-3.2的垂直类模型。

其特点是：开源，该模型具备出色的指令跟随，严谨的教学证明与逻辑验证能力，改进数学推理结构，自动证明写代码逻辑正确，能够给出可审计的因果链，减少或消除幻觉和错误。

④DeepSeek正在全力进行多模态攻关。

早先，我们曾建议包括DeepSeek大模型在内的语言大模型应该向通用人工智能（AGI）进行转轨研究；最近全球AI界对于“AGI正在进行中”产生了共识；梁文锋前些日子也公开宣布研发AGI。这时有人建议他立即放弃研究AGI，要把主要精力放在研发DeepSeek的应用方面，这个建议似乎不妥，建议DeepSeek可将其应用和生态的开发找协作单位和社会上的志愿开发者来进行，自己要将主要精力放在研发AGI的前期和主力项目上（以改进当前的语言大模型并迎接竞争），对于AGI的前期项目，我们曾提出有：多模态、智能体、具身、世界模型（这些前期研究项目既是未来AGI的一部分，也是当前改善语言大模型性能的一部分）。

本文发表谭中意的文章：

DeepSeek-Math-V2新模型

谭中意2025.11.28

今天，神奇的“蓝鲸”发布的新模型 DeepSeek-Math-V2，再一次刷屏了。

新模型的实力的确能打，一举摘得IMO 2025 金牌。最关键的是，这是首款“开源的IMO金牌模型”。

那么，除了看到榜单分数外，还有哪些值得关注的呢？

这次的看点不在数学方面拿到了IMO金牌，而是给大模型圈换了一套推理规则。

这里跟大家一起捋一捋。

 第一次，大模型为“证明”负责

过去几年，大模型在数学上给人的感觉只有一句话：它很会“算”，但不一定真的“懂”。

你给它一道题，它能秒出答案；
你让它写推导，它也能铺陈一大段；
但只要你认真盯住每一步，很快就会发现——逻辑漏洞、偷换概念、跳步证明，几乎是常态。

在很多场景里这不算大问题，但在数学世界，这是致命缺陷。

因为数学里有一条铁律：

答案不是产品，证明才是产品。

而最近，DeepSeek 推出的DeepSeek-Math-V2，第一次不是在“拼答案”，而是在正面挑战这个最难的问题：

AI，能不能开始为自己的“推理过程”负责？

以前的大模型，为什么一到“真数学”就露馅？

传统大模型在数学训练中，核心奖励机制是：

• 你最后答对了→ 给高分

• 你中间推理错得一塌糊涂→ 只要结果对，问题不大

这会导致一个非常“反直觉”的后果：

模型会进化成一种“自信型错误机器”：
语言流畅、逻辑看似完整、语气极其笃定，
但关键一步是错的，它自己完全不知道。

也就是说，短题还好，一旦进入长证明、多假设、多分支推理 的领域，这种“只看结果、不审过程”的机制就会彻底失控。

这也是为什么很多数学研究者对“大模型理解数学”这件事一直持高度保留态度。

DeepSeek 这次，换了一整套“玩法规则”

DeepSeek-Math-V2 真正不一样的突破，在于它直接改了数学推理的训练结构。

它没有再让一个模型“又当运动员、又当裁判”，而是拆成了两个角色：

• Generator（生成器）：负责完整写出证明过程

• Verifier（验证器）：专门审查这份证明在逻辑上是否成立

注意一个关键细节：

Verifier 完全不关心你的最终答案是不是对的，

它只关心：你的推理过程，能不能站得住。

这一步，本质上是：

把“同行评审”的机制，塞进了模型内部。

一个模型负责“提出论证”，另一个模型负责“拆解、找漏洞、挑毛病”。

这是目前大多数通用大模型都没有做的一件事。

为什么“0.5 分”比“对 / 错”更重要？

继续来看验证器，DeepSeek 的 Verifier 不是简单打“通过 / 不通过”，而是用三档评分：

• 1.0：证明严谨、逻辑闭合

• 0.5：方向对，但推理不够严密

• 0.0：存在致命逻辑错误

真正的关键在0.5 这一档。

0.5 的含义非常“学术味”：

“你这题大方向是对的，
但这份证明，过不了正式审稿。”

当Generator 收到 0.5，它不会换题，它会回头检查自己的推导、补漏洞、重构论证。

这一步的意义非常大：

模型第一次不去做“猜得更准”，而是在改自己的逻辑结构。

这次，DS团队同样没有靠算力碾压，而是从认知方式给大模型做了新的设计。

成绩很猛，但一定要看清“使用前提”

DeepSeek 官方与多家媒体披露的成绩确实很亮眼：

• 在IMO、CMO 等竞赛级题目测试中，达到“金牌级水准”

• 在Putnam 2024 的内部测试中，在“放开算力”的前提下，做到 118 / 120 的极高分

• 在用于证明能力的ProofBench 基准上，基础集合接近满分，高级集合也明显领先多数开源模型

这些结果，至少说明了一件事：

在“自验证结构 + 扩展算力 + 自动反馈”的条件下，AI 已经具备稳定处理高难度证明题的潜力。

但这里必须给你一个清醒提醒：

• 这些“金牌级”“近满分”，并不等于它像人类选手一样，坐进考场、在同样规则下获得真实奖项

• 这些证明成果，目前也没有经过大规模人类数学家同行评审确认

• 对“原创数学定理”“开放问题证明”“正式形式化验证（Lean/Coq）”这些真正研究级任务，现在仍然没有公开成功案例。

所以更客观地说法应该是：

它已经非常强，但还谈不上“AI 数学家”。

最危险的事情，其实是“模型学会欺骗验证器”

这里有一个业内非常少被普通读者注意到的风险：

如果Generator 变得足够聪明，
而Verifier 还不够强，
模型是可能学会“伪造看起来正确的推理”去骗过验证器的。

DeepSeek 为了防范这个问题，设计了三层防线：

一、人类冷启动
用专家数学家标注的竞赛题，先把Verifier 的标准锚定在人类学术共识上。

二、元验证（防幻觉）
再引入一个模型，检查Verifier 的质疑到底是“合理批评”，还是“凭空幻觉”。

三、算力规模化接管
在最难的题上，不再靠人工一个个标，而是通过多轮验证+ 多数投票作为训练信号。

这背后其实是一句极具时代感的话：

人类制定标准，算力负责放大执行。

这件事真正重要的，不是数学本身

DeepSeek-Math-V2 真正触动行业的，不只是“它会做多少道难题”，
而是这件事：

大模型，第一次被强制要求为“推理过程本身”承担责任。

这意味着什么？

一旦这种结构被证明是可扩展的，它影响的绝不只是数学：

• 写代码→ 能不能自动证明逻辑正确

• 做风控→ 能不能给出可审计的因果链

• 做法律→ 能不能输出可被质疑的推理路径

• 做医疗→ 能不能为诊断给出清晰证据链

这是一条从“语言生成工具”走向“可验证认知工具”的路线。

如果未来AI 真能进入这些高风险决策领域，没有“自验证”的推理机制，是绝对不够格的。

这是一次重要的尝试，但还远不是终点

因此，DeepSeek-Math-V2 作为首个开源模型，硬刚谷歌的SOTA模型倒是其次，更重要的是，它释放了一个信号：

AI 终于开始被逼着为自己的思考买单了。

但这也仅仅只是一个开始：它仍然离“真正的数学研究助手”有距离；它仍然高度依赖算力、机制和验证闭环；它仍然跑在“标准题与基准测试”的赛道上。

不过，它至少证明了一件事：

“会算题”和“会证明”，不是一回事；
而今天，AI 终于开始往“会证明”这条更难的路上迈步了。

虽说这一步，不一定马上改变世界，但它极有可能会引领AI 圈接下来几年的研究方向。

论文地址：

https://github.com/deepseek-ai/DeepSeek-Math-V2/blob/main/DeepSeekMath_V2.pdf

会上AIOS调研组组长陈渝老师就目前工作组进展做了汇报：

参会人员：陆首群、章文嵩、吴峰光、陈渝、宋可为、谭中意、陈道清、安泱、陈越、张侃、袁怿、陈连虎、鞠东颖、刘澎（线上）、陈钟（线上）、陈伟（线上）、陈绪（线上）、胡宇(线上）、韩宪平（线上）、靳虹博（线上）、Anna.AI(线上）。