TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science

一句话概括

TCSAlgBench 是一个面向研究级理论计算机科学（TCS）的自动证明基准，从 138 篇 STOC 与 COLT 2026 论文中提炼出 398 个定理级挑战，用「证明者—验证者」讨论与多种智能体工作流来测量大模型能否给出人类可审查的算法正确性论证，结果显示当前最强配置的验证者接受覆盖率也只有约四分之一。

问题背景

大模型在竞赛数学上表现亮眼，但竞赛题有标准答案、有固定评分，而研究级推理没有。真正的科研推理发生在开放问题、未定结论和需要判断「什么才算一个证明」的语境里，很难用静态题库系统评估。

理论计算机科学（TCS）恰好提供了一个折中地带。它一方面关心算法设计，另一方面要求显式的保证：时间复杂度、近似比、竞争比、下界。也就是说，一个 TCS 结论必须能被写成「在某某计算假设下，达到某某定量保证」的形式，论证过程可以被同行逐步检查。这让它成为评估模型「能否为计算改进提供可审查理由」的理想试验场。

但已有的数学基准大多停留在竞赛题或本科习题层面，缺少来自最新研究论文、保留原始假设与定量保证、并且能持续更新的评测集。TCSAlgBench 想填补的正是这个空档。

方法要点

基准的构建方式是本文最值得关注的部分。作者从 138 篇 STOC 和 COLT 2026 论文中提取了 398 个定理级挑战。关键在于「专家设计的规则」：这些规则为每道题补全论文特定的上下文，保留原有的计算假设和定量保证，同时在「发现算法本身就是任务的一部分」时，刻意隐去构造。换句话说，题目不会把答案里的算法直接送给模型，而是要求模型自己找到构造或证明。

每道任务中，证明系统会拿到定理陈述，并可以访问被引用的先前工作。这一点很贴近真实科研：你不是从零开始，而是站在文献之上。

评测流程支持「新鲜、带版本号的挑战批次」，也就是说，随着新论文发布，可以持续生成新的题目批次，避免基准被训练数据污染而迅速饱和。

实验部分评估了来自四个模型家族的十种模型配置，比较了两种交互形态：直接推理，以及证明者—验证者讨论。此外还单独比较了四种智能体工作流，并且是在「匹配模型调用机会」的条件下对比，尽量控制算力差异带来的干扰。所有评估都使用完整基准，而非子集。

关键结论（仅基于摘要可合理推断的部分；不确定处标明「摘要未给出」）

在模型对比中，GPT-5.6 Sol max 在 10 轮讨论后取得最高的五次运行验证者接受覆盖率，为 23.6%。讨论和重复采样都能提升覆盖率。

在另一组使用 GPT-5.5 xhigh 的智能体对比中，任务分解比讨论更有效，而带规划的智能体方式取得最高的五次运行验证者接受覆盖率，为 25.4%。

由此可以合理推断：当前模型在研究级 TCS 证明上仍处于较低水平，即便最好的配置也只覆盖约四分之一的任务；交互式讨论、重复采样和任务分解这些「推理时技巧」确实带来增益，但增益有限，尚未把问题解决。

需要标明「摘要未给出」的信息包括：各模型配置的完整排名与具体分数、直接推理与讨论各自的绝对数值、四种智能体工作流的逐项结果、验证者接受的具体判定标准、任务按子领域或难度的分布、以及错误类型分析。这些都需要查阅正文才能确认。

读后思考 / 适用场景

这个基准的价值不只在「排名」，更在于它把评测对象从「答案对不对」转向「论证能不能被检查」。验证者接受覆盖率这个指标本身值得玩味：它衡量的是模型产出的证明能否通过一个验证环节，而不是与人类证明逐字比对。这更接近科研评审的实际形态。

适用场景上，TCSAlgBench 适合用来追踪模型在算法设计与下界论证上的进展，也适合研究「什么样的智能体工作流能支持长链条证明」。对于做 AI for Math、自动定理证明、以及 LLM 推理评测的研究者，它提供了一个可刷新、可版本化的测试床。对理论 CS 研究者而言，它也可能成为检验「模型能否辅助我检查一个引理」的实用工具。

局限与开放问题

第一，覆盖率绝对值偏低，23.6% 和 25.4% 意味着大部分任务无人通过，基准目前更像「难度天花板探测」而非「能力区分度工具」，是否会在短期内饱和或长期停滞，需要持续观察。

第二，验证者接受是否等同于证明正确，摘要未给出验证机制细节。如果验证者本身也是模型，那么「接受」可能包含系统性偏差，这是自动证明评测的共性难题。

第三，题目来自 STOC 和 COLT 2026，时间新是优点，但也意味着这些论文可能很快进入训练数据，基准的「新鲜度」需要靠版本化批次来维持，长期维护成本不低。

第四，隐去构造、保留假设的设计很巧妙，但如何界定「发现算法是任务的一部分」可能存在主观性，不同任务之间的难度可比性摘要未给出。

开放问题包括：讨论轮数增加是否持续带来增益，还是很快进入平台期；任务分解为何优于讨论，是分解降低了单步难度，还是讨论引入了噪声；以及当模型规模或推理预算继续增长时，这个基准的通过率会以什么斜率上升。