姚期智与杨植麟联合发布 TCSExam 基准，Kimi K3 刷新图论纪录

Andrew Yao（姚期智）与 Yang Zhilin（杨植麟）等人共同署名推出 TCSExam，一个面向理论计算机科学的 AI 研究能力基准。该基准的核心机制是用 Lean 4 定理证明器和程序检查器对模型的解答做自动化验证，避免传统数学基准中人工判卷或答案泄漏的问题。 首批结果中，Kimi K3 在图论任务上给出了一个 124 个顶点、630 条边的图构造，刷新了该项纪录。这类极值图构造问题需要模型先提出候选结构，再通过程序枚举与证明确认其正确性，对推理与验证能力都是硬性考验。 TCSExam 的出现把 AI 数学能力评测从竞赛题推向了理论计算机科学这个更细分的领域，Lean 4 可验证评分的思路与近期的 FormEval、MiniF2F 等形式化基准方向一致。对研究团队而言，署名阵容（清华大学与月之暗面背景）也显示出产学合作正直接进入评测建设环节。