图灵奖得主姚期智与月之暗面创始人杨植麟，首次联手发论文了。
这篇论文名叫 TCSExam。
论文于一周前在 arXiv 公开，五位作者来自清华大学、月之暗面和上海期智研究院。他们把目光放在了大模型的科研能力上：一份完整证明、一段可复用的程序、一个满足条件的数学对象，模型到底能完成哪些工作？
研究团队为此准备了 100 道理论计算机科学任务，把定理证明、求解器工程、数学构造和开放猜想放进同一套评测。任务要有明确的交付物，证明交给 Lean 内核，程序和构造则接受相应检查器的验证。
这张考卷考什么
理论计算机科学研究有不同的工作方式。有人寻找证明，有人写程序搜索，也有人通过一个具体构造，改进某个问题的已知界限。TCSExam 按研究者需要交出的东西，划分了四条轨道。
20 道定理证明题，要交完整的 Lean 4 证明。 题目来自2023至2026年的研究论文，覆盖13个子领域。主评测提供目标命题、定义和数学假设，不给中间引理，让模型自己找到证明路线。
30 道求解器工程题，要交能反复使用的程序。 模型拿到问题、朴素基线和公开实例，开发自己的算法实现，最终在隐藏实例上运行。图着色、车辆路径、作业调度、逻辑综合，都在其中。
以逻辑综合为例，模型写出的程序要生成与原电路功能一致的电路，检查器先验功能，再比较与门数量。同一段程序还要处理一批不同输入，不能只把某一个例子做漂亮。
20 道数学构造题，要交具体对象和性质证书。 一张满足约束的图、一套纠错码，都可以成为答案。先确认对象有效，再把它的参数与文献中的参考结果比较。
30 道开放猜想题，接受完整证明或反驳。 每道题都留有两个 Lean 证明位置，分别对应命题及其否定。找到反例也可以，但需要证明它确实推翻了题目中的命题。
这些任务里的证明、程序和构造还能互相配合：程序搜索出候选对象，证明确认它的性质，一个构造又可能成为某个猜想的反例。
答案怎样验收
把研究论文变成机器能检查的任务，本身也需要反复核对。
一句定理里的定义、量词、假设和参数范围，都要对应到形式化命题里。少了一个条件，或者把范围缩小了，模型即使交出通过验证的代码，也可能已经换了一道题。
TCSExam 的开发流程中，研究者先挑选有研究意义的问题，Agent 辅助编写题面、提交接口和检查器，再由独立上下文中的审查、试跑和领域专家确认。题意错配、检查器问题和异常结果，会退回修改。开发期间，40多道已被试跑解出的定理题退出了候选集。
提交之后，还要区分局部推导与完整证明。
模型可能先证明某个中间引理，也可能在假设其他引理成立的情况下完成一个步骤。这些检查能帮助定位它卡在哪里；整道题要拿到完整证明分，仍须去掉尚未证明的中间假设，再独立检查主定理。
构造超过参考值时，团队还会回查文献，核对原先的界限、问题参数和比较条件。对象有效与是否产生了新结果，是两项不同的检查。
运行设置也公开了。一次尝试最多有12小时开发时间，模型可以调用工具、写代码、调试，再提交最终产物。定理和求解器任务不能自由上网，构造和开放猜想则允许查文献。
论文比较的是模型与执行 harness 组成的 Agent 系统：Astra 搭配 Codex，Kimi 使用 Kimi Code，另外还有 Claude Code 和 Grok Build。Full 评测了8套系统，Lite 从100题中各类选5题，再加入 Opus 5.5，共比较9套系统。
模型交出了什么
构造题里有一个很直观的例子：给定124个顶点，尽可能多地连边，同时不允许出现三角形或四边形。
Kimi K3 交出了一张 630 条边的图，比论文采用的629边公开参考构造多一条。图中所有顶点和边都能从提交的证书中提取，再逐一检查约束。这把已知构造的下界往前推进了一步，最大可能边数仍待研究。
论文图5a Kimi K3提交的124顶点630边构造 绿色标出一个五边形
Kimi K3 还构造了 [[25,7,6]] 量子稳定子码：用25个物理量子比特编码7个逻辑量子比特，将对应参考码的最小距离从5提高到6。
Astra 也达到了这两项构造参数。Qwen3.8 Max、Grok 4.6 和 DeepSeek V4.1 Flash 0910，同样得到了630边的图。
论文图5b Kimi K3提交的量子纠错码 每行对应一个稳定子生成元
不同研究环节差距很大
完整版综合得分中，GPT-6 Astra 为 71.9，Kimi K3.1 Pro 为 57.4，Kimi K3 为 46.8。轻量版只保留20道题，Opus 5.5 以72.3分居首，两种试卷的成绩分开报告。
论文表2 完整版100题结果 开放猜想的非零分包含对已发表结果的适配
定理证明拉开了最大的差距。Astra 对20道题各尝试一次，完成了14道，成功率70%。Kimi K3.1 Pro 每题尝试3次，60次中成功23次，成功率38.3%，至少做出过一次的不同定理共有9道。
具体到单题，优势又可能倒过来。PCP 字母表与可靠性那道题，Kimi K3.1 Pro 三次全部完成，Astra 的一次尝试没有成功。
DeepSeek V4.1 Flash 0910 在60次定理证明尝试里没有成功，却能通过搜索和已有文献交出630边构造。证明、编程搜索与数学构造，并没有随着总分一起整齐变化。
研究团队还给 Kimi K3 和 DeepSeek 0910 做了三档引导实验：只给目标命题，再补中间引理，最后进一步提供证明思路。
Kimi K3 至少成功过一次的定理数，依次是 3道、4道、7道；DeepSeek 0910 则是 0道、2道、6道。同一组题，给到哪些研究线索，会明显改变模型能走多远。
猜想没有解完
30道开放猜想里，有两道出现了通过验证的完整提交，但它们用到了已经发表的成果。
这些题是在 OpenAI 公布相关反例和 Lean 证明之前选的。等 Kimi K3.1 Pro 和 DeepSeek V4.1 Flash 1017 参加联网评测时，相关结果已经公开。模型检索到 Ryser 猜想和修正整数进位猜想的已有成果，再适配到 TCSExam 的定义中，通过了检查。
其余28道猜想没有被完整解决。不过，完整解题记零分的地方，也留下了进展。
Astra 在尝试 Alon–Jaeger–Tarsi 猜想时，证明了 五元素有限域上、维度不超过9 的情形，将论文对照的已有维度范围从8推进到9。研究团队另起干净环境重建 Lean 项目，并独立复算了证明中的整数证书。
论文图6 九维Alon Jaeger Tarsi特例的证明证书
完整猜想仍未解决，这个九维特例已经是一份可以检查、可以继续推进的研究结果。
TCSExam 的题目、环境构建和评测工具都已开源。想继续研究的团队，可以从原题、提交接口和验证过程接着往下做。
参考链接
-
TCSExam 论文 v1：https://arxiv.org/abs/2611.07962v1 -
项目与交互结果：https://moonshotai.github.io/TCSExam/ -
任务与评测代码：https://github.com/MoonshotAI/TCSExam