好家伙，图灵奖得主姚期智，和 Kimi 创始人杨植麟，首次联手发论文了？！

就在最近上传至 arXiv 的一篇论文中，两人的名字同时出现在作者栏。

（P.S. 至少从目前检索到的公开论文记录来看，尚未发现两人此前共同署名的论文。）

这俩人，一位是理论计算机科学领域的泰斗，一位是如今国内大模型创业圈的代表人物。

如今凑到一起，研究的还是个相当硬核的问题：

当下的顶尖 AI，到底能不能像真正的科学家一样，搞理论计算机科学研究？

巧了不是，前两天 Jeff Dean 和李飞飞对谈时，刚好聊过类似的话题。

当时李飞飞就问，AI 如今已经能自动做实验了，但像牛顿、爱因斯坦那样搞理论研究，它也能胜任吗？

Jeff 的回答相当乐观：

他认为，AI 同样有能力开展高水平的理论研究，甚至可以自主寻找能够解释实验现象的新理论。

结果这边话音刚落，姚期智和杨植麟等人就通过论文提出的全新基准 TCSEXAM，直接给了所有人一记暴击：

强如 GPT-6 Astra，虽然在研究级定理证明中拿下了 70% 的成功率，但是面对 30 道人类尚未解决的开放猜想，一道都没能独立攻破。

一道都无，0，大鸭蛋。。。

所以，这个将所有模型打回原形的基准，到底什么来头？？

GPT-6 Astra 证明 70% 研究级定理，却被 30 道开放猜想难住了

TCSExam，全称 Theoretical Computer Science Exam。

顾名思义，专门考理论计算机科学。

说实话，以前看各家刷数学榜，我基本已经脱敏了。

不是高中奥数题库翻来覆去洗，就是搞几道早已被人类证明得明明白白的本科教材题，模型背过多少套路，跑分就能冲多高。这种打榜除了给技术发布会凑几页 PPT，对真实的科研工作几乎零参考价值。

TCSExam 这次有点不一样。

100 道题，瞄准的都是科研级任务。

题目具体分为四类：

20 道形式化定理证明题：给出数学命题，让 AI 用 Lean 4 写出能够通过机器检查的证明。

30 道求解器工程题：考验 AI 能否编写、改进算法与求解程序，真正解决计算问题。

20 道数学构造题：按照给定条件，构造出符合要求的数学对象。

30 道开放猜想题：直接挑战人类目前尚未解决的理论问题。

从证明已有定理，到挑战人类尚未解决的猜想，难度逐渐离谱。

更绝的是评判机制。

告别以往的人工肉眼打分或者大模型当裁判互吹彩虹屁，所有考题全部对接 Lean 形式化内核与自动化验证工具。

代码跑得过就是跑得过，跑不过当场报错，绝不存在一丝模糊空间。

然后就到了检验环节了。

他们把 GPT-6 Astra、Kimi、DeepSeek、Qwen 等一众前沿模型拉上了考场，结果成绩单一出来，还真有点意思。

在完整版 TCSExam-Full 上，GPT-6 Astra 以 71.9 分拿下第一，Kimi K3.1 Pro 以 57.4 分紧随其后。

GPT-6 Astra 断层第一？怎么做到的？

原来它在已解的研究级定理证明里表现堪称恐怖，直接轰下了70%的通过率。

很多人类博士生抓耳挠腮几天都啃不下来的证明链条，它硬生生用形式化语言严丝合缝地填满了。

我当时看完这个数字也是心头一紧：难道 AI 做理论科研的奇点真要到了？

然后转头看第二部分，当场被浇了一盆冷水。

面对那 30 道真实世界里的开放猜想，没有任何一位参赛选手能独立攻破哪怕一道。

表格里虽然有两个模型零星得分了，但根据论文的说法，它们在证明过程中用到了联网搜索，直接 " 抄了 "OpenAI 此前公开发表的反例和证明，所以本质上不算独立解决。

（就……一时间无语凝噎）

懂套路、能做题，甚至能完成极其复杂的研究级推导，但只要走出人类已知知识的边界，推开门面对彻底的未知荒原，大模型瞬间就现了原形。

世界难题没攻破，AI 却顺手刷新了部分数学结果

不过，先别急着下结论说 AI 科研彻底寄了。

当你以为它们全面扑街的时候，有几个细节却让人眼前一亮。

在测试极端边界条件的时候，这群模型没有像传统意义上那样证明出一个完整的宏大猜想，但在具体的数学构造上，它们居然顺手越界，把人类长期保持的记录给刷了。

