Definition Grounding in Theory-Level Auto-formalization

Summary (Overview)

• The paper introduces definition grounding, a framework for continuously evaluating and revising formalized definitions to ensure they remain usable (compatible) with downstream mathematical statements in theory-level auto-formalization.
• The authors curate ReuseBench, a benchmark with 8 mathematical theories (102 definitions, 410 downstream statements across 5 difficulty layers) to evaluate whether LLM agents produce reusable, idiomatic Lean 4 formalizations.
• Key finding: Only 25%–50% of LLM-generated definition formalizations (from raw textbook text) are compatible with all downstream statements; however, cleaning informal definitions improves this to 77.5% on average.
• LLM judges can predict definition incompatibility with 85% accuracy when given basic downstream formalizations ($S_1$), at only ~11% of the definition formalization cost.
• The work addresses a critical gap: existing benchmarks evaluate theorem proving, but not the reusability of definitions—which is essential for building extensible formalized mathematical libraries.

---

Introduction and Theoretical Foundation

Background and Motivation

AI systems now generate mathematical results faster than humans can verify. Formal verification in Lean 4 is increasingly important, but large-scale auto-formalizations are often:

• Overly convoluted and unrefactored
• Hard to use in downstream formalization projects
• Built on definitions that are subtly unfaithful or too narrow

The paper highlights a critical failure point: definition quality. In theory-level auto-formalization, a formalized theory library is built layer by layer:

$$\dot{C}_{i+1} \sim \mathcal{A}(S_i \mid \dot{C}_i)$$

where each layer $S_i$ builds on previous ones. If a definition is incompatible with later statements, refactoring it requires modifying everything built on top of it.

Key Terminology

• Informal: Natural-language mathematical statements (textbooks, papers)
• Formal: Verified Lean 4 code
• Theory-level auto-formalization: Formalizing a new mathematical field from its core definitions upward
• Downstream statements: Statements that use a definition (in their statement or proof)
• Definition grounding: The process of producing and maintaining definition formalizations that later layers can be built on

Related Work

The paper contrasts with prior work:

• Zhang et al. (2025) and MathAtlas evaluate whether definitions are correct; ReuseBench tests whether later statements can be built on them.
• APE-Bench and MathlibPR study LLM judges for Lean code; this work focuses specifically on definition quality.
• Software engineering parallels (SlopCodeBench, SWE-CI, MaintainBench) show that agent-written code degrades maintainability—analogous to formalization reusability.

---

Methodology

Problem Formulation

The paper formalizes theory-level autoformalization as an iterative process:

1. Agent $\mathcal{A}$ generates $\dot{C}_{i+1} \sim \mathcal{A}(S_i \mid \dot{C}_i)$
2. LLM judge $J : \dot{\mathcal{C}} \to \mathbb{B}$ predicts compatibility: $J(\dot{C}_{i+1}) \in \mathbb{B}$
3. If $J(\dot{C}_{i+1}) = \text{False}$, refactor/re-generate until True
4. Proceed to next iteration

ReuseBench Dataset

Structure: Each theory contains layers labeled $D, S_1, \ldots, S_5$:

Selection criteria:

• Theories must be adjacent to (but not fully in) Mathlib
• Definitions must be non-trivial and not already formalized
• All statements are self-contained (cleaned to remove implicit assumptions)

Experimental Setup

Definition generation: 5 frontier models (GPT 6 Astra, GPT 5.6 Sol, Claude Fable 5.1, Claude Opus 5, Claude Sonnet 5) generate definition candidates under two conditions:

• Source: Verbatim textbook text
• Cleaned: Restated, self-contained definitions

Compatibility measurement: A canonical agent (GPT 5.6 Sol) formalizes downstream statements. If it must write wrappers, revise definitions, or formalize unfaithfully, the statement is a witness against the definition.

Key metrics:

