姚期智与杨植麟团队提出 TCSExam，Kimi K3 将图论参考纪录推到 630 条边

Kimi 刷新 629 条边图论参考纪录，只多加了1条边，为什么数学界等了这么多年？

    作者丨郑佳美

    编辑丨岑   峰

给 124 个点连线，不能出现三角形，也不能出现四边形。此前的参考记录是 629 条——数学界认为这已经接近极限。而Kimi K3 构造出了 630 条边的图，并通过程序验证。

多1条边，听起来不多。但在组合数学里，你每试图多塞进一条边，都需要在全图 124 个点之间重新完成一次精密的结构大重构。这1条边意味着AI第一次在“极值构造”这类研究级任务上，把人类参考纪录往前推了一步。

这项成果来自图灵奖得主、中科院院士、清华大学交叉信息研究院院长姚期智与月之暗面创始人杨植麟等人的联合研究。他们真正想回答的问题是：AI到底能不能做数学研究，而不只是做数学题？

01

「多 1 条边」算不算真突破？

姚期智，图灵奖得主、清华大学交叉信息研究院院长，是中国理论计算机科学的奠基者之一；杨植麟，月之暗面创始人，Kimi背后的推动者。

两代人、两种身份：一位是理论计算机科学的泰斗，一位是大模型创业的一线操盘手，第一次联合署名。

这个组合本身就说明了一件事：AI做科研，已经不是“实验室里的猜想”，而是需要理论计算机科学家和大模型团队坐在一起定义“什么叫算做出来了”。

但在另一面，争议同样如影随形：多构造出一条边，到底算不算真正的科学突破？这算不算只是暴力搜索蒙对的个例？AI真懂背后的数学机理吗？

这正是姚期智团队的核心初衷。如果无法区分‘运气好撞上’和‘逻辑上证明’，AI 就永远只是个黑盒计算器。于是，他们没有继续在传统基准上打转，而是联手搭了一套前所未有的评测系统——TCSExam。

为回答这个问题，他们提出 TCSExam，用 100 项理论计算机科学科研任务，测试前沿 AI Agent 能否证明定理、开发 Solver、构造数学对象，甚至挑战长期未解决的猜想。

论文地址：https://arxiv.org/pdf/2611.07962v1

实验中，GPT-6 Astra 完成了 20 项研究级定理中的 14 项，还将一个有限域矩阵猜想在特定条件下的已知证明范围从 8 维推进到了 9 维。

TCSExam 的核心创新，是将 AI 科研能力转化为可以独立验证的研究成果。 它通过 Lean 4、程序检查器和 Checkpoint 机制，分别验证数学证明、算法表现及中间推导，避免把局部进展误判为完整成果。

其中，Astra 的 9 维证明将复杂的矩阵问题压缩为整数约束，最终利用 143 条方程构造出可核验的矛盾证书。从任务形式化、研究证书设计到数学证明的自动检查，这套框架展示了 AI 参与真实科研的一条技术路径。

02

TCSExam 如何建立评测框架？

一句话：把“AI 做科研”拆成四条可验证的轨道，再用三层机制防止“局部进展被误判为完整成果”。

普通数学考试有标准答案，而理论计算机科学涉及的研究工作差异很大，有的需要证明新定理，有的需要开发最优算法，有的要构造满足约束的数学对象。这些成果的形式不同，评价方式也必须随之调整。

研究团队因此将 100 项任务划分为四条轨道：

• 定理证明（20 项）：覆盖 13 个理论计算机科学领域，要求模型提交 Lean 4 证明。

• Solver 工程（30 项）：要求开发可重复运行的算法程序，在独立测试实例和统一资源限制下评测；

• 数学构造（20 项）：考察模型能否生成符合严格约束的图、纠错码等对象；开放猜想（30 项）：允许模型从证明成立或寻找反例两个方向展开研究。雷峰网

任务划分之后，更复杂的问题出现在数学语言的转换过程中。人类研究者能够理解一段定理描述，但机器验证需要明确的定义、量词、假设和参数范围。任何一个条件发生变化，最终证明的数学含义就可能不同。

例如，一个定理原本要求某种性质对任意规模的图成立，如果转写成 Lean 时额外增加了图规模限制，那么模型即使完成证明，也只解决了范围缩小后的问题。形式化证明系统能够检查代码中的逻辑，却无法自行判断它是否忠实于原始研究目标。

