文 | 字母 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%，开放猜想 0.0%。
以第一名 GPT-6 Astra 的 71.9 分为例子，定理 70.0%×30 得 21 分，求解器 64.7%×30 得 19.4 分，构造 104.9%×30 得 31.5 分，猜想 0 分，加起来正好 71.9。
第一名 GPT-6 Astra 领先第二名 Kimi K3.1 Pro 14.5 分；从第三名 Kimi K3 到第八名 DeepSeek V4.1 Flash 0910，六个模型挤在 40 到 47 分之间，彼此差不到 7 分。
轻量版多了一位考生，Anthropic 的 Opus 5.5。它只参加了轻量版，并且一来就拿了第一。
5 道定理题，Opus 5.5 证出 4 道（80.0%），Astra 证出 3 道（60.0%）。两家的构造分一样，都是 100.4%；求解器 Astra 还高一点，63.0% 对 60.5%。
两张榜单的排名高度一致。
8 个两边都参加了的模型，任意挑两个比谁先谁后，一共能挑出 28 对，其中 26 对的先后顺序在两张榜上一模一样。统计上有个专门衡量两份排名像不像的指标，叫斯皮尔曼相关系数，完全一致是1，这里是 0.93。也就是说，轻量版虽然只有 20 道题，排出来的座次是靠得住的。
但是这种考试不能光看分数，还要看分布情况。
求解器这一项，各家大差不差，最低 43.8%，最高 64.7%。构造也是如此，从 86.2% 到 104.9%。可唯独定理证明这一块，70.0%、38.3%、11.7%、6.7%、5.0%、5.0%、5.0%、0.0%，一路断崖。
这就跟高考一样，前面的基础题大家分数差不多，一到最后的压轴大题，差距一下子就拉开了。
会证明和会构造，也不是一回事。
DeepSeek 0910 在 60 次定理证明尝试里，一份完整证明都没交出来，却在构造题里做出了超过参考纪录的结果。GLM-5.3 构造平均 97.7%，稳得很，但一次也没超过参考纪录。Astra 最全面，30 道求解器题里，有 27 道拿了最高平均分。
Kimi K3.1 Pro 也不是处处落后于 GPT。有一道关于概率可检验证明（PCP）的定理，它三次全证出来了，第一名 GPT-6 Astra 那一次没证出来。
打个比方，这些模型都是外卖骑手小哥。
你让他把一条没跑过的路线从头写清楚，每一步都得说出为什么这么走，他一句也写不出来。可真塞给他一堆订单，他却能排出一个谁也没排过的送法，核查下来，还真更快。DeepSeek 0910 就是这样的骑手。
那定理证不出来，是真不会，还是差一口气？论文专门做了个对比：同样 20 道定理，每题 3 次机会，分三档提示来考。Kimi K3 裸考解出 3 道，列出中间结论后解出 4 道，连思路也给了，解出 7 道。DeepSeek 0910 是 0 道、2 道、6 道。有人递台阶，模型是爬得上去的。
构造题里有几个实打实的新结果。
Kimi K3 造出了一张图：124 个顶点、630 条边，里面既没有三角形，也没有四边形。这类题的玩法可以这么想：124 个村子之间修路，路修得越多越好，但任何三个村子之间不能修成一个三角形的环线，任何四个村子之间也不能修成一个四边形的环线。文献里此前的最好成绩是 629 条边，它多连出了一条。
同一个模型还交出一套[[25,7,6]]量子纠错码。量子计算机很容易出错，纠错码就是给数据加的一层保险。好比寄易碎品，真正要寄的东西只有 7 件，却占了 25 件的地方，多出来的全是防撞的泡沫。这套码用 25 个量子比特保护 7 个量子比特的信息，方括号里最后那个 6 叫“最小距离”，越大说明保险越牢。此前同样规格的码，这个数是5，它提到了6。通俗地说，能检测出的错误，从最多涉及 4 个量子比特扩大到了 5 个。
这两项成果，论文里展示的是 Kimi K3 交的答卷，同时注明 Astra 也达到了同样的参数；项目主页上，量子码则挂在 Astra 名下。两个模型是各自做出来的。那张 630 条边的图，Qwen3.8 Max、Grok 4.6 和 DeepSeek 0910 也各造出了一张。
Astra 另有一项成绩，和编码有关。问题是这样的：用 22 位长的 0 和 1 串当“码字”，要求任意两个码字之间至少有 10 位不一样，这样的码字最多能有多少个？这好比发车牌：每张车牌 22 位，任意两张至少有 10 位不同，这样就算看错三四位，也不会把这辆车认成那辆车。
问题是，这样的车牌最多能发多少张？2012 年发表的结论是不超过 84 个，Astra 证明了不超过 82 个，把这个上限又压低了2。注意，这不是造出了更多车牌，而是把天花板量得更准了。Astra 的构造平均分 104.9%，20 道题里 17 道追平参考纪录，3 道超过。
求解器方面，在前面说的那道精简电路的题上（题目来自 IWLS 2023 竞赛），Astra 写的程序对 100 个测试电路全部给出了功能正确的结果，其中 22 个用的元件比参考答案少，31 个打平，47 个比参考答案多。这是“能用”，不是“全胜”。
最难的猜想题，考得怎么样？
30 道猜想，只有两个模型的得分不是0：Kimi K3.1 Pro 1.1%，DeepSeek 1017 5.6%。不过说实话，这和0% 也没什么区别。
拆开看，被判通过的提交一共 6 次，只涉及 2 道题。一道是 Ryser 猜想，Kimi K3.1 Pro 3 次里过了 1 次，DeepSeek 1017 3 次里过了 2 次；另一道是 MIRUP（修正整数上取整猜想），DeepSeek 1017 3 次全过。其余 28 道，一个完整的解都没有。
而且这 6 次还不是模型靠自己推理出来的，全都是查资料查到的。
前面说过，猜想题是开卷，允许上网。研究团队出题的时候，这两道题确实还没人解开。可等到 Kimi K3.1 Pro 和 DeepSeek 1017 上考场时，OpenAI 已经把这两个猜想的反例和 Lean 证明公开发表了。两个模型在网上搜到了，改写成考试要求的格式，交了上去。
相当于开卷考试时，答案刚好印在了参考书上。
论文没有回避这一点，在成绩表下面专门加了说明，还提出今后可以在断网条件下，用考试当时仍然没人解开的猜想来考。论文同时写了一句：OpenAI 的这些结果，显示了 AI 辅助解决猜想的潜力。只是这份功劳，记不到考场上这两位考生头上。
但 0 分不等于没产出。
Astra 在攻一个叫 Alon-Jaeger-Tarsi 的猜想时，整个猜想没拿下，却独立证明了其中一部分。这个猜想可以按规模n从小到大，一级一级去证，好比爬一栋没有顶的楼。在其中一种设定下（数学上叫“五元有限域”），前人 1999 年证到了n≤7，今年一篇预印本报告证到了n≤8，Astra 证到了n≤9，等于又往上爬了一层，并且通过了 Lean 的独立验证。按规则，整个猜想没解开，这道题它照样是 0 分，因为猜想说的是每一层都成立，这栋楼还远没爬到头。
论文另外还列了 4 个类似的局部结果，分属另外几个数学问题，同样经过了验证。
也就是说，至少往前走了一小步，不至于说是毫无进展。
还要提醒一句：这张成绩单上的数字，换一种算分方法，可能就是另一个样子。
求解器原本的算分公式是(B−A)/(B−K)。B是最笨解法的成绩，K是参考答案的成绩，A是模型的成绩。
你可以把它想成一段跑道：最笨解法是起跑线，参考答案是终点线，看模型从起跑线往终点跑了多远。跑到终点得1，也就是 100%；原地没动得0；要是倒着往回跑，就是负分。
这个公式有个毛病，单独一道题的得分可以离谱到把整科成绩带歪。Qwen3.8 Max 就碰上了：在 IWLS 2023 的一个电路（编号 ex37）上，它交的电路功能没错，却用了 273,020 个 AND 门，而最笨的解法只用 698 个，参考答案只用 106 个。代进公式，这一道题的得分大约是−460，等于朝反方向跑出去了四百多条跑道那么远。
所以论文另外设计了一把尺子，拿 Kimi K3 的成绩当参照，每道题的得分限制在 0 到 100 之间。Qwen3.8 Max 的求解器成绩，按原来的公式算平均是 64.7%，按新尺子算只有 49.2%。前面成绩单上用的是新尺子。
构造题也类似。成绩要先按公式换算成百分数，20 道题里有 14 道用的换算方式比较特殊，其余 6 道是按比例直接换算。同样的进步，换算出来的分差可能被放大，也可能被压缩。所以论文坚持把原始的数字一并报出来：边数从 629 到 630，最小距离从 5 到6，码字上限从 84 到 82，而不只说一个“104.9%”。
说到底，在 TCS 这种对严谨程度要求最狠的领域，最强的几个模型的确能独立完成一部分研究水平的证明、求解和构造工作，甚至改进参考答案。只是这种本事高度集中在少数几个模型身上。
但“解决前人未解难题”这道坎，考场上的模型始终没跨过去。归根结底一句话，始终没有模型能靠自己“摘皇冠上的明珠”。
