姚期智与杨植麟联合发布 TCSExam 基准，Kimi K3 刷新图论纪录
Andrew Yao and Yang Zhilin Co-Author TCSExam as Kimi K3 Adds an Edge to a Graph Record
姚期智和杨植麟一起做了个理论计算机科学基准，用 Lean 4 自动判分，Kimi K3 还顺手刷了个 124 顶点 630 边的图论纪录。做形式化验证或模型评测的人可以看看它的出题思路。
Andrew Yao（姚期智）与 Yang Zhilin（杨植麟）等人共同署名推出 TCSExam，一个面向理论计算机科学的 AI 研究能力基准。该基准的核心机制是用 Lean 4 定理证明器和程序检查器对模型的解答做自动化验证，避免传统数学基准中人工判卷或答案泄漏的问题。
首批结果中，Kimi K3 在图论任务上给出了一个 124 个顶点、630 条边的图构造，刷新了该项纪录。这类极值图构造问题需要模型先提出候选结构，再通过程序枚举与证明确认其正确性，对推理与验证能力都是硬性考验。
TCSExam 的出现把 AI 数学能力评测从竞赛题推向了理论计算机科学这个更细分的领域，Lean 4 可验证评分的思路与近期的 FormEval、MiniF2F 等形式化基准方向一致。对研究团队而言，署名阵容（清华大学与月之暗面背景）也显示出产学合作正直接进入评测建设环节。
Andrew Yao and Yang Zhilin Co-Author TCSExam as Kimi K3 Adds an Edge to a Graph Record
TCSExam, co-authored by Andrew Yao and Yang Zhilin, checks AI research in theoretical CS with Lean 4 and program checkers. Kimi K3 found a 124-vertex graph with a record 630 edges.
本条情报归属 AITOP「论文」核心栏目，重点聚焦中国 AI 产业与国产大模型生态。在跨区域产业观察坐标中，该动态直接关联「中美大模型技术代差与商业化对照」「AI 开发者工具链、Coding Agent 与工程化实践」研究主线，反映出当前技术演进与商业落地的最新风向。涉及核心实体与技术议题包括：TCSExam、Kimi K3、Lean 4、推理模型，读者可通过下方标签进入对应专题页查阅历史脉络与关联对比。
信源核验说明：本文原始信息发布自一手权威信源「pandaily」（Tier-1 一手发布），具备高确定性参考价值。
