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

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

Abstract

The paper introduces 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. The authors evaluate state-of-the-art models on this benchmark, verifying the correctness of generated proofs via a verification agent. The reference verifier achieves over 90% accuracy on an expert-labeled set.

Introduction

The paper notes that LLMs have achieved superhuman performance on standardized benchmarks, including professional exams and programming competitions, and have extended into formal mathematics, with models demonstrating IMO gold-medalist-level problem solving. Recently, these capabilities have crossed into open-ended scientific discovery, with models contributing to expert-level mathematical breakthroughs, such as solving open problems, refuting conjectures, and generating novel proofs across TCS, optimization, and physics.

However, the authors identify a critical gap: a significant gap has emerged between what state-of-the-art agents can achieve in active research and what our standardized benchmarks can actually measure. Existing benchmarks fail to capture real-world mathematical research difficulties because: (1) competition problems are self-contained, whereas research theorems are embedded in bespoke definitions, notations, and previously established lemmas; (2) research results frequently involve constructing a scaffold of interconnected results, going beyond finding a single clever insight.

Contributions

The paper's key contributions are:

• TCS-Bench, a benchmark composed of 300 theorem-proving tasks from papers published at FOCS, STOC, and SODA between 2020 and 2026.

• An automated proof verification system achieving more than 90% accuracy against human expert judgments on a held-out set of 100 human-labeled proofs.

The task construction involves scraping and processing LaTeX source of papers, building dependency graphs of statements, and assembling multiple versions of context for each statement, hiding varying subsets of dependencies. Each task is packaged as a self-contained JSON entry with three fields: context, target statement, and ground-truth proof.

Related Work

The paper situates TCS-Bench at the intersection of benchmarks for mathematical reasoning, formal proof generation, and AI in scientific research. It contrasts with:

• Competition mathematics benchmarks (e.g., IMO-based) which test self-contained problems, whereas TCS-Bench requires reasoning within rich interdependent theoretical contexts.

• Research-level mathematical benchmarks like HorizonMath (unsolved problems with generator-verifier gaps), LemmaBench (automatically extracted lemmas from arXiv preprints), and BrokenMath (evaluating sycophancy in theorem proving). TCS-Bench differs by targeting proof completion within the contextual dependencies of published TCS papers.

• Formal theorem proving benchmarks (Lean, Coq) which test machine-verifiable proofs, whereas TCS-Bench focuses on complete, human-readable natural language proofs.

• AI for scientific discovery benchmarks like PaperBench (replicating empirical AI research), whereas TCS-Bench is the first to focus on replicating theoretical contributions.

The TCS Benchmark

Data Acquisition and Preprocessing: The benchmark is constructed from papers published at FOCS, STOC, and SODA between 2020 and 2026. LaTeX source is obtained from arXiv, limited to papers under permissive licenses (CC-0 or CC-BY-4.0). Target statements whose proofs invoke external results without restating them are skipped to ensure self-containment.

Dependency Structure Construction: The core is a structural analysis extracting the logical dependency structure of each paper, producing a directed acyclic graph (DAG) over all formal statements. A deterministic LaTeX parser identifies theorem-like environments, and an LLM-based analysis pass maps proofs to statements and constructs dependency edges. Acyclicity is programmatically verified. Each statement's rank is computed as the length of the longest directed path terminating at that node, with definitions and axioms at rank 0. This ranking stratifies tasks by difficulty and prevents information leakage during context assembly.

Task Construction: Each task consists of context, target statement, and ground-truth proof. The context is assembled by concatenating resolved external reference digests, the paper's text truncated at the start of the target proof, with statements of rank ≥ r hidden and all proof environments removed. Dependencies falling outside the truncated portion are re-inserted. To create scalable difficulty, multiple variants are generated by systematically withholding intermediate results. Context compression uses iterative section pruning (removing irrelevant sections) and an LLM shortener to condense remaining context while preserving mathematical content, keeping tasks within a 10,000-token limit.

Quality Filtering: Tasks are rejected if they fail structural checks (figure/image references, label leaks, exceeding token limits, incomplete dependency coverage, unresolved references) or semantic checks (well-definedness, unambiguity and correctness, context coherence) performed by three independent LLM calls.

