TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability
2026-08-10 • Computation and Language
Computation and LanguageArtificial Intelligence
AI summaryⓘ
The authors created TCS-Bench, a test to see how well large language models can write proofs for hard computer science problems. These problems come from top research papers and include all information needed to prove a specific statement. They tested current language models on these tasks and used a special program to check if the proofs were correct. This program was also tested against human experts and showed over 90% accuracy in judging proof correctness.
Theoretical Computer ScienceLarge Language ModelsAutomated Theorem ProvingProof VerificationBenchmarkSTOCFOCSSODAFormal ProofsMachine Learning
Authors
Vincent Cohen-Addad, Dimitris Paparas, Ernest van Wijland, Max Springer, Julien Canitrot-Paradis, Honghao Lin, David Woodruff, Adarsh Kumarappan, Rajesh Jayaram, Rudrajit Das, Lalit Jain, Ola Svensson, Silvio Lattanzi, Mislav Balunovic, Theophane Weber, Vahab Mirrokni
Abstract
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.