# Reliable Evaluation and Benchmarks for Statement Autoformalization

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

## Key facts

- Cited by 32 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 33 references that are in the map.
- First posted on arXiv 11 Jun 2024.

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

- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [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)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [V-STaR: Training Verifiers for Self-Taught Reasoners](https://mlsanity.com/paper/2402.06457/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)

## Built on by (most cited first, 30 of 32)

- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [M2F: Automated Formalization of Mathematical Literature at Scale](https://mlsanity.com/paper/2602.17016/) (2026)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [FormaRL: Enhancing Autoformalization with no Labeled Data](https://mlsanity.com/paper/2508.18914/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [Theory-Scale Auto-Formalization of Logics for Computer Science](https://mlsanity.com/paper/2606.26525/) (2026)
- [SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization](https://mlsanity.com/paper/2608.29270/) (2026)
- [LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization](https://mlsanity.com/paper/2607.20503/) (2026)
- [Discovering New Theorems via LLMs with In-Context Proof Learning in Lean](https://mlsanity.com/paper/2509.14274/) (2025)
- [Conjecturing: An Overlooked Step in Formal Mathematical Reasoning](https://mlsanity.com/paper/2510.11986/) (2025)
- [FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models](https://mlsanity.com/paper/2608.20153/) (2026)
- [Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization](https://mlsanity.com/paper/2604.16347/) (2026)
- [Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization](https://mlsanity.com/paper/2604.23135/) (2026)
- [Benchmarking Testing in Automated Theorem Proving](https://mlsanity.com/paper/2604.23698/) (2026)
- [Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery](https://mlsanity.com/paper/2606.08728/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures](https://mlsanity.com/paper/2607.27709/) (2026)
- [FVSpec: Real-World Property-Based Tests as Lean Challenges](https://mlsanity.com/paper/2606.01008/) (2026)
- [Lean-GAP: A Dataset of Formalized Graduate Algebra Problems](https://mlsanity.com/paper/2606.02588/) (2026)
- [Evaluating the Robustness of Proof Autoformalization in Lean 4](https://mlsanity.com/paper/2606.14867/) (2026)
- [Sage: Formalization with Semantic Correction](https://mlsanity.com/paper/2609.35790/) (2026)
- [Objects Without Morphisms: What LLMs for Mathematics Do Not Represent](https://mlsanity.com/paper/2610.03551/) (2026)
- [AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness](https://mlsanity.com/paper/2610.05367/) (2026)
- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)
- [Aligning Faithfulness for Theory-Scale Autoformalization](https://mlsanity.com/paper/2610.18498/) (2026)

## Abstract (arXiv)

Evaluating statement autoformalization, translating natural language mathematics into formal languages like Lean 4, remains a significant challenge, with few metrics, datasets, and standards to robustly measure progress. In this work, we present a comprehensive approach combining improved metrics, robust benchmarks, and systematic evaluation, to fill this gap. First, we introduce BEq+, an automated metric that correlates strongly with human judgment, along with ProofNetVerif, a new dataset for assessing the quality of evaluation metrics, containing 3,752 annotated examples. Second, we develop two new autoformalization benchmarks: ProofNet#, a corrected version of ProofNet, and RLM25, with 619 new pairs of research-level mathematics from six formalization projects. Through systematic experimentation across these benchmarks, we find that current techniques can achieve up to 45.1% accuracy on undergraduate mathematics but struggle with research-level content without proper context. Our work establishes a reliable foundation for evaluating and advancing autoformalization systems.