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

• URL: http://arxiv.org/abs/2608.09538v2
• Date: Thu, 13 Aug 2026 16:11:12 GMT
• Title: TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability
• Abstract summary: We introduce TCS-Bench, a benchmark for evaluating Large Language Models (LLMs) on research-level Theoretical Computer Science (TCS) proof generation.<n> TCS-Bench consists of theorem-proving tasks from papers published at top theoretical computer science venues.
• Score: 59.079078796751496
• License: http://creativecommons.org/publicdomain/zero/1.0/
• 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.

Related papers

• FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models [53.68149869349268]
  Large language models (LLMs) have shown growing potential for automated theoretical computer science (TCS) research.<n>We introduce ourbenchmark, an expert-validated benchmark for evaluating LLMs on frontier, end-to-end TCS research.
  arXiv  Detail & Related papers  (2026-08-20T15:13:41Z)
• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T is a framework that evaluates the semantic correctness of formal theorems.<n>We construct a benchmark from 5 real-world Lean 4 repositories.<n>Experiments demonstrate that while state-of-the-art models achieve high compilation success, they perform significantly worse under our semantic metric.
  arXiv  Detail & Related papers  (2026-04-26T13:24:20Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  Large language models (LLMs) have demonstrated significant potential in formal theorem proving.<n>We exploit an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts.<n>We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration.
  arXiv  Detail & Related papers  (2026-03-13T01:33:20Z)
• Neural Theorem Proving for Verification Conditions: A Real-World Benchmark [9.350519191460018]
  This work introduces Neural Theorem Proving for Verification Conditions (NTP4VC), presenting the first real-world multi-language benchmark for this task.<n>We evaluate large language models (LLMs), both general-purpose and those fine-tuned for theorem proving, on NTP4VC.
  arXiv  Detail & Related papers  (2026-01-26T20:37:11Z)
• RPC-Bench: A Fine-grained Benchmark for Research Paper Comprehension [65.81339691942757]
  RPC-Bench is a large-scale question-answering benchmark built from review-rebuttal exchanges of high-quality computer science papers.<n>We design a fine-grained taxonomy aligned with the scientific research flow to assess models' ability to understand and answer why, what, and how questions in scholarly contexts.
  arXiv  Detail & Related papers  (2026-01-14T11:37:00Z)
• Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics [1.2978846076301875]
  Ax-Prover is a multi-agent system for automated theorem proving in Lean.<n>It can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts.<n>We benchmark our approach against frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks we introduce in the fields of abstract algebra and quantum theory.
  arXiv  Detail & Related papers  (2025-10-14T17:57:04Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving [36.194330645092634]
  In this paper, we introduce an INequality Theorem proving benchmark, specifically designed to test agents' generalization ability. Int is based on a procedure for generating theorems and proofs; this procedure's knobs allow us to measure 6 different types of generalization. We then evaluate the same agents augmented with Monte Carlo Tree Search (MCTS) at test time, and show that MCTS can help to prove new theorems.
  arXiv  Detail & Related papers  (2020-07-06T17:55:33Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.