# Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

arXiv: https://arxiv.org/abs/2610.20573 · HTML: https://mlsanity.com/paper/2610.20573/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 24 of its 55 references that are in the map.
- First posted on arXiv 14 Oct 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 24 of 24)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics](https://mlsanity.com/paper/2505.03171/) (2025)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [Formalizing Mathematics at Scale](https://mlsanity.com/paper/2605.29955/) (2026)
- [Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization](https://mlsanity.com/paper/2606.31002/) (2026)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [RLMEval: Evaluating Research-Level Neural Theorem Proving](https://mlsanity.com/paper/2510.25427/) (2025)
- [Formalization of QFT](https://mlsanity.com/paper/2603.15770/) (2026)
- [LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization](https://mlsanity.com/paper/2607.20503/) (2026)
- [Benchmarking Testing in Automated Theorem Proving](https://mlsanity.com/paper/2604.23698/) (2026)

## Abstract (arXiv)

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.