人工智能真的能够在理论计算机科学领域里发挥作用并且成为一个合格的科学家吗? 这一问题目前已经得到了回答, 答案是肯定的。这一结果的依据来自于由姚期智先生和杨植麟先生共同署名的一篇学术文章的内容展示。
要是把理论计算机科学说成是在数学领域举办奥林匹克运动会的话, 那么它研究的根本就不是如何去修理电脑这种日常杂事, 而是去探究计算这件事情本身能够达到什么样的上限。具体来说是什么问题能够在相对比较快的速度之内被运算出来, 还有在进行数学证明时, 那些边界和极限究竟会存在在哪里。
在这个时候, 有相当一批属于前沿性质的大规模语言模型加入了这一行列之中, 这其中既包括了GPT这样的产品, 也包括了其他许多种类的人工智能大模型, 它们全部作为参与者来奔赴这场被称为奥林匹克的盛会了。
2025年11月9日, 澎湃新闻的记者知道了这么一件事, 最近图灵奖的得主, 还是中国科学院的院士, 也是清华大学交叉信息研究院院长姚期智的团队, 他们联手了叫作月之暗面的这家公司的创始人杨植麟等一众人员, 一起发表了有署名的学术文章, 那篇文章的名字叫《TCSEXAM: 在TCS研究的全范围内评估前沿大型语言模型》。
在论文里, 推出了一个叫 TCSExam 的“统一考试”, 称这是第一次把理论计算机科学研究的完整链条都纳入到评测里面去。
在关于大模型的研究文献里面, 总体一共设定了四个类别的考试题目, 并且每一个类别都安排了机械化的自动计算检验程序, 从而面向在全球范围内处于前沿位置的九个大型人工智能模型, 出具了一份用于测试理论计算机科学能力的标准化书面考核材料。
第一类是这样的定理证明这件事, 就是拿出研究级别数学界的定理来交给那个叫做人工智能的系统, 让它把非常严密的证明过程给写出来, 这个证明需要借助一种被称作是Lean 4的软件去编写, 大家完全可以把它理解成为是用来自动批改数学作业的一种工具, 它这个地方完全不认识那些含含糊糊的表达方式, 但是它只认那种逐行进行严格推敲的逻辑关系, 然后执行批改工作的是那个叫做Lean内核的东西, 这相当于就是一台机器在进行逐行的验算工作。
第二种类别涉及 solver 工程学领域, 其核心理念并非让人工智能为具体题目固定单一答案, 而是引导其开发一套具有普遍适用性的解题工具代码, 随后运用海量具体的测试样本进行运行验证, 例如输入包含多个图形的数据结构并促使该工具识别其中规模最大的团簇或最优的分割策略, 关键在于最终生成的程序必须具备可复用特性且不能依赖对既有结果的机械记忆。
第三类构造, 其含义是指要求人工智能交付一个特定的、具体的数学对象, 这个对象可以是一幅图, 或者是一个编码集合, 也可以是某种几何排列方式, 此外, 还必须同时提供一个被称为“证书”的东西, 该证书的功能是用来作为凭证, 以证明前述对象确实符合相应的规范要求, 随后计算机会对这一对象以及对应的证书进行核查, 从而确认两者是否完全相符且彼此匹配。
第四类是开放猜想。把那些几十年里既没有人证明出来、也没有被人推翻的数学难题交给AI去处理。要求就是让AI把这个猜想完整地证明出来, 或者把它完整地反证清楚。所谓把猜想反证清楚, 意思就是要拿出一个反例来。同时, 还要把这个反例确实能够推翻原猜想的道理给讲明白、证明出来。
在最受关注的定理证明这个类别里面, 有一个情况值得提一下。GPT-6 Astra表现得很突出。它的条件是“裸考”, 意思就是只给主定理, 不给中间引理。面对20道题, 它成功完整证明了14道。
这么算下来, 它的成功率达到了70%。Kimi K3.1 Pro以38.3%的成功率排在第二位。至于其余的多个模型, 它们的成功率很惨, 只有个位数, 甚至有的还是零。
这篇文章的研究结果显示, 若是给人工智能提供所谓的“小抄行为”, 具体操作内容为补充其中间的依据以及推导逻辑的大致方向, 其解决问题的成功率便会发生显著增长。
以Kimi K3模型为例, 它成功解答的定理数量由原先的三道增多至七道, 而DeepSeek V4.1 Flash模型的解答数量则从没有解题到解出六道。这一现象表明人工智能并非彻底缺乏推理能力, 只是它们需要更具支持性的辅助结构, 我们可以把这种东西称为更好的脚手架。
在构造类的情况里, 人工智能做的事情, 不仅仅是要达到人类写出来的那些记录的水平, 甚至出现了已经超过这些记录的事儿。
Kimi K3造出了一个有124个顶点, 且有630条边, 既没有三角形也没有四边形的图, 这个图的边数超过了论文引用的629条边的参考记录, 它还造出了一个量子纠错码, 把这个纠错码的最小距离从5提升到了6。
GPT-6 Astra证明了一个二进制编码的上界, 这个二进制编码的长度是22, 最小距离是10, 它的编码最多只能有82个码字, 这个结果改进了此前发表的84这个数字。
论文还同时发出了提醒, 要求这些所谓的“超纪录”的情况必须得通过独立的渠道去进行核对证实。因为那个用来打分的函数公式它有能力把数值之间的区别给放大起来, 也可能把这种区别给压缩变小。所以, 研究者们还一并报告了那些最最原始的、最基础的那个数学参数数据。
