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

1 Introduction

• TCS proof discovery tests whether models can reason about algorithms, information access, and computational requirements using arguments humans can inspect and challenge.The motivation connects explicit assumptions, guarantees, and limits to evaluating proposed computational improvements.Source: §1 · p. 1
• TCSAlgBench contains 398 theorem-level challenges from 138 STOC and COLT 2026 papers and supports fresh, versioned batches from newly released work.Challenges span several TCS areas and provide local definitions, assumptions, notation, and necessary prior work.Source: §1 · p. 2
• Expert-designed rules preserve computational assumptions and quantitative guarantees while withholding named constructions when algorithm design is part of the task.The rules add needed definitions, remove source-paper lemmas, and were manually reviewed for fidelity and self-containment.Source: §1 · p. 2
• Across all 398 challenges, MCTS performs best on seed-1 acceptance, while agentic planning performs best on five-run coverage.The study compares ten model configurations and four workflows, with the workflow comparison controlling model-call opportunities.Source: §1 · p. 2

Mathematical and TCS benchmarks

• Mathematical evaluations range from exact-answer and difficult or fresh problems to research-level proofs, motivating systematic evaluation across these settings.The passage surveys benchmarks and reported advances including Navier–Stokes.Source: §2 · p. 2
• TCSAlgBench emphasizes theorem-level TCS proof discovery, TCS-specific context repairs, and cited prior work, while related benchmarks differ in task inputs and pipeline design.The comparison discusses TCS-BENCH (Cohen-Addad et al., 2026) and FormalTCS (Wang et al., 2026).Source: §2 · p. 3

Proof-agent designs

• Prior proof-agent work covers iterative generation and critique, sketch-based decomposition, AND–OR or value-guided search, and replanning over dependency structures.Examples include Feng et al. (2026a), Jiang et al. (2022), Lample et al. (2022), and An et al. (2026).Source: §2 · p. 3

LLM-based proof verification

• Proof-verification approaches include expert-compared LLM judging, reference solutions and rubrics, and premise–conclusion modules for error localization.TCS-BENCH supplies a reference proof (Cohen-Addad et al., 2026), whereas this paper checks cited statements against their sources.Source: §2 · p. 3

Autoformalization and formal proving

• Formalization benchmarks and tools include LeanDojo (Yang et al., 2023), miniF2F (Zheng et al., 2021), and PutnamBench (Tsoukalas et al., 2024), but compilation alone does not ensure statement fidelity.Model consensus is described as an imperfect, human-calibrated proxy (Zhang et al., 2026b).Source: §2 · p. 3

3 Benchmark Scope and Evaluation

• The benchmark targets upper- and lower-bound challenges about sample or runtime complexity, where proofs address achievable computational improvements or limits under explicit assumptions.Its 398 challenges come from 138 publicly available arXiv papers accepted to STOC and COLT 2026, spanning areas including privacy, learning, optimization, sampling, cryptography, graph theory, and coding theory.Source: §3.1 · p. 3, §3 · p. 3

3.1 Benchmark Construction and Pipeline Development

• The construction pipeline selects main theorems from parsed proof graphs, then uses source text and self-containment checks to complete their context.Expert-designed repairs resolve references, recover information-access and action-order rules, harmonize notation, and remove solution-revealing details; existence rewrites preserve assumptions and quantitative guarantees.Source: §3.1 · pp. 3–4, Figure 2 · p. 4
• Manual review found all 40 additional reviewed challenges faithful to their source results and self-contained; headline comparisons use the full 398-challenge collection.The 61 reviewed statements comprised 21 development challenges and 40 additional challenges.Source: §3.1 · p. 4

3.2 Evaluation Protocol

• Provers receive a self-contained theorem and cited prior work, but not the source paper, its construction graph, or artifacts containing the target proof.Three GPT-5.5 high-effort voters accept a submission when at least two vote PASS; identical submissions are also rescored with Opus 4.8.Source: Figure 3 · p. 4, §3.2 · p. 5
• Workflow comparisons match model-call opportunities and fix the backbone model, problem input, and tool access, while reporting input and output tokens separately.The automated rubric checks logical rigor, faithful use of assumptions and cited results, and quantitative correctness.Source: §3.2 · p. 5, Figure 4 · p. 5

