姚期智杨植麟联手，让数学家松了一口气

文 | 字母AI 11月5日，有这么一篇新论文挂上了arXiv。 五位作者来自月之暗面、清华大学和上海期智研究院，其中两个名字格外显眼：一位是图灵奖得主、清华大学交叉信息研究院院长姚期智，一位是月之暗面（Kimi）创始人杨植麟。 论文标题是《TCSExam：对前沿大语言模型开展全领域理论计算机科学研究评估》（TCSExam: Evaluating Frontier LLMs on the Full Range of TCS Research）。 一句话概括，他们出了一张卷子，拿去考当下最强的一批AI大模型。 TCS是理论计算机科学（Theoretical Computer Science）的缩写。它不管怎么修电脑、怎么写代码，它琢磨的是“计算”这件事本身。 程序员像司机，想的是发动机和内饰，而TCS则是交通，从甲地到乙地最快到底能有多快，有没有哪条路注定走不通。 这是数学和计算机科学的交叉地带，所有问题都围着“计算”两个字转，做研究主要靠证明。 这篇论文出来的时间点有点微妙。10月初，OpenAI一口气公开了722篇由AI写出的数学手稿，按相关性归成372个“结果族”，覆盖数论、理论计算机、几何、数学物理等17个领域。“AI把数学干废了”的话题，一度冲上微博热搜。 陶哲轩曾对《自然》（Nature）表示，AI在几乎所有领域都有个致命伤：会犯没法核验的错误。唯独数学不一样，尤其是证明，对不对可以交给机器自动检查。这有点像数独，填出来难，填完了对不对，查一遍就知道。所以AI公司最没有争议的成绩，会出在数学上。 可姚期智和杨植麟这篇论文考下来，结论有点泼冷水： 那些至今悬而未决的开放猜想，没有任何一个参考的模型能靠自己解开。 大模型有那么多基准， 为什么还要出卷子？ 大模型的跑分几乎每两个月就涨一轮，各种榜单让人看得头晕眼花。可实际上，这些榜单只能证明模型会做题，却不能反应出模型的研究水平。 做题本质上是照着菜谱炒菜，步骤是现成的，味道是有标准的，你也没见过锅包肉里面加巧克力的对吧？而研究没有规定好的步骤，最后能不能成，事先谁也拿不准，甚至于很多问题连出题的人自己都不知道答案。 更麻烦的是判卷。模型一口气写出几百页“证明”，谁有工夫一页页看？它说自己攻破了一个几十年没人解开的猜想，又有谁能证明它写对了？ OpenAI那722篇手稿就是现成的例子。 这篇论文想弄清的就是这件事：真让AI去干研究的活儿，它到底能干成什么样。 办法是只出机器能判卷的题。 题目越像真研究，越难判分； TCS恰好是个例外，它的结论大多能被机器验证。 卷子一共100道题，分四类，对应理论计算机科学家平时干的四种活。 第一类，定理证明，20道。 题目是从2023到2026年的TCS论文里摘出来的定理，都是研究人员正式发表过的成果，覆盖13个细分方向。 模型要从头到尾写出一份完整的证明，而且不能用大白话写，得用一种叫Lean 4的专门语言来写，方便机器检查。这就像去窗口办事填表，每一栏都得按规定的格式填，写篇作文交上去是不收的。考法分三档，可以拿爬山来理解。 第二类，求解器工程，30道。 “求解器”就是专门用来解某一类题的程序。这类题不是让模型解一道题，而是让它写一个程序，把同一类的题都解了。 模型会拿到一份问题说明、一个最笨的解法和一批公开的例题。比如给一批电路，要求功能不变，把里面一种基本元件（AND门，也叫与门）的数量尽量压下去，元件越少越好。 第三类，显式构造，20道。 前面都是让模型“纸上谈兵”，到了构造这一步，就得让模型把东西造出来。 第四类，开放猜想，30道。 这些题目是至今没人证明、也没人推翻的猜想。 老百姓最熟的开放猜想大概是哥德巴赫猜想，提出两百八十多年了，我也没看到谁能给出一个靠谱的证明法。 卷子上这30道没那么出名，性质是一样的。每道题留两个空，一个填“猜想成立”的完整证明，一个填“猜想不成立”的完整证明，填满其中一个才算数。 而且这一栏没有步骤分，解不开就是0分。 题目先由专家按三条标准挑选：有没有研究价值，领域覆盖全不全，结果能不能验证。 100道题全部经过专家审阅。接着让一个AI助手把题目翻译成Lean语言、写好评分程序，再让另一个独立的AI助手回头对照原论文，逐条核对题目的条件和范围有没有抄错，还要拿一些特殊的小例子去试，再把Lean写的题目翻回人话比一遍，防止题目在翻译里走了样。 试考阶段，有40多道定理题因为被模型做了出来，所以这些题直接淘汰。正式考试里，哪道题意外被证出来，或者分数高得反常，都会触发对题目和出处的重新审查。 不光是这样，假如模型在考试中刷新了纪录，AI还要重新审它的整个运行过程。 就和你参加过的所有考试一样，TCSExam也限时。 每道题每次作答，最多给12个小时，按现实里流逝的时间算。Kimi K3、Kimi K3.1 Pro和两个版本的DeepSeek每题考3次，其余模型每题考1次。100道题各考一遍，最多要用1200小时。 而且TCSExam也分开卷和闭卷。微积分、概率论闭卷，马哲、思修开卷，上过大学的都懂。TCSExam里，定理证明和求解器这两类不让上网，只有构造和猜想两类允许查文献。记住这一条，后面有用。 考一次完整版太费时间，所以还有个轻量版Lite：四类题各抽5道，一共20道，每次作答的时限不变，题量砍掉80%，最多要用240小时。题目、代码和评测工具全部公开，谁都可以拿去复查。 最后，四类成绩合成一个总分，叫TCSExam Index。算法很简单：定理证明、求解器、构造三类各占30分，开放猜想占10分。写成公式是I=30P+30S+30C+10O，P、S、C、O分别是这四类题的平均得分。 分数如何呢？ 看成绩之前，先说清楚每一项怎么读。 参加完整版考试的有8位考生：OpenAI的GPT-6 Astra，月之暗面的Kimi K3和Kimi K3.1 Pro，智谱的GLM-5.3，阿里的Qwen3.8 Max，xAI的Grok 4.6，还有DeepSeek V4.1 Flash的两个版本（0910和1017）。成绩按总分从高到低排： 第一名GPT-6 Astra，71.9分：定理证明70.0%，求解器64.7%，构造104.9%，开放猜想0.0%。 第二名Kimi K3.1 Pro，57.4分：定理证明38.3%，求解器54.1%，构造98.6%，开放猜想1.1%。 第三名Kimi K3，46.8分：定理证明11.7%，求解器48.7%，构造95.5%，开放猜想0.0%。 第四名DeepSeek V4.1 Flash 1017，46.0分：定理证明6.7%，求解器53.1%，构造91.8%，开放猜想5.6%。 第五名GLM-5.3，45.5分：定理证明5.0%，求解器49.1%，构造97.7%，开放猜想0.0%。 第六名Qwen3.8 Max (0902)，44.8分：定理证明5.0%，求解器49.2%，构造95.1%，开放猜想0.0%。 第七名Grok 4.6，40.5分：定理证明5.0%，求解器43.8%，构造86.2%，开放猜想0.0%。 第八名DeepSeek V4.1 Flash 0910，40.4分：定理证明0.0%，求解器48.3%，构造86.6%