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
Sep 28, 2026 · v1
cs.CL
TL;DR
Supplies 221 provisional Lean 4 statements, autoformalized by a GPT-5.5 agent in a pinned Mathlib/CSLib environment, that pass compilation and semantic screening.
Abstract
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.
Problem
Research-level reasoning by LLMs is hard to evaluate systematically, because most benchmarks target competition mathematics or isolated problems. Theoretical computer science offers explicit algorithmic guarantees that can be checked through human-inspectable proofs.
Approach
TCSAlgBench contains 398 theorem-level challenges from 138 STOC and COLT 2026 papers. Expert-designed rules add paper-specific context and withhold constructions for algorithm-design tasks. Provers receive theorem statements plus cited prior work and must write natural-language proofs, which LLM verifiers judge. As a supplement, a GPT-5.5 agent autoformalizes challenge statements as Lean 4 Prop declarations against Mathlib/CSLib; declarations must compile without sorry, admit, or untrusted axioms.
Results
GPT-5.6 Sol max reaches 23.6% five-run verifier-accepted coverage after 10-round discussion. With GPT-5.5 xhigh, agentic planning reaches the highest coverage among workflows at 25.4%. 221 provisional Lean statements pass compilation and semantic screening.
| Workflow | Seed 1 | Five-run coverage |
|---|
| Decomposition with MCTS search | 77 (19.3%) | 96 (24.1%) |
| Discussion, no decomposition | 60 (15.1%) | 84 (21.1%) |
| Discussion, root-only decomposition | 73 (18.3%) | 93 (23.4%) |
| Discussion, agentic planning | 72 (18.1%) | 101 (25.4%) |
Agent workflow comparison with GPT-5.5 xhigh