3.3 Provisional Lean Statements

• The supplementary formalization pipeline retains 221 candidate Lean 4 statements, or 55.5% of 398 challenges, after compilation and two-reviewer checks.Candidates compile without sorry, admit, or untrusted axioms and are checked for back-translation consistency and degeneracy.Source: §3.3 · p. 6

4.1 Experimental Setup

• Ten configurations across four model families were tested with direct inference and 10-round discussion; agent workflows used GPT-5.5 xhigh under matched call opportunities.Direct inference used ten runs and discussion five; the agent comparison used up to 20 outer iterations per run.Source: §4.1 · p. 6

4.2 The Benchmark Separates Model Configurations

• 23.6% five-run coverage makes GPT-5.6 Sol max the leading discussion configuration; Fable 5 leads direct inference, showing that model rankings depend on inference organization.Fable 5 xhigh has the highest seed-1 direct acceptance (6.8%), while Fable 5 high has the highest ten-run direct coverage (14.6%).Source: §4.2 · p. 6, Figure 5 · p. 7
• One 10-round discussion run outperforms ten-run direct coverage for all eight GPT and Opus configurations, while Fable 5 favors direct coverage.For Sol max, one discussion run reaches 18.8% versus 13.8% for ten-run direct coverage.Source: §4.2 · p. 6, Figure 5 · p. 7

4.3 Agent Design Changes Effectiveness and Cost

• 25.4% five-run coverage for agentic planning exceeds MCTS's 24.1%, despite lower seed-1 acceptance (18.1% versus 19.3%) and higher sampled token use.Planning averages 60.4M input and 9.0M output tokens per run, versus MCTS's 27.4M and 3.9M.Source: Figure 6 · p. 7, §4.3 · p. 8
• Root-only decomposition raises five-run coverage from 21.1% to 23.4% versus discussion; finding easier, jointly sufficient subgoals remains a substantive reasoning task.MCTS has 19.3% seed-1 acceptance, but its five-run coverage exceeds root-only decomposition by only three challenges (96 versus 93).Source: §4.3 · pp. 7–8

4.4 Diagnostic Analyses and Broader Uses

• Differential privacy was difficult for Sol max: it covered 2 of 33 challenges (6.1%), compared with 23.6% overall coverage.Figure 7 plots within-topic coverage alongside topic shares of the benchmark.Source: §4.4 · p. 8, Figure 7 · p. 8
• Opus re-scoring preserves the ordering of eight shared configurations, and both verifiers find no clear MCTS advantage over root-only decomposition.Five-run counts change from −6 to +2 under the alternate verifier.Source: §4.4 · p. 8
• Post-cutoff coverage is higher for seven of ten configurations, but differences range from −4.0 to +4.3 percentage points, with no consistent pre-cutoff advantage.The authors identify source-date partitions and fresh challenge batches as potential diagnostics for studying training exposure.Source: §4.4 · p. 8, Figure 8 · p. 9

5 Conclusion

• Discussion and repeated sampling improve coverage, while agentic planning achieves the highest five-run coverage among the tested workflows when maximizing coverage takes priority.Root-only decomposition provides further gains at substantially lower token cost than agentic planning.Source: §5 · p. 9

AI use statement

• The authors used generative AI for synthetic data, method and experiment work, dataset cleaning, writing refinement, and literature research, but not for mathematical claims or proofs.They state that they reviewed AI-assisted work, writing, citations, and generated code.Source: AI use statement · p. 9

Reproducibility statement

• The authors plan to release 166 challenges from 57 licensed papers and provide titles for all 138 papers used.They say the pipeline and prover workflow should be reproducible using the prompts in Appendix E.Source: Reproducibility statement · p. 9

A Research Challenge: Calibeating from online regret bounds

