TLDR: RLMEval is a new evaluation suite designed to assess the performance of large language models (LLMs) in neural theorem proving and proof autoformalization on complex, research-level mathematics. Unlike existing benchmarks, RLMEval uses ‘blueprint theorems’ from real-world Lean formalization projects, revealing a significant performance gap where even state-of-the-art models achieve only a 10.3% pass rate. This benchmark aims to guide LLM development towards more practical utility in formal mathematics.
Large language models (LLMs) have shown impressive capabilities in various tasks, including automated reasoning and theorem proving. However, a new research paper introduces a benchmark that suggests their practical impact on complex, research-level mathematics is still quite limited. This new evaluation suite, called RLMEval, aims to provide a more realistic and challenging testbed for these advanced AI systems.
The Challenge of Research-Level Mathematics
Traditional benchmarks for neural theorem proving (NTP) and proof autoformalization, such as MiniF2F and ProofNet, have seen LLMs achieve high success rates. While valuable, these benchmarks often suffer from issues like saturation (models performing too well), inaccuracies, or a focus on competition-style problems that don’t fully capture the intricacies of real-world mathematical research. This means that a model performing well on these benchmarks might not be genuinely useful in assisting mathematicians with ongoing, complex formalization projects.
Introducing RLMEval: A New Standard
To address this gap, researchers Auguste Poiroux, Antoine Bosselut, and Viktor Kunčak from EPFL, Switzerland, developed RLMEval. This benchmark focuses specifically on “blueprint theorems” – significant, high-level results from actual Lean 4 formalization projects. These are the core conceptual advances in mathematics, unlike the more numerous, simpler auxiliary lemmas that often make up the bulk of theorems in Lean projects. By concentrating on these challenging blueprint theorems, RLMEval offers a more demanding and realistic evaluation for LLMs.
The benchmark includes 613 theorems from six different Lean projects, covering diverse mathematical domains like Analysis, Number Theory, and Combinatorics. RLMEval is also designed to be extensible and will be updated annually with new Lean projects to ensure its relevance and mitigate data contamination risks.
How RLMEval Works
RLMEval evaluates models on two primary tasks: Neural Theorem Proving (NTP), where a model generates a verifiable Lean proof from a formal statement, and Proof Autoformalization, where it generates a verifiable Lean proof from both an informal (natural language) proof and its formal statement.
To assess models under varying conditions, RLMEval uses two evaluation modes:
Easy mode: Models have access to all definitions and lemmas from the source project, including auxiliary lemmas not part of the informal blueprint.
Normal mode: Models only have access to blueprint theorems, simulating a more realistic scenario where mathematicians might need to prove intermediate results themselves.
Key Findings: A Significant Performance Gap
The evaluation of state-of-the-art LLMs on RLMEval revealed a stark contrast to their performance on existing benchmarks. For instance, DeepSeek-Prover-V2-7B, one of the best-performing models, achieved only a 10.3% pass rate on proof autoformalization in “normal” mode. This is significantly lower than its reported 75%+ on MiniF2F, even with a smaller sampling budget. This highlights that current models struggle considerably with the complexity of research-level mathematics in real-world contexts.
Other notable findings include:
Models consistently performed better in “easy” mode, indicating the critical role of auxiliary lemmas. Access to these intermediate results improved performance by up to 6%.
Providing an informal proof offered only a modest benefit (around 1.5 percentage points improvement for DeepSeek-Prover-V2-7B in normal mode), suggesting that current models can leverage informal proofs to some extent, but the benefit is limited for complex problems.
Performance varied greatly across projects, with FLT3 (Fermat’s Last Theorem for n=3) yielding higher success rates (up to 32.1%) and Carleson (Analysis) proving much more challenging (max 2.73%). This suggests that mathematical domain and formalization style significantly impact model effectiveness.
While increasing the number of generated proof attempts (sampling) improved pass rates, the gains diminished, unlike on simpler benchmarks where aggressive sampling led to substantial improvements.
Successful model-generated proofs were significantly shorter than human-written ones (averaging 2.5–6.0 lines compared to 16.6 lines for humans). This suggests models primarily succeed on theorems that admit concise proof strategies, which are often the easier problems within RLMEval.
Also Read:
- New Benchmark Reveals LLMs’ Ongoing Struggle with Advanced High School Math
- Formalizing College Physics: A New Framework for AI Reasoning in Lean4
Looking Ahead
The RLMEval benchmark establishes a new, more realistic standard for evaluating neural theorem provers in mathematical settings. The significant performance gap observed underscores that while LLMs have made impressive strides, they are still far from reliably handling the complexities of ongoing formalization efforts in research-level mathematics. Future research directions include developing enhanced techniques for lemma discovery, improving context retrieval strategies, and finding better ways to leverage informal proofs.
For more detailed information, you can read the full research paper: RLMEval: Evaluating Research-Level Neural Theorem Proving.
