# Definition Grounding in Theory-Level Auto-formalization

> LLM-generated Lean 4 definitions from raw textbook text fail downstream reusability 50-75% of the time, but cleaning informal text and LLM-judge screening with basic properties raises compatibility to 77.5% at 11% of formalization cost.

- **Source:** [arXiv](https://arxiv.org/abs/2610.19223)
- **Published:** 2026-10-17
- **Permalink:** https://picx.dev/p/Uj7MPq
- **Whiteboard:** https://picx.dev/p/Uj7MPq/image

## Summary

# 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$:

| Layer | Content |
|-------|---------|
| $D$ | Foundational definitions |
| $S_1$ | Basic properties of definitions |
| $S_2$ | Textbook exercises, slightly advanced properties |
| $S_3$ | Intermediate lemmas toward core results |
| $S_4$ | Core results of the theory |
| $S_5$ | Research-level results (from papers) |

**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**

| Model | $S_1$ | $S_2$ | $S_3$ | $S_4$ | $S_5$ | Full pass rate (%) |
|-------|-------|-------|-------|-------|-------|-------------------|
| **Source** | | | | | | |
| GPT 6 Astra | 6.3 | 18.1 | 10.8 | 11.7 | 15.2 | 43.8 |
| GPT 5.6 Sol | 5.2 | 18.0 | 14.1 | 16.9 | 19.2 | 31.2 |
| Claude Fable 5.1 | 4.8 | 10.3 | 5.6 | 6.2 | 3.8 | 50.0 |
| Claude Opus 5 | 5.5 | 6.5 | 6.2 | 9.0 | 6.9 | 50.0 |
| Claude Sonnet 5 | 10.1 | 22.3 | 19.6 | 16.1 | 18.8 | 25.0 |
| **All models** | **6.4** | **15.0** | **11.3** | **12.0** | **12.8** | **40.0** |
| **Cleaned** | | | | | | |
| GPT 6 Astra | 0.0 | 1.0 | 0.9 | 0.0 | 2.5 | 81.2 |
| GPT 5.6 Sol | 2.0 | 3.4 | 3.6 | 5.8 | 10.0 | 75.0 |
| Claude Fable 5.1 | 0.0 | 0.0 | 0.0 | 0.0 | 0.0 | 100.0 |
| Claude Opus 5 | 0.4 | 2.5 | 0.0 | 0.0 | 0.0 | 87.5 |
| Claude Sonnet 5 | 8.8 | 13.8 | 11.9 | 12.8 | 25.2 | 43.8 |
| **All models** | **2.2** | **4.1** | **3.3** | **3.7** | **7.5** | **77.5** |

**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})$**

| Metric | Baseline | $D(J_0)$ | $+S_1(J_1)$ | $+S_2(J_2)$ | $+S_3(J_3)$ | $+S_4(J_4)$ |
|--------|----------|----------|-------------|-------------|-------------|-------------|
| Accuracy | 0.62 | 0.65 | **0.85** | 0.82 | 0.82 | 0.81 |
| AUC | 0.62 | 0.79 | 0.85 | 0.85 | 0.84 | **0.87** |
| Precision | 0.62 | 0.78 | **0.86** | 0.82 | 0.86 | 0.86 |
| Formalization cost (USD) | – | $4.32 | $0.27 | $0.30 | $0.24 | $0.26 |
| Judge cost (5 repeats) | – | $0.17 | $0.21 | $0.27 | $0.32 | $0.35 |

**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.

---

_Markdown view of https://picx.dev/p/Uj7MPq, served by PicX — AI-generated visual whiteboard summaries of research papers._