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

cs.AISep 28, 2026

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

Authors: Chutong Yang, Xiyuan Zhang, Yu Huang, Boran Han, Soonho Kong, Shuai Zhang, Vihang Prakash Patil, Zhen Han, +2 more

Organizations: Department of Computer Science, The University of Texas at Austin · Amazon · Department of Statistics and Data Science, The Wharton School, University of Pennsylvania

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.

Figures & tables

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

Topic	Retained	Total
Algorithmic fairness	17	30
Differential privacy	11	33
Learning theory	61	101
Optimization	25	52
Sampling	22	38
Other	85	144

Appendix

Table 1: Candidate Lean-statement retention by topic after compilation and automated semantic filtering. The rows follow the topic order used in Table 4 . Retention is a construction diagnostic, not expert-validated formalization accuracy.

Benchmark	Metric	GPT-5.5 xhigh	Opus 4.8 max
AIME 2026	Final-answer accuracy	100.00	100.00
HMMT February 2026	Final-answer accuracy	98.48	95.45
Apex	Final-answer accuracy	80.21	81.25
Apex Shortlist	Final-answer accuracy	98.40	90.43
ArXivMath June 2026	Final-answer accuracy	83.63	69.97
TCSAlgBench	Five-run proof coverage	18.1	4.5

Appendix

Table 2: Published MathArena results and TCSAlgBench five-run coverage with 10-round discussion, in percent. Metrics and evaluation protocols differ.

Configuration	Seed 1 acceptance	10-run coverage	Avg. input tokens	Avg. output tokens
GPT-5.6 Sol max	23 (5.8%)	55 (13.8%)	17K	19K
GPT-5.6 Sol xhigh	19 (4.8%)	43 (10.8%)	17K	16K
GPT-5.6 Sol high	19 (4.8%)	41 (10.3%)	16K	10K
GPT-5.5 xhigh	13 (3.3%)	28 (7.0%)	15K	17K
GPT-5.5 high	8 (2.0%)	21 (5.3%)	16K	16K
Opus 4.8 max	3 (0.8%)	7 (1.8%)	20K	9K

Appendix

Table 3: Direct-inference results for Figure 5 (a) on all 398 challenges, using three-voter majority voting. Entries are accepted-challenge counts, with percentages in parentheses. Seed 1 reports one run; 10-run coverage counts challenges accepted in any of ten independently seeded runs. Input and output tokens are averaged per prover call; K denotes thousands.

Panel A: First run (seed 1; $N=398$ )
Configuration	AF (30)	DP (33)	LT (101)	Opt. (52)	Samp. (38)	Other (144)	All (398)
Opus 4.8 high	3	0	2	1	1	1	8
Opus 4.8 xhigh	4	0	2	1	2	1	10
Opus 4.8 max	3	0	2	1	2	1	9
GPT-5.5 high	9	1	9	3	6	14	42
GPT-5.5 xhigh	8	1	12	5	6	13	45

Appendix

Table 4: Verifier-accepted proofs by topic on all 398 TCSAlgBench challenges after 10-round discussion. Panel A reports seed 1, and Panel B reports five-run coverage. AF denotes algorithmic fairness; DP, LT, Opt., and Samp. abbreviate differential privacy, learning theory, optimization, and sampling, respectively. Parenthesized column-header values give category totals.

Configuration	Three-voter majority	Opus 4.8 verifier	$\Delta$
Opus 4.8 high	14	14	0
Opus 4.8 xhigh	15	16	+1
Opus 4.8 max	18	18	0
GPT-5.5 high	66	60	-6
GPT-5.5 xhigh	72	68	-4
GPT-5.6 Sol high	79	77	-2

Appendix

Table 5: Five-run coverage for the eight model configurations evaluated under both the primary three-voter majority rule and an alternative Opus 4.8 verifier, using the same generated proofs.

\Delta

is Opus-verifier coverage minus majority-vote coverage.

Panel A: First run (seed 1; $N=398$ )
Models	Cutoff	Pre-cutoff	Post-cutoff	All
Opus 4.8 high	2026-01-01	3/201 (1.5%)	5/197 (2.5%)	8/398 (2.0%)
Opus 4.8 xhigh	2026-01-01	3/201 (1.5%)	7/197 (3.6%)	10/398 (2.5%)
Opus 4.8 max	2026-01-01	2/201 (1.0%)	7/197 (3.6%)	9/398 (2.3%)
GPT-5.5 high	2025-12-01	19/188 (10.1%)	23/210 (11.0%)	42/398 (10.6%)
GPT-5.5 xhigh	2025-12-01	24/188 (12.8%)	21/210 (10.0%)	45/398 (11.3%)

Appendix

Table 6: Verifier-accepted proofs before and after the assumed model-family knowledge cutoff on all 398 challenges. Panel A reports seed 1, and Panel B reports five-run coverage. Percentages use the corresponding pre- or post-cutoff column total; percentages in the All column use all 398 challenges.

Panel A: Opus 4.8 and GPT-5.5
	Opus 4.8: xhigh vs. max			GPT-5.5: high vs. xhigh
	Overlap	xhigh only	max only	Overlap	high only	xhigh only
