Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

Anna Mei; Michael R. Douglas

cs.LOOct 14, 2026

Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

Authors: Anna Mei, Michael R. Douglas

Organizations: Harvard University · CMSA, Harvard University and AletheAI, Inc

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: The verification workflow. A theorem is verified if it receives a semantic FAITHFUL and no numerical or vacuity FAIL .

Stage	Agent work	Gate on every theorem / equation
DAG	Enumerate equations and dependencies	Open-world gap report
Extract	Write typed definitions and theorem statements	(i) Formalized with appropriate tag or (ii) documented in DISPOSITIONS.md
Verify	Run numerical and back-translation fidelity checks	(i) Obtained a 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

Table 1: Autoformalization pipeline for FLMF.

	FLMF (182 C / 289 I)		Beyond Compilation (245 C / 106 I)		ProofNet (163 C / 204 I)
Method	Incorrect / accepted (rate)	Flagged / correct	Incorrect / accepted (rate)	Flagged / correct	Incorrect / accepted (rate)	Flagged / correct
Ours	5/105 (4.8%)	45.1%	3/154 (1.9%)	38.4%	14/153 (9.2%)	14.7%
GPT-5.5	28/178 (15.7%)	17.6%	10/227 (4.4%)	11.4%	26/176 (14.8%)	8.0%
GPT-5.5 (joint)	45/203 (22.2%)	13.2%	13/232 (5.6%)	10.6%	38/194 (19.6%)	4.3%
Opus 4.6	72/232 (31.0%)	12.1%	24/261 (9.2%)	3.3%	44/206 (21.4%)	0.6%
Opus 4.6 (joint)	88/250 (35.2%)	11.0%	42/267 (15.7%)	8.2%	56/215 (26.0%)	2.5%

Table 2: Accepted-error rate by method on the three labeled datasets. Incorrect / accepted counts the incorrect items among those a method did not flag. A lower accepted-error rate means fewer incorrect Lean formalizations after the check. Flagged / correct is the percentage of all items the method flags among those labeled “correct”. The counts under each dataset are its correct (C) and incorrect (I) items.

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
	Vacuity	23	12	1	0	10
	Combined	195	102	18	43	35
ProofNet	Numerical	85	85	0	0	0
	Semantic	203	183	1	1	17

Table 3: Flags across different datasets and reviewed defect types. Flagged counts all alerts by each method. Labeled incorrect counts alerts on items the dataset labels incorrect. Translation defects and Source defects count review findings among flagged items that the dataset labels correct. RLM25 has no correctness labels; therefore, all statements are considered “correct” by the dataset.

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

Ch.	Chapter	Targets	Extract	Verified	Proved
1	Algebraic and Analytic Methods	705	88	38	75
2	Asymptotic Approximations	349	2	1	2
3	Numerical Methods	297	2	0	2
4	Elementary Functions	518	26	14	24
5	Gamma Function	164	162	123	137
6	Exponential, Logarithmic, Sine and Cosine Integrals	100	97	56	77

Appendix

Table 4: Complete DLMF chapter progress, reported as counts.

DLMF	Printed defect and correction	Independent evidence
20.10.4	The display uses $(1+\beta)$ where scale covariance and the theta shift require $(\ell+\beta)$ . The $\theta_{1}$ transform has the opposite printed sign, and the $\theta_{1}$ and shifted $\theta_{2}$ integrals are negatives of each other, not equal.	Theta quasi-periodicity already makes the printed chain inconsistent at $\ell=1$ ; termwise Laplace transforms and independent 25-digit quadrature recover the corrected form.
20.10.5	The display uses $(1+\beta)$ where scale covariance and the theta shift require $(\ell+\beta)$ .	Termwise Laplace transforms and independent 25-digit quadrature recover the corrected form.
20.13.5	The alternating heat-kernel sum is printed as $\theta_{4}$ ; Poisson summation gives $\theta_{2}$ .	At $(\alpha,t,z)=(0.7,0.3,0.4)$ , the sum is $1.5982\ldots$ and matches $\theta_{2}$ to $1.6\times 10^{-26}$ , whereas the printed $\theta_{4}$ side is $0.3972\ldots$ ; complex samples agree.

Appendix

Table 5: DLMF misprint findings.

Dataset	Component	Correct	Incorrect
FLMF	Seeds	38	2
	Bound-variable renamings of the seeds	38	2
	Human-approved corrected forms of DLMF misprints	7
	Mutations of the seeds (M1–M8 + sanity)		160
	Historical FLMF errors		17
	Misprinted DLMF equations		7

