RLMEval: Evaluating Research-Level Neural Theorem Proving

TL;DR

RLMEval is a new evaluation suite designed to assess the performance of neural theorem proving models on complex, research-level mathematics, revealing a significant gap between benchmark results and real-world applicability.

Contribution

The paper introduces RLMEval, a challenging benchmark based on real-world Lean formalizations, to better evaluate neural theorem proving in research-level mathematics.

Findings

State-of-the-art models achieve only 10.3% pass rate on RLMEval.

Existing benchmarks do not reflect the difficulty of research-level theorems.

RLMEval highlights the need for improved models for formal mathematics.

Abstract

Despite impressive results on curated benchmarks, the practical impact of large language models (LLMs) on research-level neural theorem proving and proof autoformalization is still limited. We introduce RLMEval, an evaluation suite for these tasks, focusing on research-level mathematics from real-world Lean formalization projects. RLMEval targets the evaluation of neural theorem proving and proof autoformalization on challenging research-level theorems by leveraging real Lean Blueprint formalization projects. Our evaluation of state-of-the-art models on RLMEval, comprising 613 theorems from 6 Lean projects, reveals a significant gap: progress on existing benchmarks does not readily translate to these more realistic settings, with the best model achieving only a 10.3 % pass rate. RLMEval provides a new, challenging benchmark designed to guide and accelerate progress in automated reasoning for formal mathematics.