# Theory-Scale Auto-Formalization of Logics for Computer Science

arXiv: https://arxiv.org/abs/2606.26525 · HTML: https://mlsanity.com/paper/2606.26525/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 45 of its 70 references that are in the map.
- First posted on arXiv 25 Jun 2026.

## Builds on (most cited first, 30 of 45)

- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [OpenHands: An Open Platform for AI Software Developers as Generalist Agents](https://mlsanity.com/paper/2407.16741/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Pyro: Deep Universal Probabilistic Programming](https://mlsanity.com/paper/1810.09538/) (2018)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [NeurASP: Embracing Neural Networks into Answer Set Programming](https://mlsanity.com/paper/2307.07700/) (2023)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Scallop: A Language for Neurosymbolic Programming](https://mlsanity.com/paper/2304.04812/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics](https://mlsanity.com/paper/2505.03171/) (2025)

## Built on by (most cited first, 4 of 4)

- [Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs](https://mlsanity.com/paper/2608.15432/) (2026)
- [FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models](https://mlsanity.com/paper/2608.20153/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)

## Abstract (arXiv)

Auto-formalization is critical for scalable formal verification, but existing progress largely focuses on isolated statements, while theory-scale auto-formalization, which coherently translates hundreds of interdependent definitions, lemmas, and theorems, remains open due to challenges in consistency, faithfulness, scalability, and correctness. In this paper, we introduce LCS-Bench, a stand-alone, theory-scale benchmark based on Logics for Computer Science. LCS-Bench is built through a novel semi-automated agentic pipeline that leverages concept graphs, formal signature planning, issue tracking, sorry-filling with counter-example search, complemented by faithfulness review from human experts. The resulting artifact covers 327 textbook items, over 4,076 Lean declarations, and more than 85K lines of Lean code. The dataset supports broad evaluation through a data engine that automatically derives five tracks of evaluation benchmarks, measuring different aspects of auto-formalization and theorem-proving capabilities. We also introduce a novel evaluation protocol featuring definitional equivalence checkers, enabling more fine-grained and faithful assessment. Through extensive evaluation on 14 models, we demonstrate that (1) LCS-Bench is of high quality, consistent, and faithful; (2) the benchmark is challenging, with state-of-the-art models achieving only 20.1% on auto-formalization tasks; and (3) our analysis reveals key findings regarding theory-scale auto-formalization and suggests promising directions for future work.