TCSAlgBench：面向研究级理论计算机科学的自动化证明基准测试

大型语言模型在竞赛数学中表现强劲，但其研究级推理能力仍难以系统评估。理论计算机科学（TCS）将算法设计与明确保证和基本极限联系起来，为评估模型是否能够用人类可审查的论证来证明计算改进提供了一个场景。我们介绍 TCSAlgBench，这是一个用于自然语言证明发现的基准和可复用流水线，包含来自 138 篇 STOC 和 COLT 2026 论文的 398 个定理级挑战。专家设计的规则补全论文特定上下文，保留计算假设和定量保证，并在发现算法本身属于任务的一部分时隐藏构造。对于每个任务，证明器系统会获得定理陈述，并可访问被引用的先前工作。该流水线支持基于新发布论文生成全新的、带版本的挑战批次。我们在直接推理和证明器-验证器讨论两种设置下评估来自四个系列的十种模型配置，并在匹配的模型调用机会下比较四种智能体工作流。所有评估均使用完整基准。在模型比较中，GPT-5.6 Sol max 在 10 轮讨论后取得最高的五次运行验证器接受覆盖率，为 23.6%。讨论和重复采样提高了覆盖率。在使用 GPT-5.5 xhigh 的单独智能体比较中，分解相较于讨论提高了覆盖率，而智能体式规划取得最高的五次运行验证器接受覆盖率，为 25.4%。TCSAlgBench 提供了一个可刷新测试平台，用于衡量模型推理的进展，并研究智能体工作流如何支持研究级证明发现。