Appendix

Table 6: Dataset composition (1,810 items).

Seeds, renamings, and corrected misprints
FLMF subset	$n$	Ours	GPT-5.5	GPT-5.5 (joint)	Opus 4.6	LeanScorer	FormalAlign	N	B	V
Seeds	40	12	8	4	3	22	37	0	9	3
Renamed seeds	40	15	7	4	4	21	36	0	12	3
Corrected misprints	7	7	7	7	6	3	1	0	7	0
Mutations, historical artifacts, and printed misprints
M1 impossible hypotheses	20	20	20	20	19	20	18	0	20	0

Appendix

Table 7: Flags on the 271 FLMF seeds, renamings, mutations, historical artifacts, and misprint items.

	FLMF (182 C / 289 I)		Beyond Compilation (245 C / 106 I)		ProofNet (163 C / 204 I)
Threshold	Incorrect / accepted	Flagged / correct	Incorrect / accepted	Flagged / correct	Incorrect / accepted	Flagged / correct
0.1	243 / 409	8.8%	100 / 338	2.9%	185 / 312	22.1%
0.2	111 / 199	51.6%	76 / 248	29.8%	81 / 120	76.1%
0.3	32 / 76	75.8%	49 / 139	63.3%	16 / 20	97.5%
0.4	12 / 22	94.5%	21 / 45	90.2%	2 / 2	100.0%
0.5	1 / 1	100.0%	3 / 8	98.0%	0 / 0	100.0%

Appendix

Table 8: FormalAlign certainty-threshold sweep on 1,189 labeled pairs. A statement is flagged when its certainty score is at most the threshold. C and I denote the dataset’s correct and incorrect labels. Incorrect / accepted counts incorrect-labeled items among accepted statements. Flagged / correct is the percentage of correct-labeled items that are flagged. The threshold of 0.3 used in the main comparison is shown in bold. The 0 / 0 entry indicates that no statements are accepted. RLM25 reference pairs are not included in this sweep.

Channel	Items	API calls	Cost (USD)	Cost / item (USD)	Time / item (s)
Numerical check	1,539	3,961	314.18	0.204	77.0
Back-translation	1,539	3,080	99.57	0.065	29.0
Vacuity check	1,539	0	0.00	0.000	–
GPT-5.5 direct	918	920	33.01	0.036	13.5
Opus 4.6 direct	918	922	20.96	0.023	14.6
LeanScorer	918	1,840	66.65	0.073	20.5

Appendix

Table 9: API cost and recorded runtime. The 918-item set comprises 200 FLMF, 351 Beyond Compilation, and 367 ProofNet statements. The 1,539-item set also includes 621 RLM25 reference pairs. Costs include retained reservations totaling $9.64 for 25 requests whose charges remain unresolved. Time per item is the sum of final recorded job durations divided by the item count, with joint-batch time amortized across items; it excludes superseded attempts and is not elapsed wall-clock time. Vacuity runtime is omitted because 1,512 records report result-reuse overhead rather than the original checking time. FormalAlign scored 918 items locally on CPU, with 32.1 minutes of recorded inference time (2.1 seconds per item), excluding model loading.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 336 papers

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
Jun 30, 2026Arshia Soltani Moakhar, Iman Gholami, Max Springer +2Multi-Agent LLM Systems Automated Theorem Proving
MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
Aug 14, 2026Lushi Pu, Weiming Zhang, Xinheng Xie +7Autoformalization Formal Verification
ModelBest Inc. · Tsinghua University
PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
Oct 22, 2026Jiyuan Tan, Vasilis Syrgkanis, Jose BlanchetAutoformalization Formal Verification
Stanford University

Jun 30, 2026J/K move · Enter open · S save

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

Arshia Soltani Moakhar, Iman Gholami, Max Springer, Mahdi JafariRaviz+1

Multi-Agent LLM Systems Automated Theorem Proving Formal Verification Lean Theorem Proving Autoformalization

Open paper AskPDF arXiv

While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on five papers from the ACM Symposium on Theory of Computing (STOC) spanning combinatorics, communication complexity, mechanism design, and learning theory, successfully formalizing their main theorems and validating the generated formalizations with human experts; for all five we also formalize the proofs alongside the statements, and notably two of them are proved with no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv .

Abstract

Formal Verification

Explore similar work

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean