TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science
作者: Chutong Yang, Xiyuan Zhang, Yu Huang, Boran Han, Soonho Kong, Shuai Zhang, Vihang Prakash Patil, Zhen Han, Michael Bohlke-Schneider, Bernie Wang
分类: cs.AI, cs.CL
发布日期: 2026-09-28
💡 一句话要点
提出TCSAlgBench以评估自动证明在理论计算机科学中的应用
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动证明 理论计算机科学 大型语言模型 推理能力 基准评估 算法设计 自然语言处理
📋 核心要点
- 现有方法在评估大型语言模型的研究级推理能力时缺乏系统性，难以验证其计算改进的合理性。
- 论文提出TCSAlgBench基准，包含398个定理级挑战，旨在通过自然语言证明发现来评估模型的推理能力。
- 实验结果表明，GPT-5.6 Sol max在10轮讨论后实现了23.6%的验证器接受覆盖率，显示出讨论和重复采样对覆盖率的提升效果。
📝 摘要（中文）
大型语言模型在竞赛数学中表现出色，但在研究级推理的系统评估上仍然面临挑战。理论计算机科学（TCS）将算法设计与明确的保证和基本限制相连接，为评估模型是否能够通过人类可检查的论证来证明计算改进提供了背景。本文介绍了TCSAlgBench，一个用于自然语言证明发现的基准和可重用管道，包含来自138篇STOC和COLT 2026论文的398个定理级挑战。该基准通过专家设计的规则补充论文特定的上下文，保留计算假设和定量保证，并在发现算法时保留构造。我们评估了来自四个家族的十种模型配置，并比较了在匹配模型调用机会下的四种代理工作流。所有评估均使用完整基准，结果显示GPT-5.6 Sol max在10轮讨论后实现了23.6%的验证器接受覆盖率。
🔬 方法详解
问题定义：本文旨在解决如何系统性评估大型语言模型在研究级推理中的能力，现有方法缺乏有效的基准和评估框架。
核心思路：通过引入TCSAlgBench基准，提供一个包含定理级挑战的管道，允许模型在自然语言环境中进行证明发现，从而评估其推理能力。
技术框架：TCSAlgBench的整体架构包括定理陈述、引用的先前工作访问、专家设计的规则和挑战批次的版本控制，支持从新发布论文中获取新挑战。
关键创新：最重要的创新在于构建了一个可重用的基准，结合了专家设计的规则和动态更新的挑战，确保了评估的全面性和有效性。
关键设计：在模型评估中，采用了不同的模型配置和工作流设计，特别是讨论和分解策略的比较，显示出不同策略对验证器接受覆盖率的影响。
🖼️ 关键图片
📊 实验亮点
实验结果显示，GPT-5.6 Sol max在10轮讨论后实现了23.6%的验证器接受覆盖率，而在使用GPT-5.5 xhigh的代理比较中，分解策略的覆盖率超过了讨论策略，代理规划实现了25.4%的最高覆盖率，展示了不同策略的有效性。
🎯 应用场景
TCSAlgBench的研究成果可广泛应用于理论计算机科学的自动证明领域，帮助研究人员评估和改进大型语言模型的推理能力。其可重用的基准和动态更新的挑战将促进相关领域的研究进展，推动自动证明技术的发展。
📄 摘要（原文）
Large language models perform strongly on competition mathematics, but their research-level reasoning remains difficult to evaluate systematically. Theoretical computer science (TCS) connects algorithm design to explicit guarantees and fundamental limits, providing a setting for evaluating whether models can justify computational improvements with arguments humans can inspect. We introduce TCSAlgBench, a benchmark and reusable pipeline for natural-language proof discovery, comprising 398 theorem-level challenges from 138 STOC and COLT 2026 papers. Expert-designed rules complete paper-specific context, preserve computational assumptions and quantitative guarantees, and withhold constructions when discovering an algorithm is part of the task. For each task, prover systems receive theorem statements and access to cited prior work. The pipeline supports fresh, versioned challenge batches from newly released papers. We evaluate ten model configurations from four families under direct inference and prover-verifier discussion, and compare four agent workflows under matched model-call opportunities. All evaluations use the full benchmark. In the model comparison, GPT-5.6 Sol max achieves the highest five-run verifier-accepted coverage at 23.6% after 10-round discussion. Discussion and repeated sampling improve coverage. In the separate agent comparison using GPT-5.5 xhigh, decomposition improves coverage over discussion, and agentic planning achieves the highest five-run verifier-accepted coverage at 25.4%. TCSAlgBench provides a refreshable testbed for measuring progress in model reasoning and studying how agent workflows support research-level proof discovery.