姚期智与杨植麟联合发布 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.
This report is categorized under AITOP's "Papers" desk, focusing on China's AI industry and domestic foundation model ecosystem. Within our cross-regional analytical framework, it directly maps to US-China foundation model benchmarks and commercialization comparison and AI developer toolchains, coding agents, and engineering workflows. Key entities and technical topics under continuous tracking include TCSExam, Kimi K3, Lean 4, 推理模型.
Primary source verification: published directly by pandaily with first-party authority.