Before cutoff	5	1	2	29	2	9
After cutoff	9	0	2	31	4	3
Total	14	1	4	60	6	12
Panel B: GPT-5.6 Sol and Fable 5

Appendix

Table 7: Complementarity of five-run verifier-accepted coverage on all 398 challenges, partitioned by the model-family knowledge cutoff. Overlap counts challenges accepted under both effort settings, while the setting-only columns count challenges accepted uniquely under one setting. For Fable 5, the high/xhigh union contains 32 challenges before the cutoff, 37 after it, and 69 overall.

Workflow	Seed 1	Five-run coverage	Avg. input tokens	Avg. output tokens
Decomposition with MCTS search	77 (19.3%)	96 (24.1%)	27.4M	3.9M
Discussion, no decomposition	60 (15.1%)	84 (21.1%)	12.1M	1.0M
Discussion, root-only decomposition	73 (18.3%)	93 (23.4%)	25.6M	3.9M
Discussion, agentic planning	72 (18.1%)	101 (25.4%)	60.4M	9.0M

Appendix

Table 8: Call-matched agent-design comparison using GPT-5.5 xhigh and the same external verifier; Appendix C details the budgets. Acceptance counts use all 398 challenges, with rates in parentheses. Seed 1 reports one run; five-run coverage counts challenges accepted in any of five independently seeded runs. Tokens are averaged per challenge–seed run over 10 randomly selected challenges and five independent seeds; M denotes millions.

Model configuration	Acceptance (%) $\uparrow$	RMS-CE (%) $\downarrow$
GPT-5.6 Sol max	18.1	10.8
GPT-5.6 Sol xhigh	15.6	4.3
GPT-5.6 Sol high	12.1	11.7
GPT-5.5 xhigh	10.8	19.1
GPT-5.5 high	10.1	17.3
Claude Opus 4.8 xhigh	2.3	2.0

Appendix

Table 9: Verifier acceptance and RMS calibration error (RMS-CE), in percent, on all 398 challenges. These runs are separate from the main model comparison. Both metrics use the same proof outputs, with confidence elicited during proof generation before external verification.

Explore similar work

Aug 10, 2026cs.CL

TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability

We introduce TCS-Bench, a benchmark for evaluating Large Language Models (LLMs) on research-level Theoretical Computer Science (TCS) proof generation. TCS-Bench consists of theorem-proving tasks from papers published at top theoretical computer science venues (STOC, FOCS, and SODA). Each task provides the necessary context to derive a self-contained proof for a target result. We evaluate state-of-the-art models on this benchmark. We verify the correctness of generated proofs via a verification agent, and further benchmark the verifier against human-expert proof judgements on a set of target statements and generated proofs pairs. Our reference verifier achieves over 90% accuracy on the expert labeled set.

Vincent Cohen-Addad, Dimitris Paparas, Ernest van Wijland +13

†Google 1 · ‡CNRS, IRIF, Université Paris-Cité · §Princeton University, Department of Computer Science +2

Large Language Model Benchmarks Data Generation

Ask PDF

Aug 20, 2026cs.CL

FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models

Large language models (LLMs) have shown growing potential for automated theoretical computer science (TCS) research, yet existing benchmarks remain far from realistic research settings. We introduce \ourbenchmark, an expert-validated benchmark for evaluating LLMs on frontier, end-to-end TCS research. \ourbenchmark contains

143

instances drawn from papers accepted to STOC, FOCS, SODA, and COLT in 2025-2026, preserving paper-specific definitions, assumptions, and proof dependencies, with expert-verified Lean formalizations and proofs. Evaluations of leading LLMs reveal that current models remain far from reliably completing the full research pipeline. In particular, autoformalization is the sharpest bottleneck: the best model achieves only

11.5

on translating natural-language claims into formal theorem statements, compared with

28.6

Pass@8 when proving human-provided formal statements. Building on \ourbenchmark, we further develop an automated TCS research framework that generates, formalizes, filters, and proves new claims. Of

64

generated claims, only

6

ultimately pass expert evaluation and proof verification, indicating that beyond formalization, limited research taste remains another major barrier to autonomous TCS research.

Dingzirui Wang, Xuanliang Zhang, Keyan Xu +2

Harbin Institute of Technology

Large Language Model Benchmarks Formalization

Ask PDF

Jun 8, 2026cs.AI

TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics

LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments. We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings. The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms: a plain main version containing one target theorem per instance, and a premised version that expands each theorem into a structured family of related proving tasks consisting of the main theorem together with automatically extracted supporting subtheorems. This design enables evaluation of not only whether the final theorem was proved from scratch, but also of partial progress through the internal proof structure of a theorem. Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models. To provide a comprehensive evaluation, we introduce theorem-level coverage and token-efficiency metrics that expose qualitative differences in proof behavior. The results show that current provers remain strongly biased toward easy subtheorems and often solve theorems through long and inefficient tactic traces rather than compact proof plans. TheoremBench therefore provides a more fine-grained view of formal reasoning ability and highlights the importance of structural benchmark design for evaluating Lean4 theorem provers.

QuocViet Pham, Elvir Karimov, Andrey Galichin +1

Skolkovo Institute of Science and Technology · HSE University · Sberbank +1

Theorem Proving

Ask PDF