• The example challenge adapts Theorem upper.bound from Calibeating Made Simple into an existence claim and omits its proof.The source version is identified as v1 and licensed under CC BY 4.0.Source: A Research Challenge: Calibeating from… · p. 13

Definitions and setup

• Each round presents external forecasts before the learner predicts; the outcome then reveals the incurred proper-scoring loss, with forecasts assumed fixed by an oblivious adversary.A proper loss makes the reported distribution minimize expected loss when it matches the outcome distribution.Source: Definitions and setup · p. 13
• The setup defines cumulative loss, refinement, calibration error, and multi-calibeating rate to state the benchmark theorem’s prediction guarantees.Multi-calibeating compares the learner’s loss with each external forecast’s refinement score plus an additive rate.Source: Definitions and setup · p. 13
• Regret is defined against the best fixed prediction, while Q denotes the set of distinct external forecast values over the horizon.The number of rounds on which the learner predicts a particular value is denoted n_T(p).Source: Definitions and setup · pp. 13–14

The challenge

• Under a proper loss and an online algorithm with concave regret bound α(T), the challenge asks for an algorithm that is |Q| α(T/|Q|)-calibeating.The construction is withheld by phrasing the target as an existence claim.Source: The challenge · p. 14

B Dataset Construction and Validation

• The appendix covers challenge construction, statement review, versioning, and a supplementary pipeline for provisional Lean statements.Source: B Dataset Construction and Validation · p. 14

B.1 Source Papers and Problem Selection

• Candidate papers are STOC 2026 and COLT 2026 papers with public arXiv versions; public releases additionally require CC BY 4.0 or CC0 licensing for the exact version.Papers are retrieved through the arXiv API with their TeX sources.Source: §B.1 · p. 14
• A model-assisted screen selects papers with sample- or runtime-complexity bounds, then identifies nontrivial theorem-level claims suitable for self-contained challenges.Each paper receives one primary area, including fairness and calibration, privacy, learning theory, optimization, sampling, or Other.Source: §B.1 · p. 14

B.2 Proof-Graph Construction

• Each numbered result becomes a graph node with its assumptions and proof, while direct invocations become edges and a glossary records paper-specific terms and definitions.Deterministic checks and semantic audits flag structural and content issues; the source graph is withheld from provers, who can access cited prior work.Source: §B.2 · p. 15

B.3 From Research Papers to Self-Contained Challenges

• The challenge pipeline selects headline theorems, assembles definitions and notation, and iteratively checks for missing context.The loop stops at a fixed round limit or when no new context can be added; remaining gaps are recorded for repair.Source: §B.3 · p. 15
• Repair passes add definitions and referenced material, normalize notation, specify information access and action order, harmonize assumptions, and remove intermediate results.When algorithm design is part of the task, named constructions and their pseudocode are removed so the challenge withholds the construction.Source: §B.3 · p. 15
• Table 1 reports Lean-statement retention by topic after compilation and automated semantic filtering, but retention is a construction diagnostic, not expert-validated accuracy.Source: Table 1 · p. 16

B.4 Statement Review and Versioning

• All 40 additional reviewed challenges were judged faithful to source results and self-contained; the headline model and workflow comparisons use all 398 challenges.The 61 reviewed statements comprised 21 development challenges and 40 additional challenges.Source: §B.4 · p. 16
• Future releases can add versioned batches from newly released papers while preserving earlier evaluation sets and recording new and unchanged challenges and splits.Source: §B.4 · p. 16
• Publication-date partitions by assumed model-family knowledge cutoffs are only a coarse diagnostic and cannot rule out contamination.Source: §B.4 · p. 16

B.5 Provisional Lean Statement Construction

• A formalization agent writes Lean declarations that must compile without sorry, admit, or untrusted axioms, then separate consistency and degeneracy gates assess semantic fidelity.Gate acceptance requires at least two yes votes from each of two model-family juries on both gates.Source: §B.5 · p. 16
• After up to five generation-and-review rounds, the pipeline retained 221 compiler-valid candidates from 398 challenges, or 55.5%.Revision uses dissent on the best candidate so far, ranked by gates passed and then total yes votes.Source: §B.5 · p. 16