TCSExam 为此建立了任务编写与独立审核机制。编写 Agent 根据研究材料构建形式化命题、提交接口和验证程序，审查 Agent 再核对定义、量词及参数条件，并通过边界样例和试运行排查问题。研究领域专家负责审定任务的研究意义。开发过程中，超过 40 道候选定理因试运行阶段已被解决而退出题库。雷峰网(公众号：雷峰网)

Solver 轨道还额外做了两件事：对部分实例做保持数学性质不变的变换，减少直接复用已有答案；数学构造轨道则固定合法性条件与参考纪录，保证可比性。

对于证明任务，研究团队还进一步控制模型能够获得多少研究指导。Bare 模式只提供定理和必要定义，Ladder 增加中间引理，Guided 则提供证明思路。这三种条件使用相同的主定理，让研究者能够分析模型是在寻找证明路线时遇到困难，还是已经知道关键步骤后仍无法完成推导。

经过这些设计，TCSExam 将研究问题转化成了有明确输入、执行条件和交付要求的任务。但模型提交的成果可能包含大量中间推导，如何从中识别真正成立的数学结论，还需要另一层验证机制。

03

怎样区分局部推理与完整证明？

TCSExam 的底层设计利用了理论计算机科学中的一个重要特点：找解难，验解易。研究团队将这种思想应用于科研评测，要求 Agent 把探索结果整理成验证器能够检查的研究证书。

对于定理证明，这份证书就是 Lean 代码。Lean 内核根据形式逻辑规则检查推导，系统还会审计证明依赖，排除未完成证明占位符和未经允许的额外公理。

不过，研究级定理往往需要多个中间引理，模型可能完成大部分推导，却始终无法处理某个关键步骤。仅凭主定理是否通过，很难判断具体的能力缺口。

TCSExam 因此设计了 Checkpoint 机制，把复杂证明拆成多个中间目标。验证其中一个 Checkpoint 时，系统会暂时把其他 Checkpoint 的命题作为假设，检查模型能否在这些条件下完成当前推导。

这种处理有一个重要的逻辑边界。假设证明 A 时借用了 B，证明 B 时又依赖 A，那么即使两个局部检查分别通过，整体证明仍然存在循环依赖。因此，Checkpoint 的成绩只能反映条件性推导的完成程度，主定理必须在移除未经证明的中间假设后，再接受独立检查。

一个案例很能说明这种区别：Kimi K3 在某次尝试中完成了 7 个中间 Checkpoint，覆盖程度达到 87.5%，却没有完成主定理所需的最终推导。系统保留了局部成绩，同时拒绝将其认定为完整证明。

结合三种指导条件，还能进一步看到模型能力的差异。Kimi K3 在 Bare、Ladder 和 Guided 模式下分别至少完成 3、4、7 道不同定理，DeepSeek V4.1 Flash 0910 则分别完成 0、2、6 道。

提供中间引理与证明思路后，模型的完成数量明显增加，说明困难往往集中在关键引理的发现，以及如何将分散的推导组织成完整证明。

另外，Checkpoint 只是一种辅助分析方式。如果模型绕过预设的中间引理，直接构造出完整有效的主定理证明，系统同样能够接受。这为 Agent 保留了自主寻找证明路线的空间。

研究证书机制在 Solver 中采用不同实现。模型需要提交可重复运行的程序，检查器重新判断输出是否合法，并计算实际目标值。

以 IWLS 2023 逻辑综合任务为例，GPT-6 Astra 在 100 个实例中均生成了有效电路，其中 22 个优于公开参考电路，31 个达到参考水平，另外 47 个使用了更多 AND 门。

为了避免不同实例的数值尺度影响整体评价，系统还引入相对于 Kimi K3 多次运行结果的标准化评分，使有效性与优化质量能够分别衡量。数学构造轨道也采取类似处理，先检查对象是否满足结构约束，再比较它取得的数学参数。

当研究目标进一步扩展到开放猜想时，仅靠局部覆盖或数值改进已经不足以判断结论是否成立。模型需要找到一条完整的数学证明路线，并将其中复杂的结构分析转化成可以逐步核验的证据。

GPT-6 Astra 在 Alon–Jaeger–Tarsi 猜想上的研究，正好展示了这个过程。

