TCSExam：大模型征战理论计算机科学的统一考场

大语言模型能否推进理论计算机科学（TCS）并解决其悬而未决的猜想？这个问题长期停留在哲学讨论层面，如今有了可量化的实验框架。新提出的 TCSExam 试图为前沿 LLM 在 TCS 全谱系研究中的能力提供统一评测基准，把定理证明、求解器工程、构造性工作与直接攻克开放猜想放在同一套标尺下衡量。

四条赛道，覆盖 TCS 研究全流程

据原始论文描述，TCSExam 的设计思路是覆盖 TCS 研究的完整链条，而非只考察单一能力。它包含四条并行赛道：定理证明、求解器工程、构造，以及直接尝试解决开放猜想。前三条对应具体的研究产出，第四条则瞄准长期未解的研究目标，考察模型能否在真正开放的问题上做出推进。

这种划分的意义在于区分"会做题"和"会研究"。定理证明和构造有明确的对错标准，而开放猜想的尝试即便没有完全解决，也可能产出可独立验证的特殊情形或界（bounds），这些中间成果本身就有学术价值。

理论计算机科学（TCS）是计算机科学的数学基础分支，研究计算的根本性限制与可能性，典型议题包括 P vs NP、算法下界、通信复杂度、密码学假设等。它与工程导向的系统研究不同，产出以定理、证明和渐近界为主，验证标准严格且往往需要形式化推理。正因如此，TCS 长期被视为最不适合用统计式语言模型直接攻克的领域之一——一个证明要么成立要么不成立，不存在"大致正确"。TCSExam 把 TCS 研究拆成定理证明、求解器工程、构造与开放猜想四条赛道，正是承认该领域既有纯形式化推理，也有需要实际运行算法求解器的工程侧面。

双重校验与两档基准

TCSExam 在评分机制上采用了硬性验证。TCSExam-Full 包含 100 个经专家审阅的任务，所有提交由 Lean 内核或可执行的任务检查器进行校验。这意味着模型的输出不能靠语言上的似是而非蒙混过关，必须通过形式化验证或实际运行检验。

为降低评测成本，团队还设计了 TCSExam-Lite：从中选取 20 个任务，每条赛道五个，在单次尝试预算不变的情况下将任务尝试数量减少 80%。

论文显示，Full 与 Lite 的排名在八个共有智能体上高度一致，Spearman 相关系数达到 0.93，这为 Lite 作为紧凑且有区分度的基准提供了统计支持。对于算力有限的研究者，Lite 提供了实用的替代方案。

Lean 是微软研究院主导开发的交互式定理证明器，同时是一门依赖类型理论编程语言。它的核心特性是"内核校验"：任何证明在被接受前，都必须由一小段可信的内核代码逐条检查推理步骤是否符合类型规则，因此模型的输出无法通过语言上的含糊其辞通过验证。Lean 社区已建立 mathlib 等大规模形式化数学库，使形式化验证从纯数学扩展到计算机科学定理成为可能。在 TCSExam 中，Lean 内核充当了定理证明赛道和部分构造任务的"硬裁判"，而求解器工程和可执行构造任务则由实际运行的任务检查器校验——前者保证逻辑正确性，后者保证算法行为符合预期，二者共同构成"双重校验"的客观性基础。

谁在领跑：八智能体上榜

研究团队在 Full 上评测了八个智能体，在 Lite 上评测了九个。TCSExam Index 综合四条赛道的成绩，GPT-6 Astra 以 71.9 分领跑 Full，Opus 5.5 以 72.3 分领跑 Lite。

比排名更值得关注的是评测过程中产生的实质产出。论文指出，这些评估带来了改进的求解器输出和数学构造，以及从开放猜想尝试中得到的、经过独立验证的特殊情形和界。也就是说，基准测试不只是给模型打分，还顺带产出了可作为研究素材的中间结果。

在基准评测中，Spearman 秩相关系数用于衡量两个排名之间的一致性，取值从 -1 到 1，越接近 1 表示两套评分给出的名次越吻合。TCSExam 报告 Full 与 Lite 的 Spearman ρ=0.93，意味着用仅含 20 个任务的 Lite 版本给智能体排序，与用 100 个任务的 Full 版本排序几乎一致。这一统计量之所以关键，是因为紧凑基准的风险在于任务抽样偏差可能扭曲排名；高秩相关说明 Lite 在保留区分度的同时大幅降低了评测成本，为算力有限的研究者提供了可信的替代方案。

框架开放，强调可复现

TCSExam 被定位为一个可扩展框架，论文提供了任务来源、Docker 构建配方和评估工具，供社区进行可复现的使用。这一点对基准类工作的长期价值至关重要——TCS 研究领域广泛，100 个任务的覆盖面必然有限，可扩展的任务接入机制让后续研究者能按同一规范补充新题。

这套基准改变了什么

TCSExam 的出现在于把"LLM 能否做研究"这个模糊问题拆解为可执行、可验证的多个子问题。Lean 内核校验和可执行检查器保证了评分的客观性，四条赛道的划分让能力画像更加立体，而 Lite 版本则在成本与区分度之间给出折中。

对关注 AI for Science 的研究者而言，这套框架的价值不仅在于当前榜单，更在于它提供了一套可以持续追加任务的评测协议。当模型能力继续演进时，同一套协议下的成绩变化将成为观察 LLM 在形式化数学与算法研究中真实进展的可靠窗口。