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

• URL: http://arxiv.org/abs/2608.20153v1
• Date: Thu, 20 Aug 2026 15:13:41 GMT
• Title: FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models
• Abstract summary: 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.
• Score: 53.68149869349268
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: Large language models (LLMs) have shown growing potential for automated theoretical computer science (TCS) research, yet existing benchmarks remain far from realistic research settings. We introduce \ourbenchmark, an expert-validated benchmark for evaluating LLMs on frontier, end-to-end TCS research. \ourbenchmark contains $175$ instances drawn from papers accepted to STOC, FOCS, SODA, and COLT in 2025-2026, preserving paper-specific definitions, assumptions, and proof dependencies, with expert-verified Lean formalizations and proofs. Evaluations of leading LLMs reveal that current models remain far from reliably completing the full research pipeline. In particular, autoformalization is the sharpest bottleneck: the best model 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 \ourbenchmark, we further develop an automated TCS research framework that generates, formalizes, filters, and proves new claims. Of $64$ generated claims, only $6$ ultimately pass expert evaluation and proof verification, indicating that beyond formalization, limited research taste remains another major barrier to autonomous TCS research.

Related papers

• TCS-BENCH: Benchmarking State-of-the-Art Generative AI Theoretical Computer Science Research Ability [59.079078796751496]
  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.
  arXiv  Detail & Related papers  (2026-08-10T12:36:16Z)
• CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference [17.447741518678374]
  CausalForge is a framework for automated theoretical research in causal inference.<n>It combines Causalean, a Lean library for causal inference, with CausalSmith, a self-improving agentic pipeline.
  arXiv  Detail & Related papers  (2026-07-24T17:32:35Z)
• Theory-Scale Auto-Formalization of Logics for Computer Science [36.45195518081978]
  LCS-Bench is a theory-scale benchmark based on Logics for Computer Science.<n>The artifact covers 327 textbook items, over 4,076 Lean declarations, and more than 85K lines of Lean code.<n>We demonstrate that LCS-Bench is of high quality, consistent, and faithful.
  arXiv  Detail & Related papers  (2026-06-25T01:59:53Z)
• 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)
• Learning to Predict Future-Aligned Research Proposals with Language Models [59.79457676644722]
  We build a time-consistent dataset of 17,771 papers from targets and their pre-cutoff citations.<n>To train models, we build a time-consistent dataset of 17,771 papers from targets and their pre-cutoff citations.<n>Across Llama-3.1 and Qwen2.5 models, future-aligned tuning improves future alignment over unaligned baselines.
  arXiv  Detail & Related papers  (2026-03-28T05:41:15Z)
• 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)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• 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)

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.