姚期智团队联合杨植麟发布TCSExam：大模型定理证明成功率最高70%

11月9日，澎湃新闻获悉，图灵奖得主、中国科学院院士、清华大学交叉信息研究院院长姚期智团队，联合月之暗面（Kimi）创始人杨植麟等发表署名论文《TCSEXAM：在TCS研究的全范围内评估前沿大型语言模型》。论文推出TCSExam统一评测，称首次把理论计算机科学研究的完整链条纳入评测。

TCSExam设置四类考题，每类都有机器验算，覆盖九个前沿大模型：定理证明要求用Lean 4写出严格证明，由Lean内核逐行验算；求解器工程要求写出可复用的通用解题程序；构造要求提交数学对象及证明其满足要求的“证书”；开放猜想则要求对长期未解难题给出完整证明或反证。

定理证明类中，GPT-6 Astra在“裸考”条件下只给主定理、不给中间引理，20道题完整证明14道，成功率70%；Kimi K3.1 Pro以38.3%位居第二，其余多个模型只有个位数甚至零成功率。补充中间引理和证明思路后，Kimi K3解出的定理数从3道增至7道，DeepSeek V4.1 Flash从0道增至6道。

构造类中，Kimi K3造出124个顶点、630条边且无三角形和四边形的图，超过论文引用的629条边参考记录；其量子纠错码把最小距离从5提升到6。GPT-6 Astra证明长度22、最小距离10的二进制编码最多只能有82个码字，改进此前发表的84。论文提醒，这些超纪录需独立核验，评分函数会放大或压缩数值差异，因此同时报告原始数学参数。

开放猜想类中，30个长期未解猜想仅6次提交被接受，且全部来自AI通过网络检索到OpenAI已公开发表的Ryser和MIRUP反例，再改写成考试要求的Lean证明，其余28个没有完整解决。论文还报告，GPT-6 Astra独立证明Alon-Jaeger-Tarsi猜想在一个有限数域上对所有不超过9维的情况成立，把已知范围从不超过8维推进一步，并经过Lean独立验证。论文推断，前沿AI已在研究级定理证明、构造优化和求解器工程上取得实质成果，但在真正解决开放猜想上仍有待加强。