比如在极值图论领域，Kimi 就直接多连出了一条边。

这类问题说起来很简单：

给你一堆点，让你尽可能多地连线，但不能出现某些特定的环路。

听起来像小学生连线题，实际上每多连一条边，都可能让整个图违反限制条件。

结果呢？

在 124 个顶点的条件下，论文引用的参考构造有 629 条边，Kimi K3 愣是连出了 630 条，而且完全符合规则。

别小看这一条边，在极值图论里，数学家研究的恰恰就是：

在严格限制下，一个结构究竟能做到多大、多复杂？

多出来的这一条边，意味着原先参考结果所达到的边界，还能继续往前推。

不仅如此，在通信与编码理论的关键战场——纠错码问题上，Kimi 又把最小汉明距离从 5 提升到了 6。

通俗理解，信息传输时，我们通常会把数据编码成一串串 0 和 1，为了避免传输出错，就希望不同编码之间尽可能容易区分。

而 Kimi 这次找到了一组新的编码，在题目规定的条件下，让任意两组编码之间至少有 6 个位置不同，比参考方案还多了一个。

别看只是从 5 到 6，这背后研究的可是如何让信息在出现错误时，依然能够被可靠识别和恢复。

另一边的 GPT-6 Astra 也没闲着。

在另一道二进制编码问题中，它把码字数量的参考上界从 84 进一步收紧到了 82。

相当于把一道数学难题的答案范围，又往前逼近了一步。

所以说，虽然 AI 还无法独立攻破那些困扰人类多年的开放猜想，但它已经开始在具体的数学问题上，拿出比已有参考结果更好的答案。

而这，恰恰是 TCSExam 这张榜单最有意思的地方。

它让我们第一次如此直观地看到，AI 距离真正独立开展理论研究，究竟还有多远。

能证明已有的定理，也能在具体问题上取得新进展。

但面对那些连人类都没有答案的难题，AI 显然还有很长的路要走。

等等，姚期智和杨植麟，怎么走到了一起？

研究结果聊完了，这篇论文的作者阵容，其实也挺有意思。

一看名单，估计很多人的第一反应和我一样：姚期智和杨植麟，怎么走到了一起？

顺着学术谱系往回倒推，两人的交集早在一个地方就埋下了伏笔。

没错，正是清华 " 叉院 "（交叉信息研究院）。

姚期智是叉院的创立者，也是大名鼎鼎的清华 " 姚班 " 创办人。

而杨植麟除了清华计算机系本科、卡内基梅隆大学博士这段经历，还有一个容易被忽略的身份：

他曾担任清华大学交叉信息研究院助理教授。

等于既是广义上的 " 师生关系 "，又是 " 同事关系 "。

而且，两人的交集还不止清华。

2021 年至 2024 年，杨植麟还曾担任上海期智研究院 PI，也就是独立研究负责人。

巧的是，这家研究院同样由姚期智领衔创办。

再看论文的另外三位作者，罗一凡、刘正颖和袁洋，分别与清华大学、月之暗面及上海期智研究院有关。

五位作者，三家机构。

一边是深耕理论计算机科学的学术团队，一边是训练前沿大模型的 AI 公司。

这么一看，这次合作倒也在情理之中了。

而且重要的是，双方关注的问题，恰好也能对上。

今年 9 月，姚期智在清华研究生开学典礼上就谈到，AI 已经开始在数学、理论计算机科学等高度抽象的领域取得突破。

另一边，杨植麟此前也曾判断，2026 年很可能成为 AI for Science 的重要突破年份。

如今两人的名字出现在同一篇论文上，研究的正是一个很具体的问题：

AI 到底能在理论科学研究中走多远？

TCSExam 给出了一份阶段性答卷。

能证明已有定理，也开始产出新的数学结果。

至于独立攻破世界难题嘛……还得继续练。（doge）

（P.S. 光一个人练肯定不行，所以他们顺手也把 TCSExam 开源了）

论文：https://arxiv.org/abs/2611.07962

开源仓库：https://github.com/MoonshotAI/TCSExam

参考链接：

[ 1 ] https://x.com/NFT_Chen/status/2119716134752776536

[ 2 ] https://x.com/rohanpaul_ai/status/2119501674465439786

一键三连「点赞」「转发」「小心心」

欢迎在评论区留下你的想法！

—  完  —

点亮星标

科技前沿进展每日见