Task Formulation Summary: Each task provides a self-contained LaTeX context (≤10,000 tokens) with definitions, prior results (proofs omitted), and condensed external reference digests, plus a target statement. The solver must produce a complete proof using only the provided context, without accessing the original paper or external sources.

Automated Proof Verification

The verifier makes a binary decision (correct/incorrect) on a candidate proof. It is provided with the task's context, target statement, and ground-truth proof. Four calls are made to Gemini 3.1 Flash, and a candidate proof is deemed correct if at least three of four verdicts mark it correct. The verifier prompt was calibrated using GEPA improvement pipeline on 50 correct and 50 incorrect human-labeled proofs, achieving over 90% accuracy.

Experimental Setup

The authors evaluate frontier models: Gemini 3.1 Pro, Gemini 3.1 DeepThink, Opus 5, and GPT 5.6 Pro, plus an internal harness called Colosseum run with Gemini 3.1 Pro, Gemini 3.6, and a combination. Models are queried with context and target statement, using maximum thinking budgets. Generated proofs are evaluated with the automated verifier. Each model attempts all 300 tasks.

Results

Table 1 shows:

• Opus 5: 32.77% accuracy (exhausts token budget of 128K tokens before answering for 162 of 300 tasks)

• Gemini 3.1 Pro: 30.3% accuracy

• Gemini 3.1 DeepThink: 52% accuracy

• GPT 5.6 Pro (max): 68% accuracy (successfully proving 204 of 300 tasks)

Colosseum Results: Running Colosseum on two base models (Gemini 3.1 Pro and Gemini 3.6 Flash) with automated cross-model selection:

• Colosseum with Gemini 3.1 Pro: 54.0% accuracy (162/300 solved)

• Colosseum with Gemini 3.6 Flash: 46.7% accuracy (140/300 solved)

• Cross-model selection between the two: 67.7% accuracy (203/300 solved)

• Oracle best-of-two (upper bound): 72.3% accuracy (217/300 solved)

The selection rule submits Gemini 3.6 Flash's proof when either Colosseum's internal verifier declined to certify Gemini 3.1 Pro's proof, or at most half of 8 independent critiques from Gemini 3.6 Flash judge Gemini 3.1 Pro's proof correct. The rule selects Gemini 3.1 Pro on 167 problems (84% accuracy vs 54% before filtering) and Gemini 3.6 Flash on the remaining 133 (47% accuracy).

The paper finds that a model's self-acceptance carries little information, but self-rejection is highly informative. Routing on self-rejection alone raises accuracy from 54.0% to 63.7%. Cross-model critique provides a complementary signal: Gemini 3.6 Flash's critiques of Gemini 3.1 Pro's proofs separate correct from incorrect proofs with an AUC of 0.854, yielding a further 4.0-point gain. On 47 problems, the critique overturns a Gemini 3.1 Pro proof that its own verifier accepted; Gemini 3.6 Flash is correct 21 times vs 9 for Gemini 3.1 Pro. The direction matters: Gemini 3.6 Flash judging Gemini 3.1 Pro achieves AUC 0.854, while the reverse gives AUC 0.637. Performance is insensitive to critique threshold (67.3-67.7% for thresholds 0/8 through 5/8).

Discussion

The paper introduces TCS-Bench as the first benchmark evaluating LLMs on proof generation from cutting-edge TCS research. It requires reasoning within rich contextual scaffolding of research papers across 300 tasks spanning multiple difficulty levels. The automated proof verification system achieves over 90% accuracy against human judgments, enabling scalable evaluation. The strongest systems solve 52-68% of tasks (Gemini 3.1 DeepThink: 52%, GPT-5.6-Pro: 68%, Colosseum with cross-model: 67.7%). The gap to perfect performance reveals substantial room for advancement, with the stable performance ceiling suggesting current architectures face fundamental limitations in constructing multi-step mathematical arguments within complex dependencies. TCS-Bench is designed for longevity through continual addition of new papers postdating model training cutoffs, scalable difficulty via dependency-hiding, and rank-based stratification for fine-grained progress tracking.