04

从 8 维到 9 维

Alon–Jaeger–Tarsi 猜想研究有限域上的可逆矩阵。简单理解，给定一个可逆矩阵，研究者希望找到一个所有坐标均不为零的向量，并且经过矩阵变换后，新向量的所有坐标仍然不为零。

此前相关研究已经覆盖五元有限域中不超过 8 维的情形，Astra 将这一范围推进到了 9 维。随着维度增加，需要考虑的矩阵与向量组合迅速膨胀，直接枚举难以完成证明，因此它采用了另一条数学路线。

证明首先假设存在一个不满足猜想的 9 维矩阵，再利用低维情形已经成立的结论，限制这个反例必须满足的条件。接下来，Astra 不再逐个分析矩阵元素，而是转向研究向量经过矩阵变换前后的非零坐标数量。

它构造了两组 10×10 的非负整数数组，分别描述原矩阵和转置矩阵作用下，不同坐标数量之间的对应关系。矩阵可逆性限制了数组的行列总数，有限傅里叶恒等式则建立了两组数组之间的联系。结合反例的结构性质，还可以推导出部分计数必须为零。

这些条件将原本复杂的矩阵问题逐渐转化成整数约束，但仍然需要进一步缩小检查范围。

Astra 随后分析矩阵中两个列向量的坐标关系，将它们按照零元素分布及非零元素之间的消去比例划分为 7 种类别。由于矩阵维度为 9，各类别的数量之和必须为 9，因此可能出现的类别计数组合只有 5005 种。

这个步骤完成了关键的规模压缩。系统无须枚举全部 9 维可逆矩阵，只需要检查这些有限类别组合对应的数学约束。

在此基础上，Astra 将相同的结构分析应用于原矩阵、逆矩阵、转置矩阵及其逆矩阵，得到四组额外的非负约束。结合此前构造的两组计数数组，最终形成一个包含 204 个非负变量的整数线性系统。

此时，证明已经转化为判断这些整数约束能否同时成立。Astra 从原始的 197 条方程中，选取 143 条具有非零乘子的方程，按照特定整数系数进行组合，得到一个无法成立的关系：204 个变量的系数全部非负，等式右侧却是负数。

由于变量本身也必须非负，这样的关系必然产生矛盾，因此假设中的 9 维反例无法存在。

这份证书将复杂的矩阵推导压缩成有限的整数计算。独立核验确认，组合后的 204 个系数中，93 个为正，111 个为零。整个证明还被整理成包含 71 个 Lean 模块的项目，在独立环境中重新编译，并完成公理依赖检查。

从极小反例出发，通过坐标计数建立约束，再利用有限类别分析缩小问题规模，最终以整数矛盾排除反例，这条证明路线体现了 AI 将数学结构分析与计算工具结合的能力。

不过，Astra 完成的是五元有限域上的 9 维特殊情形，完整的 Alon–Jaeger–Tarsi 猜想仍未解决。TCSExam 的其他开放猜想实验同样表明，当前模型距离独立解决一般性难题仍有差距。

部分被接受的 Ryser 和 MIRUP 反证来自对 OpenAI 已公开成果的检索与适配，其余 28 项开放猜想没有得到完整解决方案。

05

从局部发现走向长期研究

TCSExam 的实验显示，AI 已经能够完成部分研究级证明，并在算法优化与数学构造中取得可核验的进展，但独立寻找关键引理、规划长程证明，以及将特殊结论推广到一般情形，仍然存在明显困难。

研究证书机制为未来的科研 Agent 提供了一种可迭代的工作基础。模型可以利用 Solver 搜索候选结构，通过形式化工具检查数学性质，再根据验证失败的位置修改证明策略，将已经成立的中间结果用于后续研究。

这次实验最值得记住的，不是“630比629多1”，也不是“9维比8维多1维”，而是：AI已经能在部分研究级任务上产出“机器可核验”的新结果，虽然离“自己提出关键引理、自己规划长程证明”还有明显距离。

对Kimi和月之暗面来说，这是一次“AI for Science”的能力展示；对数学界来说，这是一套可以复用的评测框架；对普通读者来说，这可能是一个信号：AI做科研，正在从“帮人查文献、写代码”，走向“帮人证定理、找反例”。

雷峰网原创文章，未经授权禁止转载。详情见转载须知。