# Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

> A three-layer verification stack combining semantic, numerical, and vacuity checks achieves the lowest error rates in Lean autoformalization, catching defects all LLM judges miss.

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

## Summary

# Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

## Summary (Overview)

- **Novel verification method**: The paper introduces a three-layer verification stack for Lean formalizations combining semantic (LLM-based) checks, mechanical numerical checks, and vacuity checks, going beyond pure LLM judgment.
- **Lowest accepted-error rate**: On three labeled datasets (FLMF, ProofNet, Beyond Compilation), the proposed method achieves the lowest rate of accepting incorrect formalizations (4.8%, 1.9%, and 9.2% respectively), outperforming GPT-5.5, Opus 4.6, LeanScorer, and FormalAlign.
- **Extract-Verify-Prove pipeline**: A human-gated autoformalization pipeline with auditor agents, producing the Formalized Library of Mathematical Functions (FLMF)—a partial formalization of the NIST DLMF with ~1,000 entries completed in 2 man-months.
- **Dataset corrections**: Expert review identified 2 defects in ProofNet items labeled faithful, 61 defects in Beyond Compilation correct-labeled items, and 205 defects in RLM25 that were previously undetected.
- **Key insight**: Numerical and vacuity checks catch errors missed by all LLM judges, including subtle translation defects and informal source errors (e.g., false Taylor bounds, contradictory hypotheses).

## Introduction and Theoretical Foundation

The paper addresses a critical challenge in automated mathematical formalization: **reliability**. While Mathlib (The mathlib Community, 2020) guarantees correctness through careful human review, its slow review process limits coverage. Agentic autoformalization systems (Gloeckle et al., 2026; Rammal et al., 2026; Wang et al., 2026) can scale formalization but face severe reliability challenges—an autoformalizer can change domains, indices, signs, or branch conventions while still producing provable statements.

The authors argue that existing verification methods fall into two categories:
- **Reference-based metrics** (BEq, GTED, ASSESS): Require a reference formal statement, limiting applicability to natural language formalization.
- **Reference-free methods** (FormalAlign, LeanScorer, Beyond Compilation): Rely solely on LLM judgments, which are ambiguous and arbitrary.

The theoretical foundation rests on the observation that **no single check establishes faithfulness**—each has a distinct failure model. The authors propose treating verification as a *stack* where each layer adds independent assurance.

## Methodology

### Verification Method (Three-Layer Stack)

**1. Semantic Check (LLM-based)**
- **Direct inspection**: An LLM judge (GPT-5.5) evaluates whether the Lean statement faithfully translates the informal statement.
- **Back-translation check**: A translator agent (Gemini 3.1 Pro) reads the Lean statement and definitions *without comments* (reducing hallucination risk), producing a structured English rendering:
  - STATEMENT, VARIABLES, CONSTRAINTS, SYMBOLS
- A second judge compares this rendering against the DLMF source with a `STANDING_CONSTRAINTS.md` document.
- Verdicts: FAITHFUL, DIVERGE, or UNCERTAIN.

**2. Numerical Check (Mechanical)**
- A mechanical extractor translates the Lean theorem into evaluations in `mpmath` (arbitrary-precision Python library).
- Special functions are bound to mpmath counterparts with appropriate conventions.
- The checker samples points from the stated domain and compares function values:
  - Exact identities use **residual gates**
  - Asymptotics use **ratio or rate gates**
- Trustworthiness of Lean-mpmath binding ensured by requiring each special function is defined only once, with binding attached to the definition.

**3. Vacuity Check**
- Scans theorem statement and proof body for empty statements.
- Tests whether trivial proof methods (rfl, simp) close the goal.
- **Goal-independent proof detection**: Replaces the target goal with an opaque conclusion `VacQ` and checks if the proof still compiles. If it does, the proof is goal-independent—likely from contradictory hypotheses (from which False can be derived).

### Autoformalization Pipeline

The pipeline proceeds in three stages with human gates at each:

