图灵奖得主、清华大学交叉信息研究院院长姚期智与月之暗面创始人杨植麟等人联合署名的一项研究，提出了面向理论计算机科学的AI评测框架TCSExam。该研究同时披露，Kimi K3在124个节点的图构造任务中构造出630条边的图并通过程序验证，超过此前629条边的参考纪录。
这项任务的约束条件为：在124个节点间连线，不得出现三角形，也不得出现四边形。组合数学领域此前认为629条边已接近极限。研究团队指出，每增加一条边都需要在全部节点之间重新完成结构重构，因此这一条边的增量被视为AI首次在极值构造类研究级任务上推进人类参考纪录。该成果的意义不仅在于数值本身，更在于研究团队试图建立一套可独立验证的标准，用以区分模型是凭借搜索运气命中结果，还是在逻辑上完成了构造。
TCSExam包含100项理论计算机科学科研任务，划分为四条轨道：定理证明20项，要求模型提交Lean 4形式化证明；Solver工程30项，要求开发可重复运行的算法程序，并在独立测试实例与统一资源限制下评测；数学构造20项，考察模型能否生成满足严格约束的图、纠错码等对象；开放猜想30项，允许模型从证明成立或寻找反例两个方向展开研究。
为防止局部进展被误判为完整成果，该框架设置了多层验证机制。定理证明由Lean内核依据形式逻辑规则检查推导，并审计证明依赖，排除未完成占位符与未经允许的额外公理。针对研究级定理需要多个中间引理的特点，框架引入Checkpoint机制，将复杂证明拆分为多个中间目标，验证时暂时将其余Checkpoint命题作为假设。研究团队同时明确了该机制的逻辑边界：若证明A借用B、证明B又依赖A，则局部检查通过不代表整体成立，主定理必须在移除未经证明的中间假设后接受独立检查。
实验数据显示，GPT-6 Astra完成了20项研究级定理中的14项，并将一个有限域矩阵猜想在特定条件下的已知证明范围从8维推进至9维，其证明将矩阵问题压缩为整数约束，最终以143条方程构造出可核验的矛盾证书。Kimi K3在Bare、Ladder、Guided三种指导模式下分别至少完成3、4、7道不同定理，DeepSeek V4.1 Flash 0910则分别完成0、2、6道。研究团队指出，提供中间引理与证明思路后模型完成数量明显增加，说明困难主要集中在关键引理的发现以及将分散推导组织为完整证明的过程。
该研究由理论计算机科学家与大模型团队共同完成，其价值在于把AI科研能力转化为可独立验证的研究成果，为评估AI参与真实科研提供了一条可操作的技术路径。随着大模型在数学与算法任务上的能力持续提升，如何建立兼顾严谨性与可比性的评测标准，将成为AI for Science领域的基础设施议题。
该文观点仅代表作者本人，企服科学平台仅提供信息存储空间服务。
