# Reliable Evaluation and Benchmarks for Statement Autoformalization

Article · Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut

- Archive id: arxiv:2406.07222
- Published: 2024-06-11
- Venue: Conference on Empirical Methods in Natural Language Processing (EMNLP)
- DOI: https://doi.org/10.18653/v1/2025.emnlp-main.907
- arXiv: https://arxiv.org/abs/2406.07222
- Citations: 1
- Source URL: https://arxiv.org/abs/2406.07222
- PDF: https://arxiv.org/pdf/2406.07222
- Provenance: arxiv

## Abstract

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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.