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

大语言模型在竞赛数学中表现强劲，但其研究水平的推理仍然难以系统评估。理论计算机科学 (TCS) 将算法设计与明确的保证和基本限制联系起来，为评估模型是否可以通过人类可以检查的论据来证明计算改进的合理性提供了一个环境。我们引入了 TCSAlgBench，这是一个用于自然语言证明发现的基准和可重用管道，包含来自 138 篇 STOC 和 COLT 2026 论文的 398 个定理级挑战。专家设计的规则完成了特定于论文的上下文，保留计算假设和定量保证，并在发现算法是任务的一部分时保留结构。对于每项任务，证明系统都会收到定理陈述并访问引用的先前工作。该管道支持来自新发布论文的新的、版本化的挑战批次。我们在直接推理和证明者-验证者讨论下评估来自四个系列的十种模型配置，并在匹配的模型调用机会下比较四个Agent工作流程。所有评估均使用完整基准。在模型比较中，GPT-5.6 Sol max 经过 10 轮讨论后，达到了 23.6% 的五轮验证者接受的最高覆盖率。讨论和重复抽样提高了覆盖率。在使用 GPT-5.5 xhigh 的单独Agent比较中，分解提高了讨论的覆盖率，agentic 规划实现了五次运行验证者接受的最高覆盖率（25.4%）。 TCSAlgBench 提供了一个可更新的测试平台，用于衡量模型推理的进展并研究Agent工作流程如何支持研究级证明发现。