Skip to content

Theory-Scale Auto-Formalization of Logics for Computer Science

🕒 Published (v1): 2026-06-25 01:59 UTC · Source: Arxiv · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

LCS-Bench is a theory-scale auto-formalization benchmark built from a logic-for-CS textbook, covering 327 items, 4,076 Lean declarations, and 85K lines of Lean code. It is constructed via a semi-automated agentic pipeline and evaluated across five tracks; the best model (Claude Opus 4.6 in agentic mode) achieves only 20.1% on item-level auto-formalization, demonstrating the benchmark's difficulty. The work reveals that theory-scale coherence—not isolated statement translation—is the binding constraint.

Problem

Existing auto-formalization benchmarks cover isolated mathematical statements and rely on mature libraries (e.g., Mathlib, LeanDojo), masking the difficulty of building full formal theories from scratch. No prior benchmark demands translating hundreds of interdependent, heterogeneous artifacts—definitions, lemmas, theorems, algorithms, deeply embedded DSLs—into a single coherent Lean development, leaving theory-scale auto-formalization largely unsolved and unevaluated.

Method

The authors construct LCS-Bench from Logics for Computer Science (2nd ed.) via a four-stage semi-automated agentic pipeline:

  1. Pre-processing: PDF → structured Markdown with per-item XML tags (<theorem>, <definition>, etc.); graphics redrawn as ASCII; implicit prose assumptions manually annotated.
  2. Formalization planning: An agent builds (a) a concept graph (nodes = keywords/sub-clauses, edges = IS-A, HAS-A, RELIES-ON, DEFINED-BY) and (b) a formal signature graph mapping each concept to its Lean realization with lean_kind, constructors, and embedding level (deep/shallow/mixed for DSLs, semantic predicates, and meta-theorems respectively).
  3. Lean implementation: Three-round agentic translation respecting dependency order: (1) inductive types/structures, (2) definitions/functions/examples, (3) theorem statements with sorry placeholders. After each round, lake build validates compilation.
  4. Formal correctness review: Automated sorry-filling, counterexample search (attempting to prove the negation to distinguish hard proofs from wrong statements), issue triage/decomposition by an orchestrator agent, and mandatory three-way review comparing each declaration against the textbook, signature graph, and implementation history. Human experts (≈6 person-months, 600+ tracked issues, ≈190K feedback tokens) handle vacuous formalizations, missing standing assumptions, and accumulated workarounds on false foundations.

A data engine then automatically derives five evaluation tracks from the artifact. Evaluation uses a novel DefEq Checker—a Lean program testing definitional equivalence (via isDefEq or grind) between model output and ground truth across definitions, theorems, inductives, and constructors.

Models are evaluated in three modes: zero-shot, thinking (extended reasoning), and agentic (SWE-agent-style scaffold with file read/write, lake build, and submit; up to 20 turns for IAF/IAF-D/DTP/ITP, 64 for SSAF).

Key Contributions

  • LCS-Bench: 327 textbook items → 4,076 Lean declarations, 85K LoC (28K proof lines); 86% of textbook items across chapters 3–10 formalized; 55% of theorems/lemmas fully machine-verified.
  • Semi-automated agentic pipeline: concept graph + formal signature graph + sorry-filling with counterexample search + orchestrated issue tracking + human expert intervention.
  • Data engine generating 1,271 data points across five tracks: IAF, SSAF, IAF-D, DTP, ITP.
  • DefEq Checker: novel evaluation protocol supporting definitional (not just logical) equivalence across heterogeneous Lean declaration kinds.
  • 14-model evaluation in zero-shot / thinking / agentic modes, with findings on theory-scale coherence challenges.

Results

  • IAF (item-level auto-formalization): best pass rate 20.1% (Claude Opus 4.6, agentic); weakest model 2.1%; zero-shot baseline ≈16.8% for top model.
  • Agentic mode consistently outperforms thinking, which outperforms zero-shot, but absolute numbers remain low across all modes.
  • Top proprietary models (Claude Opus 4.6, GPT-5.4) outperform others by only a small margin; correct outcomes largely overlap, reducing circular-evaluation concern.
  • IAF-D (with distractors): pass rate drop of approximately −2.7 percentage points (zero-shot) and −2.2 (agentic) relative to IAF, indicating moderate sensitivity to irrelevant context.
  • SSAF, DTP, ITP: agentic-only results reported; detailed per-model numbers shown in Figure 7 (not fully reproduced in the truncated text) but all tracks remain well below saturation.
  • Rankings are stable across three repeated runs (small SEM error bars).

Limitations

  • 45% of theorems/lemmas lack machine-verified proofs (primarily mechanically demanding meta-theorems like termination and completeness); these are validated by human experts but not formally proved.
  • Human expert effort is substantial (≈6 person-months), limiting scalability of this pipeline to new domains.
  • Pipeline relies on two specific models (Claude Opus 4.6, GPT-5.4) for construction, potentially biasing the artifact toward their stylistic conventions despite human-set naming/style guidelines.
  • Benchmark covers a single textbook; generalizability to other CS subfields or mathematical domains is unverified.
  • The DefEq Checker covers four declaration kinds; edge cases in constructor-level equivalence use only isDefEq (no grind), which may miss some valid equivalences.
  • Truncated paper text means some per-track quantitative results (SSAF, DTP, ITP pass rates) are not fully reported here.

Relevance to Agentic AI / LLM Agents

The benchmark is directly relevant to agentic AI in two ways: (1) the construction pipeline is itself a multi-agent system—an orchestrator triages issues, decomposes stuck proofs, triggers review cycles, and interleaves automated sorry-filling with counterexample search, representing a concrete case study in agentic formal-methods automation; (2) the evaluation explicitly compares zero-shot, thinking, and agentic (SWE-agent-style) modes, showing that tool-augmented agent loops provide the highest pass rates on complex formal-reasoning tasks. The low ceiling (20.1% best) positions LCS-Bench as a hard, unsaturated testbed for measuring progress in long-horizon, tool-using LLM agents that must maintain global consistency across hundreds of interdependent artifacts—a regime where current agents still fail badly. The "accumulated workarounds on a false foundation" failure mode is a particularly sharp finding about multi-step agentic coherence.