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

What it claims

The useful detail beyond the headline numbers is how the challenges are built and what the prover can see. The authors developed rules that turn a theorem extracted from a paper into a fair proof task. These rules keep the paper's computational model, its restrictions on what information an algorithm can access and in what order it acts, its assumptions and its quantitative bounds. They also hide the solution. When the task is to design an algorithm, a claim like "Algorithm 1 solves P in T(n)" becomes "there exists an A that solves P in T(n)". Separately, the paper ranks agent workflows differently depending on the metric: MCTS is best on seed-1 acceptance, while agentic planning is best on five-run coverage.

How it works

Opus 4.8 (high reasoning mode) runs the construction pipeline:

flowchart LR
  A[arXiv TeX + cited work] --> B[Proof graph]
  B --> C[Pick 1-4 main theorems]
  C --> D[Challenge draft]
  D --> E{LLM self-containment check}
  E -- missing context --> F[Repair rules: notation, assumptions, existence rewrite]
  F --> D
  E -- complete --> G[Released challenge]

• Paper selection. A model-assisted screen keeps only papers whose main results are upper or lower bounds on sample or runtime complexity.
• Context. Definitions are quoted from the source paper, with notation normalized. Added standard-background definitions are explicitly labeled.
• Withheld material. Lemmas from the source paper are removed, not supplied.
• Evaluation sandbox. Proving runs in an offline sandbox. The prover can read cited prior work through "local prover graphs" and TeX files. The source paper, its construction graph and anything containing the target proof are excluded.
• Output. The prover returns one prose proof, which an external LLM verifier scores.
• Verifier check. Before judging a proof, the verifier checks that the cited statements match their sources. TCS-BENCH instead gives its judge a reference proof.

The four agent workflows share the same backbone model, input, tools, number of model-call opportunities and per-call generation limit:

1. Role-based discussion: a prover, verifier and decider work over a shared, bounded history.
2. Root-only decomposition: the root theorem is split into one level of subgoals, retrying with new splits.
3. MCTS: Monte Carlo tree search over a full AND–OR tree of subgoals.
4. Agentic planning: the agent plans a lemma dependency graph (DAG) and revises it from critic feedback.

Realized input and output tokens are reported separately for each workflow.

Evidence

• Coverage. The best five-run coverage is 23.6%, from GPT-5.6 Sol max with 10-round discussion. In the agent comparison on GPT-5.5 xhigh, agentic planning reaches 25.4%. Decomposition beats discussion.
• Discussion and sampling. Both more discussion rounds and repeated sampling raise coverage.
• Gap to math benchmarks. Figure 1 compares strong published final-answer accuracy on AIME, HMMT, Apex and ArXivMath with TCSAlgBench. Its labels appear to give TCSAlgBench scores of 18.1% for GPT-5.5 xhigh and 4.5% for Opus 4.8 max, after five runs of 10-round discussion.
• Statement fidelity. The rules were developed on 21 challenges. Reviewers then manually checked 61 statements: the 21 development ones plus 40 others. All 40 held-out statements were judged faithful to the source and self-contained.
• Verifier sensitivity. Identical submissions are re-scored with Opus 4.8 to see whether conclusions change with the verifier. The excerpt does not include those results.

How to use it

• Licensing. The public release includes only challenges from arXiv versions licensed CC BY 4.0 or CC0.
• Provenance. Each challenge records its source paper and version.
• Fresh batches. The pipeline can produce new, versioned batches from papers published after a model's knowledge cutoff, with controllable size and topic mix.
• Prompts. The pipeline prompts are in Appendix E.
• Lean statements. A supplementary set of 221 provisional Lean statements is included. They compile and passed automated semantic screening. They are not verified formalizations.
• Not stated. The excerpt gives no repository, install command or harness interface.

Limits

• Review coverage. Only 61 of the 398 statements were human-reviewed. The other 337 rely on the automated pipeline.
• Scoring. All scores come from an LLM verifier, not expert grading. The authors re-score with a second model precisely because verifier choice may matter.
• Scope. Tasks start after a human has already identified the problem and the relevant literature. Problem formulation and literature search are not tested.
• Topic coverage. Only complexity-bound results are included, from STOC and COLT 2026.
• Related benchmarks. TCS-BENCH (300 tasks from STOC, FOCS and SODA, graded by experts) and FormalTCS are close alternatives. The authors say the differences are in task inputs and pipeline design.
• Truncated excerpt. The fetched text ends partway through the evaluation protocol, so per-model tables, token costs and verifier-sensitivity outcomes are not covered here.