Large language models can describe and reason about advanced theoretical computer-science ideas more effectively than they can turn those ideas into formal statements and machine-checkable proofs, according to a new benchmark. The gap was clearest at the translation stage known as autoformalization, where no evaluated model scored above 11.2. When a human supplied the formal theorem, proof generation reached as high as 28.7 Pass@8, a measure based on whether at least one accepted proof appears among eight attempts.
The benchmark contains 143 instances drawn from 143 distinct research papers. Its source pool consisted of papers accepted to the STOC, FOCS, SODA and COLT conferences in 2025 and 2026. FormalTCS was designed to test several stages of theoretical computer-science research, from understanding a claim in ordinary language to producing a formal theorem and proof.
The study evaluated four stages separately and gave models human-annotated inputs at each stage, rather than feeding one model’s output into the next step. That design helps locate a weak link, but it does not measure how errors would accumulate in a single fully automated run. The experiments covered three model families: GPT, Claude and DeepSeek.
The hardest step came before the proof
Claude Opus-5 was reported as the strongest model on most tasks. It scored 66.9 on understanding natural-language claims and 68.7 on generating proof strategies, yet its final formal-proof result was 28.7 Pass@8. The contrast matters because the first two numbers are rubric scores for language-based tasks, while Pass@8 asks whether at least one of eight candidate outputs is accepted as a proof.
To score the language-based tasks, the researchers used an LLM-Rubric that combined four component scores, each normalized to a 0-to-100 scale. Logical validity carried 40% of the total, completeness 30%, correctness 20% and clarity 10%. The formalization and proof results were reported as separate stages, so a model could perform well at explaining a theorem while struggling to express it in a form suitable for proof checking.
The benchmark also tested whether the framework could produce research claims of its own. Its automated loop used three roles: a planner to propose directions, a formalizer to express them in formal language, and a judger to assess the results. The system generated 64 core claims, but only six remained after expert evaluation and proof verification. Two experts independently reviewed candidate claims for novelty and potential value in theoretical computer science, and the framework did not use an automated claim-quality evaluator.
Checks strengthened the benchmark, but did not settle the bigger question
Human checks produced agreement of 86% for core claims, 90% for natural-language claims and 93% for formal-language proofs. Experts still made substantive revisions to 13% of natural-language proofs, 15% of formal-language proofs, 24% of proof blueprints and 31% of formal-language theorems. The figures show that the annotations used to split the benchmark into stages still needed expert correction in a portion of cases.
The authors also ran an output-only black-box audit for possible paper leakage. Aggregate completion similarity was below 9.6% for both audited models. They treated that as evidence of low contamination, not proof that the papers had never appeared in training data.
These results do not amount to a demonstration that AI can conduct theoretical computer-science research autonomously. FormalTCS uses a selected source pool from four conferences, and its agent-generated claims were judged by two experts for novelty and potential value. The black-box audit was also an output-only check, so its low similarity result does not prove that the papers were absent from model training data.
In this benchmark, the clearest weakness was not the ability to discuss a theorem or outline a proof, but the step between those abilities and a formal statement that can be checked. The result leaves open whether the same pattern would appear with newer papers, broader areas of theoretical computer science or future model snapshots.
Paper data and sources
Original title: FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models
Authors: Dingzirui Wang, Xuanliang Zhang, Keyan Xu et al.
Journal/Repository: arXiv
Status: Preprint, not yet peer-reviewed
First online: 2026-08-20
DOI: Not available
Original paper · Full text