| Stage | Agent Work | Gate on every theorem/equation |
|-------|-----------|-------------------------------|
| **Extract** | Write typed definitions and theorem statements | (i) Formalized with tag or (ii) documented in DISPOSITIONS.md |
| **Verify** | Run numerical and back-translation fidelity checks | (i) Verified stamp or (ii) documented in HUMAN_REVIEW.md |
| **Prove** | Fill frozen theorem bodies in waves | (i) Proved with clean build and 0 sorry or (ii) documented in UNPROVEN.md |

**Key components**:
- **DAG** (Directed Acyclic Graph) tracking dependencies between DLMF chapters/equations
- Each extracted theorem carries 4 tags: DLMF equation number, Fidelity check method, Verification status, DAG node
- **Auditor agents** inspect human review documents, make simple fixes, and provide analysis for hard issues
- Corrections logged in an **ERRATA file** for error analysis

### Example Formalized Statement (DLMF 5.5.3)

```lean
/- **DLMF 5.5.3** -- Γ(s)Γ(1 − s) = π/sin(πs) (complex)
(DLMF-faithful restriction of 'complex_reflection': s ≠ 0, ±1, ±2, . . .).
DAG: E-5.5.3.
Fidelity: numeric PASS
Verified: verified
-/
theorem complex_reflection_dlmf
    (s : ℂ)
    (_hs : ∀ m : ℤ, s ≠ (m : ℂ)) :
    Complex.Gamma s * Complex.Gamma (1 - s) =
      (Real.pi : ℂ) / Complex.sin ((Real.pi : ℂ) * s) := by
  sorry
```

## Empirical Validation / Results

### Experimental Setup

- **1,810 informal–formal pairs** from four datasets:
  - **FLMF**: 471 statements (182 correct / 289 incorrect) from DLMF formalization, combining library statements, mutations, historical errors, and misprint pairs
  - **ProofNet**: 371 problems (163 correct / 204 incorrect) with Ground False faithfulness verdicts
  - **Beyond Compilation**: 351 problems (245 correct / 106 incorrect) with GPT-5.2 judge labels
  - **RLM25**: 621 reference pairs (no correctness labels, all treated as correct)

### Main Results: Accepted-Error Rates

| Method | FLMF (182C/289I) | Beyond Compilation (245C/106I) | ProofNet (163C/204I) |
|--------|-------------------|-------------------------------|----------------------|
| **Ours** | **5/105 (4.8%)** | **3/154 (1.9%)** | **14/153 (9.2%)** |
| GPT-5.5 | 28/178 (15.7%) | 10/227 (4.4%) | 26/176 (14.8%) |
| GPT-5.5 (joint) | 45/203 (22.2%) | 13/232 (5.6%) | 38/194 (19.6%) |
| Opus 4.6 | 72/232 (31.0%) | 24/261 (9.2%) | 44/206 (21.4%) |
| Opus 4.6 (joint) | 88/250 (35.2%) | 42/267 (15.7%) | 56/215 (26.0%) |
| LeanScorer | 10/93 (10.8%) | 7/175 (4.0%) | 17/135 (12.6%) |
| FormalAlign (≤0.3) | 32/76 (42.1%) | 49/139 (35.3%) | 16/20 (80.0%) |

**Key finding**: Our method achieves the **lowest accepted-error rate** on all three datasets. While flagging rate is higher, false alarms are acceptable given auditing agent support.

### Audit Results on External Datasets

| Dataset | Check | Flagged | Labeled incorrect | Translation defects | Source defects | False alarm |
|---------|-------|---------|-------------------|-------------------|---------------|-------------|
| Beyond Compilation | Numerical | 76 | 35 | 8 | 37 | 0 |
| | Semantic | 151 | 101 | 15 | 12 | 25 |
| | Combined | 195 | 102 | 18 | 43 | 35 |
| ProofNet | Numerical | 85 | 85 | 0 | 0 | 0 |
| | Semantic | 203 | 183 | 1 | 1 | 17 |
| | Combined | 208 | 186 | 1 | 1 | 19 |
| RLM25 | Numerical | 12 | n/a | 7 | 0 | 4 |
| | Semantic | 367 | n/a | 184 | 21 | 143 |
| | Combined | 373 | n/a | 184 | 21 | 149 |

