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

Summary (Overview)

• FORMALTCS is a new expert-validated benchmark for evaluating LLMs on frontier, end-to-end TCS research, containing 175 instances from papers accepted to STOC, FOCS, SODA, and COLT in 2025–2026.
• The benchmark decomposes the TCS research pipeline into five stages (core claim → NL claim → formal theorem → NL proof → formal proof) with expert-verified Lean 4.32.2 formalizations and proofs.
• Autoformalization (NC2FT) is identified as the sharpest bottleneck: the best model (CLAUDE-OPUS-5) 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 FORMALTCS, the authors develop an automated TCS research framework with planner/formalizer/judger agents; of 64 generated claims, only 6 pass expert evaluation and proof verification, indicating limited "research taste" in current LLMs.
• The paper identifies two complementary directions for progress: improving autoformalization and developing stronger research taste in LLMs.

Introduction and Theoretical Foundation

Theoretical computer science (TCS) studies fundamental principles of computation through mathematical methods, including models of computation, algorithms, computational complexity, and limits of computability. TCS provides the theoretical foundation for understanding which problems can be computed and how efficiently.

Existing TCS benchmarks (e.g., LCS-Bench, TCS-Bench) exhibit substantial gaps from real-world research:

1. Incomplete research pipeline: They evaluate isolated capabilities (autoformalization or proof generation) rather than end-to-end research.
2. Outdated content — constructed from textbooks or theorems already in libraries like Mathlib, risking data contamination and lacking frontier relevance.
3. Simplified problem settings — focus on self-contained theorems, while real papers involve paper-specific definitions, assumptions, and multi-layered dependencies among lemmas and theorems.

FORMALTCS addresses these gaps by providing:

• (i) End-to-end evaluation — decomposes the pipeline into five stages for fine-grained diagnosis.
• (ii) Frontier research content — from 2025–2026 top conference papers with contamination filtering.
• (iii) Realistic research problems — preserves paper-specific definitions, assumptions, and proof dependencies.

Methodology

Data Format and Statistics

FORMALTCS contains 175 instances, each from a distinct research paper. Each instance includes:

Quality dimensions: (i) High difficulty — expert-validated Lean proofs average 22.0 statements and 29.6 nodes; (ii) High diversity — spans 13 major TCS research areas.

Annotator Pipeline

Five human experts (each with multiple top-tier TCS publications) participate, assisted by GPT-5.6-SOL and CODEX. The pipeline involves:

1. Source paper selection — Automated scripts scan STOC/FOCS/SODA/COLT 2025–2026 papers; human experts verify relevance. A black-box audit (queries to GPT-5.6-SOL and CLAUDE-OPUS-5 with partial theorem statements) shows completion similarity below 9.6%, indicating low contamination risk.

2. Core claim generation — Concise summaries (<36 words, minimal notation) of central theoretical results. Two experts independently write candidates; a third selects the stronger.

3. Natural language claim — Theorems are rewritten to be self-contained when they depend on paper-specific definitions, then reviewed by another expert for faithfulness.

4. Formal language theorem and proof — LLM generates a proof-blueprint DAG, human experts verify structure, then the LLM proves nodes in dependency order. Human experts check rigor (no sorry or axioms), and an independent end-to-end review fixes remaining issues. The final theorem is extracted with the proof body replaced by sorry.

5. Natural language proof — LLM generates a proof sketch from the verified formal proof and paper; human experts check faithfulness and completeness.

Tasks and Metrics

FORMALTCS includes four tasks:

Metrics:

