RLMEval: Evaluating Research-Level Neural Theorem Proving

• URL: http://arxiv.org/abs/2510.25427v1
• Date: Wed, 29 Oct 2025 11:49:49 GMT
• Title: RLMEval: Evaluating Research-Level Neural Theorem Proving
• Abstract summary: We introduce RLMEval, an evaluation suite for research-level mathematics from real-world Lean formalization projects.<n>Our evaluation of state-of-the-art models on RLMEval, comprising 613 theorems from 6 Lean projects, reveals a significant gap.<n> RLMEval provides a new, challenging benchmark designed to guide and accelerate progress in automated reasoning for formal mathematics.
• Score: 18.42453100491575
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• INSPIRE: An Internalize-Then-Improve Approach for Example-Driven Mathematical Reasoning [61.60016491769943]
  In human mathematics education, example-based reasoning such as constructing counterexamples to test theorem boundaries reflects deep conceptual understanding.<n>We propose INSPIRE, an Internalize-Then-Improve approach combining Reference-Guided Student Internalization (RGSI) with a stage-wise preference training strategy.<n>Experiments across multiple model scales and families demonstrate consistent improvements, even surpassing larger open-source models.
  arXiv  Detail & Related papers  (2026-08-27T03:24:03Z)
• LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics [5.676144562388248]
  We present a new approach for benchmarking Large Language Model capabilities on research-level mathematics.<n>Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research.<n>Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics.
  arXiv  Detail & Related papers  (2026-02-27T16:52:52Z)
• Prioritize the Process, Not Just the Outcome: Rewarding Latent Thought Trajectories Improves Reasoning in Looped Language Models [0.0]
  We introduce RLTT (Reward Latent Thought Trajectories), a reinforcement learning framework which distributes reward across the full latent reasoning trajectory.<n> RLTT yields substantial improvements over GRPO on challenging mathematical reasoning benchmarks, improving accuracy by +14.4% on MATH-500, +16.6% on AIME24, and +10.0% on BeyondAIME.<n>Despite being trained exclusively on mathematics, RLTT also transfers effectively to non-mathematical reasoning benchmarks, demonstrating the effectiveness of trajectory-level credit assignment for reinforcement learning in LoopLMs.
  arXiv  Detail & Related papers  (2026-02-11T04:39:42Z)
• Evaluating Large Language Models in Scientific Discovery [91.732562776782]
  Large language models (LLMs) are increasingly applied to scientific research, yet prevailing science benchmarks probe decontextualized knowledge.<n>We introduce a scenario-grounded benchmark that evaluates LLMs across biology, chemistry, materials, and physics.<n>The framework assesses models at two levels: (i) question-level accuracy on scenario-tied items and (ii) project-level performance.
  arXiv  Detail & Related papers  (2025-12-17T16:20:03Z)
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
  Large language models (LLMs) have recently demonstrated remarkable progress in formal theorem proving.<n>Yet their ability to serve as practical assistants for mathematicians, filling in missing steps within complex proofs, remains underexplored.<n>We introduce FormalML, a Lean 4 benchmark built from foundational theories of machine learning.
  arXiv  Detail & Related papers  (2025-09-26T14:40:14Z)
• Revisiting LLM Reasoning via Information Bottleneck [57.519119962528166]
  Large language models (LLMs) have recently demonstrated remarkable progress in reasoning capabilities through reinforcement learning with verifiable rewards (RLVR)<n>We present a theoretical characterization of LLM reasoning grounded in information bottleneck (IB) principle.<n>We propose IB-aware reasoning optimization (IBRO), a framework that encourages reasoning trajectories to be both informative about the final correct answer and generalizable.
  arXiv  Detail & Related papers  (2025-07-24T13:14:25Z)
• Model Reprogramming Demystified: A Neural Tangent Kernel Perspective [49.42322600160337]
  We present a comprehensive theoretical analysis of Model Reprogramming (MR) through the lens of the Neural Tangent Kernel (NTK) framework.<n>We demonstrate that the success of MR is governed by the eigenvalue spectrum of the NTK matrix on the target dataset.<n>Our contributions include a novel theoretical framework for MR, insights into the relationship between source and target models, and extensive experiments validating our findings.
  arXiv  Detail & Related papers  (2025-05-31T16:15:04Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  We present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems.<n>We introduce a novel human-in-the-loop autoformalization pipeline that integrates statement autoformalization, semantic verification, and negation-based disproof filtering strategies.<n>Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations.
  arXiv  Detail & Related papers  (2025-05-05T15:37:00Z)
• Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning [38.4246156415702]
  Kimina-Prover is a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving.<n>Trained with a large-scale reinforcement learning pipeline from Qwen2.5-72B, Kimina-Prover demonstrates strong performance in Lean 4 proof generation.<n>Kimina-Prover sets a new state-of-the-art on the miniF2F benchmark, reaching 80.7% with pass@8192.
  arXiv  Detail & Related papers  (2025-04-15T16:23:44Z)
• Theorem Prover as a Judge for Synthetic Data Generation [22.124954482278536]
  We present a framework that replaces human annotation with theorem prover in Reinforcement Learning from Human Feedback (RLHF)<n>Across multiple large language models (LLMs), applying TP-as-a-Judge and RF improves benchmarks with only 3,508 samples, achieving 5.56% accuracy on Mistral-7B for MultiArithm.
  arXiv  Detail & Related papers  (2025-02-18T18:57:09Z)
• TFG: Unified Training-Free Guidance for Diffusion Models [82.14536097768632]
  Training-free guidance can generate samples with desirable target properties without additional training. Existing methods, though effective in various individual applications, often lack theoretical grounding and rigorous testing on extensive benchmarks. This paper introduces a novel algorithmic framework encompassing existing methods as special cases, unifying the study of training-free guidance into the analysis of an algorithm-agnostic design space.
  arXiv  Detail & Related papers  (2024-09-24T05:31:17Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.