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 这种对严谨程度要求最狠的领域，最强的几个模型的确能独立完成一部分研究水平的证明、求解和构造工作，甚至改进参考答案。只是这种本事高度集中在少数几个模型身上。

但 " 解决前人未解难题 " 这道坎，考场上的模型始终没跨过去。归根结底一句话，始终没有模型能靠自己 " 摘皇冠上的明珠 "。