• LLM-Rubric (CC2NC, C2NP): weighted score based on logical validity, completeness, correctness, clarity: $\mathrm{Score} = 0.4 s_{\mathrm{logic}} + 0.3 s_{\mathrm{complete}} + 0.2 s_{\mathrm{correct}} + 0.1 s_{\mathrm{clear}}$
• BEq+ (NC2FT): bidirectional theorem proving — proves both $t_r \Rightarrow t_c$ and $t_c \Rightarrow t_r$ in Lean for reference theorem $t_r$ and candidate $t_c$.
• Pass@k (FT2FP): proportion of instances where at least one of k sampled proofs is accepted by the Lean compiler (with warningAsError true and #print axioms checks).

Generation parameters: 8 candidates for NC2FT and FT2FP (temperature 0.6, top p 0.9); single generation for CC2NC and C2NP (temperature 0.0, top p 1.0).

Empirical Validation / Results

Main Results (Table 4)

Key Findings

Finding 1: Current LLMs struggle with end-to-end TCS research. Even the best model (CLAUDE-OPUS-5) achieves only 66.9 and 68.7 on natural-language tasks, but formal proof generation drops to 28.6 Pass@8.

Finding 2: Formalization tasks are substantially more difficult than natural-language tasks. CLAUDE-OPUS-5 achieves 68.7 on C2NP but only 11.5 on NC2FT; GPT-5.6-SOL achieves 67.9 vs. 10.6.

Finding 3: Autoformalization is the primary bottleneck. NC2FT is the lowest-performing stage (no model exceeds 11.5), while FT2FP reaches 28.6 when given human-annotated formal statements. The fundamental challenge lies in identifying mathematical objects, assumptions, and logical structure to translate into formal definitions.

Automated Research Framework (Section 5)

A multi-agent framework (planner, formalizer, judger) using GPT-5.6-SOL with CODEX:

• Planner proposes new research objectives with flexibility to reformulate, strengthen, or relax assumptions.
• Formalizer translates objectives into Lean statements with up to 3 rounds of compiler feedback.
• Judger translates formal statements back to natural language, assesses novelty, and filters.

Results: Of 64 generated core claims, only 6 pass human evaluation and proof verification. Two representative accepted claims include:

Adaptive damping achieves the asymptotic coefficient 1/2 for sparse-state shift-recall loss. — If $K(n), T(n) \to \infty$ and $(2T(n) + 1)/K(n) \to 0$, then the specified diagonal linear RNN with adaptive damping $\alpha_n = \frac{1}{8} \log\left(1 + \min\{2T(n) + 1, K(n)/(2T(n) + 1)\}\right)$ satisfies $\frac{L_n - 1}{(2T(n) + 1)/K(n)} \to -\frac{1}{2}$.

2. Cutoff calibration error controls monotone-recalibration excess risk with the sharp constant 1. — For any threshold $\tau$, the excess cost-sensitive risk of $\mathbf{1}\{V \geq \tau\}$ relative to the best monotone recalibration is at most $\sup_I |\mathbb{E}[(Y - V)\mathbf{1}\{V \in I\}]|$, where $I$ ranges over order-connected sets. The coefficient 1 is optimal.

Interestingly, the proof success rate for accepted claims is higher than FT2FP performance, since LLMs can more easily prove claims aligned with their own reasoning trajectories.

Theoretical and Practical Implications

Theoretical:

• Establishes a rigorous, expert-validated benchmark for research-level TCS evaluation.
• Demonstrates that mathematical modeling (autoformalization) is a more fundamental limitation than proof generation itself.
• Suggests that LLM's "research taste" — the ability to generate novel and valuable claims — is a distinct capability from proving ability, and is currently underdeveloped.

Practical:

• Provides a realistic testbed for measuring LLM progress toward autonomous TCS research.
• The stage-wise evaluation enables fine-grained diagnosis of model capabilities.
• The automated framework demonstrates a prototype of a full research pipeline, though with limited success rate (6/64).

Conclusion

FORMALTCS is an expert-validated benchmark for evaluating LLMs across the end-to-end pipeline of frontier TCS research, using recent conference papers and expert-verified Lean formalizations. Key findings:

• LLMs perform substantially better at understanding and reasoning about TCS problems in natural language than at expressing them formally.
• Autoformalization is the primary bottleneck.
• Models can often prove claims that survive expert screening, but only a small fraction of their proposed claims are novel and valuable, indicating limited research taste.

Progress toward autonomous TCS research requires advances along two complementary dimensions:

1. Accurately translating research ideas into rigorous formal objects (autoformalization).
2. Developing a stronger research taste for identifying meaningful theoretical claims.

Future directions include improving autoformalization capabilities, developing automated claim-quality evaluators, and using FORMALTCS as a realistic testbed for measuring progress toward autonomous TCS research.