**Notable**: In Beyond Compilation, **all 41 statements flagged by the numerical check yet labeled correct turn out to contain real defects**—highlighting the mechanical check's unique power.

### Case Study 1: Vacuity Check Catches Contradictory Hypotheses

DLMF §7.13.5 describes Fresnel integral zeros ordered by **increasing absolute value**. The Lean formalization instead imposed:

```lean
(hmono : StrictMono (fun n ↦ (z n).re))
(hall : ∀ w : ℂ, cfresnelC w = 0 → 0 < w.re → 0 < w.im → ∃ n, z n = w)
```

The hypotheses are **contradictory**: large-index zeros approach the real axis, and mirror symmetry gives first-quadrant zeros with arbitrarily small positive real parts, violating monotonicity. False can be derived, making the theorem vacuously true. **All baseline methods accepted this as correct**; only the vacuity check detected the problem.

### Case Study 2: Numerical Check Catches False Taylor Bound

A Beyond Compilation statement claimed: if f is holomorphic on a neighborhood of the closed unit disk and f(0) ≠ 0, then:

$$\exists C \in \mathbb{R},\ \forall m \in \mathbb{N},\ \forall z,\ |z| \leq 1: \left|\;1 - \sum_{k=0}^{m} \frac{f^{(k)}(0)}{k!\, f(0)} z^k\;\right| \leq C |z|^{m+1}$$

The numerical check found the counterexample $f(z) = e^z$ with m = 1:
$$|1 - (1+z)| = |z| \leq C|z|^2 \implies C \geq 1/|z|$$
which no constant can satisfy as $z \to 0$. **Only the numerical check flagged this**—all LLM-based methods accepted it.

## Theoretical and Practical Implications

### Implications for Autoformalization Verification

1. **LLM judgments are necessary but insufficient**: The paper demonstrates that LLM judges consistently miss subtle mathematical defects, including impossible uniform bounds and contradictory hypotheses. Mechanical checks provide complementary, reproducible evidence.

2. **Checkable feedback matters**: Unlike LLM verdicts, numerical checks point to exact misalignments, and vacuity checks reveal proof inconsistencies. This tractable feedback enables agent repair and human review.

3. **Source defects are common**: The audit found 205 defects in RLM25 and 61 in Beyond Compilation—many flagged exclusively by numerical checks—suggesting existing benchmarks contain more errors than previously recognized.

### Practical Implications

- **FLMF progress**: Chapter 5 (Gamma Function), 7 (Error Functions), and 20 (Theta Functions) are essentially complete. Overall: 1,326/8,833 (15%) DLMF equations stated, 641 (7%) verified, 1,142 with sorry-free proofs.
- **DLMF misprints identified**: Three confirmed DLMF misprints (20.10.4, 20.10.5, 20.13.5) with independent numerical evidence, confirmed by the DLMF committee.
- **Pipeline economics**: ~$0.20/item for numerical checks, ~$0.065/item for back-translation; cost-effective at scale.

### Limitations

- Numerical checks only apply to numerically evaluable statements (not definitions, limits, infinite sums).
- Vacuity checks require completed proofs.
- Common failure mode: narrower domain in Lean statement vs. informal source.
- Passing checks doesn't guarantee correctness, but ensures numerical consistency and non-vacuity.

## Conclusion

The paper introduces a **verification stack** combining semantic, numerical, and vacuity checks that achieves the lowest accepted-error rate among evaluated methods across three labeled datasets. The Extract-Verify-Prove pipeline with human gates and auditor agents enables trustworthy, large-scale autoformalization—demonstrated by FLMF's ~1,000 DLMF entries in 2 man-months.

**Future work** will:
- Extend numerical and vacuity checks to additional corner cases
- Reduce vacuity false alarms by distinguishing contradictory assumptions from legitimate definitional identities
- Explore additional mechanical checks for independently checkable evidence

The authors emphasize that checks are strict by design: *"we would rather have them flag a correct statement than miss an incorrect one."*

---

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