Reliable Evaluation and Benchmarks for Statement Autoformalization

TL;DR

This paper introduces improved metrics, datasets, and benchmarks for evaluating statement autoformalization, enabling more reliable assessment of systems translating natural language mathematics into formal languages like Lean 4.

Contribution

It presents BEq+ and ProofNetVerif for better evaluation, along with new benchmarks ProofNet# and RLM25, to systematically measure autoformalization progress.

Findings

Current techniques achieve up to 45.1% accuracy on undergraduate math.

Systems struggle with research-level content without proper context.

The work establishes a reliable foundation for future autoformalization evaluation.

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.