Improvements to AI Systems Based on TCS-Bench

1. Implement self-rejection as a confidence signal for proof generation.

• What to build: Modify LLM inference to track whether the model’s internal verifier rejects its own generated proof. If rejected, trigger a second, independent generation attempt or route to a different model.

• Capability gained: The system improves proof accuracy from 54% to 63.7% on TCS-Bench tasks, reducing false positives without requiring external feedback.

2. Add asymmetric cross-model critique routing.

• What to build: Create a two-model pipeline where a weaker/faster model (e.g., Gemini 3.6 Flash) critiques the proof of a stronger model (e.g., Gemini 3.1 Pro) using a binary correctness score. Route the final submission to the critic’s model if the critique score falls below a threshold (e.g., ≤4/8 correct).

• Capability gained: Achieves 67.7% accuracy (vs. 54% for the stronger model alone), leveraging the critic’s higher discriminative power (AUC 0.854) over the reverse direction (AUC 0.637).

3. Integrate dependency-graph-aware context assembly for multi-step reasoning.

• What to build: During training or inference, structure the input context as a ranked DAG of lemmas/theorems (as in TCS-Bench), hiding intermediate results to force the model to reconstruct missing steps. Fine-tune on tasks with varying dependency-hiding levels.

• Capability gained: The model learns to reason within rich, interdependent theoretical contexts, improving performance on research-level problems beyond self-contained competition tasks.

4. Add automated proof verification with calibrated multi-vote consensus.

• What to build: Deploy a verifier that makes four independent LLM calls (e.g., Gemini 3.1 Flash) and accepts a proof only if ≥3/4 agree it is correct. Calibrate the prompt using a small human-labeled set (50 correct/50 incorrect) via iterative prompt optimization.

• Capability gained: Achieves >90% verification accuracy, enabling scalable, reliable evaluation of open-ended proofs without human oversight.

5. Use self-acceptance vs. self-rejection asymmetry to filter low-quality generations.

• What to build: In any multi-sample generation pipeline, discard proofs the model itself accepts with low confidence (since self-acceptance carries little signal), but retain proofs it rejects—then re-generate or refine them.

• Capability gained: Reduces wasted compute on false positives and focuses resources on uncertain cases, improving overall yield in proof-generation tasks.

6. Build a routing system that selects between models based on critique directionality.

• What to build: For each task, run two models (A and B). Have A critique B’s proof and B critique A’s proof. Submit the proof from the model whose critic has higher historical AUC (e.g., always use the model that is better at judging the other).

• Capability gained: Approaches the oracle best-of-two upper bound (72.3% vs. 67.7% achieved), maximizing accuracy by exploiting asymmetric evaluative strengths.

7. Add rank-based difficulty stratification for curriculum learning.

• What to build: Train models on tasks sorted by dependency rank (rank 0 = definitions, higher ranks = deeper theorems). Start with low-rank tasks (fewer hidden dependencies) and progressively increase rank.

• Capability gained: The model learns to construct multi-step proofs incrementally, improving generalization to novel research theorems with complex dependency scaffolds.

8. Implement token-budget-aware proof generation.

• What to build: Detect when a model exhausts its token budget without producing a proof (as Opus 5 did for 162/300 tasks) and automatically switch to a more concise reasoning strategy or a different model with higher efficiency.

• Capability gained: Prevents wasted inference and increases solve rate, especially for long-context research problems where verbose reasoning is a bottleneck.

9. Use context compression via iterative section pruning and LLM shortening.

• What to build: Preprocess any research paper input by removing irrelevant sections and condensing remaining context with an LLM shortener, while preserving mathematical content, to fit within a 10,000-token limit.

• Capability gained: Enables LLMs to handle full research papers (which often exceed context windows) without losing critical definitions or lemmas, improving performance on real-world theorem-proving tasks.

10. Add a self-containment check for external references.

• What to build: Before generating a proof, automatically detect if the target statement relies on external results not restated in the context. If so, either inject a digest of those references or flag the task as unsolvable.

• Capability gained: Prevents hallucinated proofs and ensures the model only attempts tasks where all necessary information is available, improving reliability in autonomous research settings.

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.