C.1 External Verification and Author Inspection

• Three external voters judge each rewritten proof, requiring two PASS votes; an author found all 10 reviewed accepted proofs correct.The internal verifier does not determine benchmark labels.Source: §C.1 · p. 17

C.2 Agent Workflow Definitions

• The four workflows use discussion, root-only decomposition, agentic planning, or decomposition with MCTS to coordinate proving and verification.Agentic planning revises a lemma DAG after failure; MCTS searches an AND–OR tree and checks reductions and recombination.Source: §C.2 · pp. 17–18
• MCTS ranks open goals by importance-weighted upper confidence bounds, with importance tracking each goal’s share of root proof difficulty.The evaluator estimates completeness and solvability; search propagates outcomes and values through ancestors before separately verifying the assembled proof.Source: §C.2 · pp. 17–18
• Decomposition workflows are assessed on reduction validity, subgoal simplicity and acceptance, and recombination soundness.Only the final recombined proof contributes to acceptance.Source: §C.2 · p. 18

C.3 Budgets and Reporting

• Agent workflows use matched model-call opportunities and fixed run limits; direct inference uses ten runs, while discussion and agent workflows use five.Each agent challenge–seed run permits at most 20 outer iterations, six parallel proof goals, and 10 discussion rounds per goal per iteration; every role’s calls count toward the budget.Source: §C.3 · p. 18
• Multi-run coverage counts each challenge once if any independent run is accepted, and input and output tokens are reported separately.Agent token counts are averaged per challenge–seed run over 10 selected challenges and five seeds.Source: §C.3 · p. 18

C.4 Confidence Calibration

• Calibration compares each model’s pre-evaluation confidence with proof acceptance across confidence bins, targeting individual-proof acceptance rather than union-of-runs coverage.The reported calibration uses all 398 challenges.Source: §C.4 · p. 18

• Model and agent acceptance comparisons cover all 398 challenges; the Lean diagnostic covers the 221 retained candidate statements.Source: D Detailed Results and Diagnostics · p. 18

• MathArena reports average final-answer accuracy, whereas TCSAlgBench reports five-run proof coverage under 10-round discussion, so the metrics and protocols differ.Table 2 presents published MathArena results and TCSAlgBench five-run coverage in percent.Source: §D.1 · p. 18, Table 2 · p. 19

D.2 Complete Model Results

• Direct-inference results cover all 398 challenges, report accepted counts and percentages, and exclude Fable 5 max because of output-token access limits.Ten-run coverage counts challenges accepted in any of ten independent runs.Source: Table 3 · p. 19, §D.2 · p. 19
• Discussion results are broken down by topic; one full 10-round run averages approximately 453.7K input and 51.4K output tokens per challenge across eight non-Fable configurations.The table reports seed-1 results and five-run coverage by topic.Source: §D.2 · p. 19, Table 4 · p. 20
• Alternative-verifier results compare five-run coverage for eight configurations using the same proofs, with the reported delta defined against majority-vote coverage.Source: Table 5 · p. 20, §D.2 · p. 20
• The cutoff analysis partitions verifier-accepted proofs around assumed model-family knowledge cutoffs, but cannot establish training-set membership and may reflect cohort differences in topic or difficulty.Table 6 reports seed-1 and five-run results, with percentages calculated within cutoff cohorts or across all 398 challenges.Source: §D.2 · pp. 20–21, Table 6 · p. 21
• Fable 5’s high/xhigh five-run union contains 69 challenges overall: 32 before and 37 after the assumed cutoff.Table 7 also reports overlap and challenges accepted uniquely under either effort setting.Source: Table 7 · p. 21, §D.2 · p. 21

D.3 Complete Agent-Design Results

• Agentic planning processed approximately five times the input and nine times the output tokens of discussion without decomposition in the sampled comparison.Table 8 describes a call-matched comparison using GPT-5.5 xhigh and the same external verifier.Source: Table 8 · p. 22, §D.3 · p. 22

D.4 Confidence and Verifier Acceptance