• Compatibility label: $L(\dot{D} \mid S_1, \ldots, S_i) \in \mathbb{B}$ — True if no witness exists
• Witness rate: Fraction of statements in layer $S_i$ that are witnesses
• Full pass rate: Fraction of definition formalizations with $L(\dot{D}) = \text{True}$ over all layers

---

Empirical Validation / Results

Q1: How often are definitions incompatible with downstream statements?

Table 2: Witness rate and full pass rate of definition formalizations

Key findings:

• With source text, only 25–50% of definition formalizations pass all downstream layers
• Incompatibility surfaces late: witness rates remain high at $S_3$–$S_5$ (11–13%), meaning costly refactoring would occur deep in the formalization process
• Cleaned data dramatically improves compatibility: full pass rate rises to 77.5% average (100% for Claude Fable 5.1)

Q2: Can model judges predict downstream compatibility?

Table 3: Judge performance against compatibility label $L(\dot{D})$

Key findings:

• The definition-only judge $J_0$ improves precision from 62% to 78% (filtering by majority of 5 votes removes 21 of 30 incompatible formalizations)
• All judges beat the baseline (always True) in AUC and precision

Q3: Do downstream formalizations help judges?

Key findings:

• Adding formalized $S_1$ (basic properties) improves accuracy from 0.65 → 0.85 and AUC from 0.79 → 0.85
• Further downstream evidence ($S_2$–$S_4$) does not substantially improve predictions
• The cost of $J_1$ (formalizing $S_1$ + 5 judge calls) is only 11% of the definition formalization cost

---

Theoretical and Practical Implications

Theoretical Significance

1. Definition grounding as a formal framework: The paper formalizes the iterative process of definition evaluation and revision, providing a theoretical foundation for quality control in auto-formalization.

2. Quantification of the "definition problem": Prior work noted definition quality issues anecdotally (e.g., 1/62 definitions usable in Ilin & Nugent 2026); this paper provides systematic measurement across 8 theories.

3. Late-surfacing incompatibility: The finding that witness rates remain high at $S_3$–$S_5$ demonstrates that definition issues are not caught by early formalization—they compound over time.

Practical Implications

1. Cost-effective quality control: Formalizing basic properties ($S_1$) and using an LLM judge provides a low-cost (11%) early warning system for definition incompatibility.

2. Textbook cleaning is essential: Raw textbook text is often unsuitable for direct formalization; cleaned statements improve compatibility from 40% to 77.5% full pass rate.

3. Benchmark for future work: ReuseBench provides a standardized evaluation for theory-level auto-formalization, enabling comparison of agents and judge models.

4. Agent design guidance: Auto-formalization systems should incorporate:

   • Definition cleaning/restatement
   • Basic property formalization as a validation step
   • LLM judge-based filtering with downstream evidence

---

Conclusion

Main Takeaways

1. LLM-generated definitions frequently fail downstream reusability: Only 25–50% of source-based definition formalizations are fully compatible with all downstream statements.

2. Definition grounding works: A judge given basic downstream formalizations ($S_1$) can identify 73% of incompatible definitions at ~11% of the definition formalization cost.

3. Cleaned informal text is critical: Clarifying definitions improves full pass rate to 77.5% (up to 100% for the best model).

4. Early detection prevents costly refactoring: Since incompatibilities surface late (high witness rates at $S_3$–$S_5$), early filtering is essential to avoid cascading refactoring costs.

Future Directions

• Extending ReuseBench: The benchmark can be extended to more theories and fields
• Automated definition revision: Beyond judging, developing agents that automatically revise incompatible definitions
• Integration with proof formalization: Investigating how definition quality interacts with proof complexity
• Better cleaning methods: Developing automated approaches to clean informal definitions for formalization
• Multi-layer grounding: Studying whether grounding at intermediate layers (not just definitions) improves overall library quality

The paper establishes that definition grounding—continuous evaluation and revision of formalized definitions using downstream evidence—is both necessary and cost-effective for scalable, high-quality theory-level auto-formalization.