从定理证明到开放猜想：TCSExam 揭示大模型科研能力边界

近日，清华大学、Moonshot AI与上海期智研究院联合发布了 TCSExam 基准，用来评估大模型在理论计算机科学研究中的真实水平。测评结果显示，表现最好的 GPT-6 Astra 能证明七成研究级定理，在部分构造问题上甚至超过了已知最好结果，却没能完整解决任何一个公开猜想。这组成绩既不说明“AI 无所不能”，也不说明“AI 只是噱头”，而是把模型能力的边界呈现得相当清楚。

一、一把更严格的尺子过去，大模型的数学评测多依赖竞赛题或人工判分，常见两个问题：一是题目可能早已混进训练数据，高分未必代表真能推理；二是自然语言写成的证明难以客观判定，评审容易被似是而非的“幻觉证明”误导。TCSExam 的 100 道任务由专家评审，覆盖定理证明、求解器工程、构造纪录和公开猜想四类工作，大致对应理论研究者从证明、实现到探索的完整流程。更关键的是，所有结果都要经过 Lean 形式化系统或程序检查器的自动验证，对就是对，错就是错，减少了“看起来像对的”错误答案蒙混过关的空间。

二、能力边界在哪里从结果看，模型的表现可以分为三个层次。第一层，复杂推理已经比较成熟。 在严格的形式化环境中证明研究级定理，需要很长的推理链条和对大量细节的准确处理。七成的成功率说明，模型已经能胜任这类有明确目标的高难度推理。第二层，在清晰目标下已能产出新成果。 构造类任务有明确的评分标准，模型可以通过大量搜索和反复验证逐步改进方案，最终给出比已知更好的结果。这说明 AI 在特定条件下已经具备一定的“发现”能力。第三层，开放性突破仍是空白。 公开猜想至今没有被解决，往往是因为现有方法本身就不够用，需要全新的概念和思路。在这一层，模型只能得到一些局部结论，离真正的突破还很远。简单来说，有方向、能打分的问题，AI 已经能做得很好；没有现成路径、需要开辟新理论的问题，仍然要靠人类。

三、被忽视的基础：稳定的网络TCSExam 也反映出大模型使用方式的变化：模型越来越多地以智能体的形式长时间运行，需要反复调用接口、检索资料、提交验证，一项任务往往包含几十甚至上百轮交互。在这种模式下，网络质量会直接影响效果。一次连接中断就可能让长任务前功尽弃，既浪费算力，也打断工作进程；延迟波动会在多轮交互中不断累积，拖慢整体效率；跨地区访问大模型服务时，线路不稳定或 IP 频繁变动还容易触发风控，导致请求失败。可以说，模型能力决定了 AI“能做什么”，而稳定、低延迟的网络决定了这些能力“能不能持续用好”。随着智能体任务越来越复杂，网络正在从配套条件变成生产力的一部分。

四、对行业的启示第一，可验证评测值得推广。 形式化验证让科研级能力也能被客观衡量，有助于减少刷榜和夸大宣传。第二，人机协作是现阶段的最优解。 把繁琐的证明、验证和搜索交给 AI，研究者专注于提出问题和设计方向，效率会明显提升。第三，开放问题是下一道门槛。 让模型在没有明确目标的情况下提出新概念、新方法，是 AI 从“科研助手”走向“科学家”的关键，可能需要在技术路线上有根本性的创新。

结语TCSExam 用严格的方式回答了“AI 现在走到了哪里”：它已经是优秀的执行者和探索者，但还不是开拓者。在模型能力持续进步的同时，网络、算力等基础设施的稳定性，也将决定这些能力能在多大程度上真正落地。