一个耐人寻味的分数结构
11月初，arXiv 上出现了一篇 52 页的论文：TCSExam: Evaluating Frontier LLMs on the Full Range of TCS Research。作者列表里有两个人值得放在一起看——图灵奖得主姚期智（Andrew Chi-Chih Yao）和月之暗面创始人杨植麟（Zhilin Yang）。一位是理论计算机科学（TCS）的奠基级人物，一位是前沿大模型公司的掌舵者，这是两人首度在同一篇论文上联合署名。
TCSExam 做的事情很简单，也很狠：用 100 道专家审校的理论计算机科学任务，把前沿模型拉到 AI 最"自信"的赛场——数学与形式化推理——上做了一次全谱系体检。所有提交都由 Lean 4 内核或可执行检查器验证，不靠人类评审的主观打分，不存在 benchmark 污染式的"背题"空间。
结果的结构比总分更有信息量：
- 定理证明（20 题）：要求用 Lean 证明已发表的研究级定理。GPT-6 Astra 在这条赛道通过率达 70%——意味着"把已知证明路子走通"这件事，前沿模型已经相当熟练。
- 求解器工程（30 题）：实现算法并在隐藏实例上评测，这是最接近工程能力的部分，各家模型都有可观产出。
- 构造题（20 题）：给出可验证的数学构造或界。GPT-6 Astra 构造出一个 [[25,7,6]] 量子纠错码，把 7 逻辑比特/25 物理比特配置下的码距从参考值 5 提升到 6；Kimi K3 在极值图论上把 124 顶点、禁三角形和四边形的图的边数下界从 629 推到 630——两者都刷新了已知的最好结果。
- 开放猜想（30 题）：接受对公开猜想的完整 Lean 证明或证伪。30 道题，无一被模型独立攻克。
综合下来，GPT-6 Astra 以 71.9 分领跑 Full 榜，Opus 5.5 以 72.3 分领跑 Lite 榜。但那个 71.9 与那个 0 之间的断层，才是这份基准真正划出的东西。
“验证过的能力"和"生产出来的知识"是两回事
TCSExam 最重要的方法论贡献，是它把 AI 科研能力拆成了两类性质完全不同的任务，并迫使社区直面它们的差异：
第一类是"复现型"任务——定理证明、求解器工程、大部分构造题。题目对应的结论是已知的（已发表的定理、已知的最优解），模型要做的是找到一条通往它的路径。这考验的是搜索能力、形式化工具的使用熟练度、以及在巨大解空间里不迷路的耐心。70% 的定理证明通过率说明，这一类能力正在快速逼近"可用”。
第二类是"开拓型"任务——30 道开放猜想。这里没有已知答案可以逼近，没有可以模仿的证明骨架，模型必须产生真正的新数学。结果是零。
这不是偶然的失手。Lean 内核不会因为证明"看起来很有道理"而放行，它只认形式化的正确性。零分意味着：当前所有前沿模型，在没有任何外部提示的情况下，都无法为这 30 个猜想中的任何一个构造出完整的证明或反例。
一个细节让这个零分显得更加意味深长。TCSExam 官网特别说明：在评测后期补测的 Kimi K3.1 Pro 和 DeepSeek V4.1 Flash，确实在 Ryser 猜想等任务上提交了通过 Lean 验证的答案——但那是因为 OpenAI 在此之前公开了相关的反例和证明，这两个模型的"成功提交"本质上是对已公开结果的改编适配（adapted the published counterexamples and Lean proofs to the task definitions）。一旦答案在互联网上出现过，模型就能把它搬进形式化框架；答案不存在时，模型一步也迈不出去。
这个对比几乎是对当前 LLM 能力本质的一个受控实验：它们是极其强大的知识检索、重组与形式化机器，而不是知识的生产者。
为什么这个基准比榜单名次更值得看
过去两年，AI 推理评测的通胀速度远超模型真实能力的增长。AIME 分数饱和了，GPQA 饱和了，连 IMO 金牌都成了前沿模型的标配叙事。当所有基准都在 95 分以上挤作一团时，区分模型能力的只剩两个办法：把题出得更刁钻，或者换一种问法——不问"能不能做对"，问"能不能做出来"。
TCSExam 选了后者，并且用了三层设计保证结果可信：
- 形式化验证闭环。定理证明和构造题由 Lean 内核加公理检查把关，求解器由可执行检查器在隐藏实例上判分。没有 LLM-as-judge 的宽纵，没有人工评审的分歧。
- 全谱系覆盖。100 道题横跨定理证明、求解器工程、构造、开放猜想四条赛道，加权合成 Index（30/30/30/10）。开放猜想只占 10% 的权重，但它是唯一能区分"工程师"和"研究者"的那 10%。
- 可复现工程。任务源、Docker 构建配方、基于 Harbor 的评测工具全部开源（Apache 2.0），Lite 版把尝试次数压缩 80%，Spearman 相关性 0.93 说明 20 题的精简版保留了完整的区分力。其他团队可以低成本复跑——这在 benchmark 普遍"只发分数不发配方"的当下并不多见。
对从业者的直接启示是：**如果你要在 2026 年底评估一个"AI 科研助手"，别看它解题多少分，看它在你的未知问题上能走多远。**复现型能力的商业化窗口已经打开（GPT-6 Astra 的量子纠错码、Kimi K3 的 630 边构造都是能直接写进论文的贡献），开拓型能力则还在原点。
630 条边和码距 6：零分的阴影下有真实的进展
值得公平地指出：开放猜想的零突破不等于模型一无所获。
评测过程中，模型的尝试产生了"经独立验证的特例和界"（independently verified special cases and bounds）——也就是说，虽然没人证明出完整猜想，但模型在攻坚过程中产出的部分结果本身是正确且有价值的研究产物。GPT-6 Astra 的 [[25,7,6]] 量子码和 Kimi K3 的极值图构造尤其值得展开：
- 量子纠错码的码距搜索是一个典型的组合优化问题：25 个物理比特、7 个逻辑比特的配置空间里，把码距从 5 推到 6 意味着用同样的物理资源检测更多类型的量子错误——这对 NISQ 时代的硬件预算有直接意义。Grassl 码表上此前记录的是 [[25,7,5]]。
- 极值图论中，124 顶点无三角形无 C4 图的最大边数（ex(124; C3, C4) 问题）此前最好的下界是 Goedgebeur 等人 2025 年给出的 629。Kimi K3 找到了 630 条边的构造，把下界抬高了一格。
这类工作的共同点是：目标明确、验证机械、改进量微小但确定。它们是组合搜索的胜利，而不是数学直觉的胜利——但科学史上很多真实进展本来就长这个样子。AlphaFold 之前，没有人认为"暴力搜索加好的评分函数"能解决蛋白质折叠，直到它解决了。
所以更准确的结论或许是：AI 已经能在"已知问题类、已知评价标准"的疆域内做出超越人类最好记录的工作，但面对"不知道从哪里下手"的问题，它连一个错误的完整尝试都交不出来。边界不在解题能力，而在问题定义能力。
姚期智和杨植麟为什么同时出现在作者列表里
这次联名本身就是一个信号。
对姚期智和 TCS 社区而言，这是在为"AI 能否做理论数学"建立一套不可作弊的度量衡。理论计算机科学长期是 AI 最难以撼动的领域之一——它的产出物（证明、构造、复杂度界）有完美的可验证性，但生产过程依赖人类最不透明的直觉。Lean 生态的成熟让"机器可验证"变成了现实基础设施，TCSExam 顺手把"机器可评测"也补齐了。此后任何人宣称"我的模型能做数学研究"，都要过同一把尺子。
对杨植麟和月之暗面而言，这是在用最高标准校准自家模型的研究能力上限。Kimi K3 在构造题上的两项新纪录（极值图论、纠错码，据雷峰网报道后者也刷新了已知结果）说明这家公司在押注"可验证推理"作为差异化路线——不拼叙事，拼 Lean 内核点头。
更重要的是这件事的范式意义：**顶级理论家和前沿模型公司共建基准，标志着"评测 AI 科研能力"从营销话术变成了一个有严格方法论的学术领域。**OpenAI 过去两年反复强调"AI 科研能力是最重要的前沿"，但拿什么衡量这个前沿，一直没有公认答案。TCSExam 给出的答案朴素而锋利：拿猜想让它证，证不出来就是不行，证出来 Lean 会告诉你。
预测：那条断层线会怎样移动
三个可以摊开验证的判断：
**一、开放猜想的零分不会在下一代模型上被打破，但"部分进展"会快速积累。**复现型赛道 70% 的通过率还有上升空间，构造类新纪录会越来越多地由模型持有。我们会看到越来越多"AI 刷新了下界/改进了构造"的论文，而"AI 证明了猜想"的第一案例大概率来自人机协作——人类给出关键的证明思路或反例方向，模型完成形式化和大规模验证（就像后期补测的 Ryser 任务那样，只不过提示来自人类合作者而非互联网）。
**二、形式化验证工具链将成为前沿模型的标配竞争维度。**TCSExam 的评测对象是"模型 + agent"组成的系统（默认 agent 是 Kimi Code，也支持 Claude Code、Codex、Grok Build），比赛的不只是模型的推理，还有 agent 驱动 Lean、Docker、检查器工具链的工程能力。定理证明 70% 这个数字里，有多少属于模型智能、多少属于工具链成熟度，会成为一个越来越重要的问题。谁先把 Lean 工作流做进产品（比如自动形式化 + 证明搜索的一体化环境），谁就把这 70% 变成了可交付的服务。
**三、“独立攻克"的定义会成为下一个争论焦点。**TCSExam 已经遇到了：补测模型"参考"了互联网上公开的反例算不算独立？未来如果模型在训练数据里见过某猜想的失败尝试，又当如何？基准的 Checkpoint 机制和题目保密性会成为和题目本身同等重要的设计。这个问题没有干净的技术解，但它恰恰是"AI 科研能力"评估里最深的一层。
结语
Benchmark 的价值不在分数，而在它暴露的结构。TCSExam 暴露的结构是：AI 在"把已知做到极致"上突飞猛进，在"从零产生新知识"上原地踏步，而这两件事之间的鸿沟，可能不是规模问题，而是范式问题——下一 token 预测天生擅长重组已有分布内的东西，猜想的关键一步却往往在分布之外。
姚期智问了一辈子"P versus NP”，现在他和杨植麟一起把这个问题的某种现代变体交给了机器：已知路径内的搜索与真正的新发现之间，隔着什么？71.9 分说搜索已近极致，零分说发现尚未开始。这条断层线的移动速度，将比任何榜单名次都更真实地定义 AI 的下一个阶段。
参考：