Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization
Autoformalization pipelines translate natural mathematical text into theorem-prover code, but current verification relies on LLM judges that miss subtle domain and sign errors. This paper proposes a layered faithfulness verifier that stacks semantic LLM review with mechanical numerical and vacuity checks, and deploys it within an Extract–Verify–Prove pipeline to build the Formalized Library of Mathematical Functions. On three labeled benchmarks the method achieves the lowest accepted-error rate, while also uncovering hundreds of defects in existing datasets.
The paper presents a well-motivated and practically oriented solution to a genuine bottleneck in autoformalization: LLM-generated Lean statements can be provable yet mathematically wrong. By combining back-translation, direct LLM inspection, numerical sampling via mpmath bindings, and a proof-vacuity test, the authors obtain a conservative gate that deliberately errs toward flagging rather than silently accepting errors. The empirical gains over GPT-5.5, Opus 4.6, LeanScorer, and FormalAlign are clear on the accepted-error metric, but the approach demands considerable human review overhead and its coverage is inherently limited to numerically evaluable identities and completed proofs.
The strongest contributions are the concrete case studies and the cross-method empirical comparison. The Fresnel-zeros example shows a genuinely subtle defect—contradictory hypotheses rendered the theorem vacuous—that every LLM baseline and the semantic checker missed, while the Taylor-bound example from Beyond Compilation exposes an incorrect informal source that only numerical sampling caught. Table 2 shows the proposed stack achieves accepted-error rates of 4.8%, 1.9%, and 9.2% on FLMF, Beyond Compilation, and ProofNet, compared to 15.7%–42.1% for baselines. The audit in Table 3 further validates that numerical flags have high precision: in Beyond Compilation, all 41 numerically flagged statements labeled “correct” turned out to contain real defects.
The most significant limitation is scalability: because the stack is deliberately conservative, flagging rates on correct statements reach 14.7%–45.1%, forcing extensive human gating at each pipeline stage. The authors acknowledge that numerical checks cannot detect domain mismatches if sampling misses isolated singularities, and that vacuity detection is evadable by subtly goal-dependent proofs. Moreover, the benchmark labels themselves are noisy; several items accepted as incorrect by the method were actually mislabeled, complicating the interpretation of accepted-error rates. The reliance on unreleased infrastructure and a partially public codebase also limits immediate adoption.
The evidence supports the core claim that mechanical checks catch errors missed by LLM judges, particularly for special-function identities. The comparison is fair in that every method sees the same informal–formal pairs, and the proposed stack combines existing ideas rather than relying on a single new model. However, the baselines are not directly comparable in coverage: vacuity checks require proofs unavailable in ProofNet and Beyond Compilation, and numerical checks do not apply to definitions, limits, or asymptotic-rate statements. Because the datasets contain mislabeled correct items, the ground-truth accepted-error rates are likely underestimates for methods that flag more aggressively, which partially confounds the ranking.
Partial code is released for Chapter 7, but the full FLMF library and the exact mpmath binding specifications are not yet public, which blocks full independent reproduction. Appendix F provides useful API cost and timing estimates, yet critical hyperparameters—random seeds for numerical point sampling, the exact prompts for the LLM judges, and the VacQ implementation—are not documented. The stated models (GPT-5.5 and Gemini 3.1 Pro) do not correspond to currently available APIs, making exact reproduction of the semantic-check pipeline impossible without substituting different models. The vacuity checker requires a working Lean 4 compilation environment and the ability to replace goals with an opaque constant, which is described conceptually but not packaged as a standalone tool.
We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.
Pick a starting point or write your own. Challenges run in the background, so you can keep reading while the AI investigates.
No challenges yet. Disagree with the review? Ask the AI to revisit a specific claim.