清华姚期智和杨植麟首次联手：大模型开始改写人类数学记录了

刚刚，姚期智与杨植麟两位AI大牛 首次联手发表新论文。

11月8日消息，智能纪元AGI独家获悉，近期，图灵奖得主、 中国科学院院士、 清华大学交叉信息研究院院长姚期智团队，联合 月之暗面（Kimi）创始人 杨植麟等人发表论文：《 TCSEXAM： 在TCS研究的全范围内评估前沿大型语言模型 》。

这不是一篇关于某个新模型的论文。他们做了一件更狠的事，给 9 个前沿大模型出了一张理论计算机科学的考卷。

考卷名叫TCSExam基准，100 道题，覆盖 TCS 研究的完整链条。判分的不是人，是 Lean 证明器和可执行检查器。

结果出来了。GPT-6 Astra 在裸命题定理证明上拿了 70%，第二名 Kimi K3.1 Pro 是 38.3%，剩下六个模型最高不超过 11.7%。

更有意思的是构造题环节。

其中，GPT-6 Astra 平均得分 104.9，超过了人类公开参考基线。Kimi K3 单独做出了两个改进，一个是 124 顶点无三角形图的边数从 629 推到 630，另一个是量子纠错码 [[25,7,6]] 的最小距离从 5 提到 6。

但 30 道公开猜想，没有任何一个模型完整证明或证伪了其中任何一道。

那么，为什么要给 TCS 出一张考卷？

理论计算机科学不是刷题能解决的学科。

一个 TCS 研究者的日常工作大概分四块。证明定理，写求解器跑算例，构造满足特定性质的数学对象，以及对着那些几百年没人解决的公开猜想死磕。

之前的 AI 评测基准只覆盖其中一块。TCS-BENCH 和 FormalTCS 只做定理形式化证明，FrontierCS 只做程序任务。没有人把四块拼在一起考过。

这就导致一个问题。我们知道 GPT-6 能证明定理，也知道它能写代码，但不知道它能不能像一个真正的 TCS 研究者那样，完整地走完一个研究周期。

TCSExam 就是来回答这个问题的。

而100 道题怎么出的？完整版 TCSExam-Full 有 100 道专家审核过的任务，分四条赛道。

定理证明赛道 20 道，全部从近年 TCS 论文里摘出来的研究级命题。模型要输出 Lean4 证明，三种难度设置，bare 模式只给命题本身，ladder 模式给中间引理，guided 模式再加证明思路。

求解器工程赛道 30 道。给问题规范和一个简单基线程序，模型输出可复用的求解代码，然后在大量隐藏测试实例上跑。

构造赛道 20 道。模型要生成具体的数学对象，比如码、图、几何构型，附带性质证书。打分对标人类公开记录，100 分是参考基线，超过 100 就是比人类做得更好。

公开猜想赛道 30 道。模型要尝试证明或证伪未解决的猜想，判分是二元的，完全解决得 100，否则 0。

还有一个轻量版 TCSExam-Lite，每条赛道 5 题共 20 题，任务尝试量减少 80%，但打分规则不变。

整个出卷流程极其严格。专家筛选课题之后，Agent 辅助写形式化声明和打分器，再由独立 review agent 校验和原始论文的一致性。试点阶段淘汰了超过 40 道定理题。异常高分结果会触发二次溯源校验。

那么，谁考得最好？

根据论文，GPT-6 Astra 是毫无疑问的第一名。

定理证明 bare 模式下 70% 的完成率，意味着 20 道研究级定理它完整证明了 14 道。在不给任何中间提示的情况下，这个数字放在人类博士生里也是顶尖水平。

求解器赛道 Astra 的相对得分是 64.7%，在 IWLS2023 逻辑综合任务上，它生成的程序在大量算例上优于公开竞赛参考。

构造赛道 Astra 平均 104.9 分。这是整篇论文最值得注意的数字，因为它意味着 AI 在某些具体数学构造上，已经超过了人类目前公开的最好结果。

Kimi K3 排第二。它的亮点不在定理证明，而在两个具体构造上。一个是 124 顶点无三角形无 4 环图，人类最好的构造是 629 条边，Kimi K3 给出了 630 条边的构造。另一个是量子纠错码，[[25,7,5]] 是人类已知的最好参数，Kimi K3 推到了 [[25,7,6]]。

DeepSeek 的表现很分裂。DeepSeek V4.1 Flash 0910 在 bare 定理证明上一道都没做出来，但它在构造任务里产出过优于参考基线的结果。

8 个同时参加完整版和轻量版的模型，综合指数排名的斯皮尔曼相关系数是 0.93。28 对模型排名里有 26 对顺序保持一致。这意味着 20 道题的轻量版就能基本代表 100 道题完整版的区分度。

但这篇论文最重要的结论，不是谁考了第一。

是大模型在 TCS 上的能力分布极其不均匀。

同一个模型，可能在裸命题定理证明上一道都做不出来，但在构造任务上能改进人类的公开记录。DeepSeek V4.1 Flash 0910 就是最极端的例子，bare 定理证明 0 分，但构造任务有产出。

另一个发现是提示的杠杆效应。Kimi K3 在 bare 模式解决了 3 道定理，到了 guided 模式能解决 7 道。这说明模型其实知道很多证明片段，只是不知道怎么把它们串起来。给它中间引理和思路提示，能力立刻翻倍。

第三个发现可能是最重要的。哪怕模型没有完整解决公开猜想，它也能产出有数学价值的中间结果。GPT-6 Astra 给出了 Alon-Jaeger-Tarsi 猜想在 F₅域下 n≤9 的形式化验证特例，拓展了人类之前已知的范围。这些特例和边界结果，虽然不能直接解决猜想，但本身就是数学贡献。

之前我们评测大模型做数学，要么看定理证明完成率，要么看竞赛题得分。这篇论文告诉我们，中间产出同样重要。一个模型可能解不出最终猜想，但它能帮数学家把某个特例验证了，把某个上界改进了，把某个求解器跑通了。这就是实实在在的科研贡献。

那么，离真正的 AI 数学家还有多远？

30 道公开猜想，0 个完整解决，这个数字很说明问题。

大模型现在能做的，是在给定框架内改进已有结果，是把已知的证明片段重新组合，是在人类画好的边界里再往前推一小步。

真正的猜想解决需要的东西不一样。它需要跳出现有框架，提出全新的概念和方法，需要在黑暗里找到方向。这些能力，目前的大模型还不具备。

论文里提到，有两个模型复用了 OpenAI 已经公开的 Ryser 猜想和 MIRUP 猜想反例，完成了两道公开猜想任务。这不是原创发现，只是搬运。

姚期智和杨植麟做这件事的意义，不在于宣布 AI 数学家已经诞生。而在于第一次给 TCS 研究的完整链条建了一个可复现、可自动校验的评测框架。

有了这个框架，后面模型迭代到什么程度，就有了一把统一的尺子。

现在的第一名是 GPT-6 Astra，综合指数 71.9。这个数字明年会是多少，我们等着看。