• Calibration and verifier-acceptance rankings differ; Opus 4.8’s low errors are consistent with confidence near the low acceptance base rate, not identifying its rare accepted proofs.Reliability diagrams, Brier scores, and expert labels are needed for a stronger proof-level interpretation.Source: §D.4 · p. 22

D.5 Prospective Formalization Resource

• 221 of 398 challenges (55.5%) yielded compiler-valid Lean declarations, while tested baseline agents produced zero accepted sorry-free Lean proofs on these candidates.The candidates remain a prospective resource for formalization research.Source: §D.5 · p. 22

E Prompt Templates

• The appendix records representative construction and proof-agent prompts, preserving instruction wording and noting the external verifier’s framing adjustment.Double-braced names indicate runtime substitutions; labels such as [SYSTEM], [USER], and [OMITTED: ...] are editorial.Source: E Prompt Templates · p. 22

E.1.1 Challenge Selection and Assembly

• The selector chooses usually one to four headline theorems and the minimal definitions needed to understand each statement, excluding results used only in its proof.It also returns a brief plain-language intuition without proof.Source: §E.1.1 · p. 23

E.1.2 Challenge Refinement

• Challenge refinement uses iterative self-containment checks to identify missing definitions and glossary matching to repair unresolved terminology.Other passes complete references, notation, information access, and action order; removal of intermediate results is deterministic.Source: §E.1.2 · pp. 23–25
• When a named construction is part of the challenge, refinement rewrites it as an existence claim and adds a scoping clause when needed to prevent unintended use of supplied black boxes.The rewriting rules preserve hypotheses, assumptions, parameters, bounds, complexity expressions, probabilities, and quantifiers.Source: §E.1.2 · pp. 25–26

E.2.1 Prover

• Direct inference invokes the prover once, whereas discussion adds verifier feedback and revision; prover instructions require exact retrieved-result statements, hypothesis checks, and explicit tracking of quantitative bounds.The settings share prover and verifier role prompts but differ in role invocation and supplied context.Source: §E.2.1 · p. 27
• The prover must give a direct proof using only admissible sources, establish any unproved subgoal inline, and avoid silently strengthening the statement’s hypotheses.Admissible sources include the statement’s hypotheses and definitions, standard results, retrieved snippets, and already-proved sibling or child subgoals.Source: §E.2.1 · p. 28

E.2.2 Verifier

• Three separately sampled GPT-5.5 high-effort voters accept a proof with at least two PASS votes, and final proofs undergo structural checks before detailed verification.The structural stage checks statement integrity, completeness, citations, and additional rules; detailed verification runs only if all structural phases pass.Source: §E.2.2 · pp. 30–31

E.2.3 Decomposer

• The decomposer proposes one to three alternative reductions whose children jointly imply the goal, rejecting added premises that grant away the problem’s hard part.Each child must preserve the goal’s free variables and assumptions and be strictly weaker than the goal.Source: §E.2.3 · p. 32

E.2.4 Planner and Plan Refinement

• The planner creates ordered, dependency-aware proof-plan DAGs with precise claims, where later steps may use earlier conclusions and the proof order must be topological.Steps must preserve relevant variables and assumptions, be strictly weaker than the goal, and not assume the hard part for free.Source: §E.2.4 · p. 33
• After an unsuccessful search, the planner receives failure feedback and must seed a fresh root with a materially different proof decomposition while reusing the prompt requirements.Feedback includes the root outcome, estimated search value, composite-attempt count, reduction subgoal counts, and truncated unclosed subgoals with their last objections.Source: §E.2.4 · p. 34

E.2 Proof Agent

• Agents receive the challenge, its definitions and assumptions, and retrieved cited prior work as proof inputs.Source-paper lemmas and the target proof are withheld.Source: §E.2 · p. 27
• Ancestor goals, sibling subgoals, and decomposition children are claims created during search, not supplied as initial facts.Source: §E.2 · p. 27
• Empty histories and optional context blocks are omitted at runtime; the external scoring verifier receives separate inputs.Source: §E.2 · p. 27