RLMEval: Evaluating Research-Level Neural Theorem Proving

📄 arXiv: 2510.25427v1 📥 PDF

作者: Auguste Poiroux, Antoine Bosselut, Viktor Kunčak

分类: cs.CL, cs.AI

发布日期: 2025-10-29

备注: Accepted to EMNLP 2025 Findings. RLMEval benchmark released: https://github.com/augustepoiroux/RLMEval

💡 一句话要点

RLMEval：提出用于评估研究级神经定理证明的新基准

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 神经定理证明 自动形式化 Lean 基准测试 形式数学

📋 核心要点

  1. 现有神经定理证明方法在人工基准上表现良好，但在实际研究级数学问题上效果不佳。
  2. RLMEval通过收集真实Lean形式化项目中的定理，构建更具挑战性的评估基准。
  3. 实验表明，现有模型在RLMEval上的表现远低于预期，突显了真实场景下的差距。

📝 摘要（中文）

尽管大型语言模型（LLMs）在精心设计的基准测试中取得了令人瞩目的成果，但它们在研究级神经定理证明和证明自动形式化方面的实际影响仍然有限。我们推出了RLMEval，这是一个用于评估这些任务的评估套件，专注于来自真实Lean形式化项目的研究级数学。RLMEval通过利用真实的Lean Blueprint形式化项目，旨在评估具有挑战性的研究级定理上的神经定理证明和证明自动形式化。我们对RLMEval上最先进模型的评估，包括来自6个Lean项目的613个定理，揭示了一个显著的差距：在现有基准上的进展并不能轻易转化为这些更真实的设置，最好的模型仅达到10.3%的通过率。RLMEval提供了一个新的、具有挑战性的基准，旨在指导和加速形式数学自动推理的进展。

🔬 方法详解

问题定义：论文旨在解决神经定理证明模型在真实研究级数学问题上泛化能力不足的问题。现有基准测试通常是人工设计的，与实际数学研究中遇到的问题存在较大差异，导致模型在这些基准上表现良好，但在实际应用中效果不佳。

核心思路：论文的核心思路是构建一个更贴近实际研究场景的评估基准，即RLMEval。该基准包含来自真实Lean形式化项目的定理，这些定理更具挑战性，能够更真实地反映模型在实际研究中的表现。通过在该基准上评估现有模型，可以更准确地了解模型的优缺点，并指导未来的研究方向。

技术框架：RLMEval的整体框架包括以下几个步骤：1) 从真实的Lean形式化项目中收集定理；2) 对收集到的定理进行预处理，使其适合神经定理证明模型；3) 使用现有模型在RLMEval上进行推理；4) 评估模型的性能，例如通过率。该框架的关键在于定理的收集和预处理，需要确保定理的质量和多样性。

关键创新：RLMEval的关键创新在于其数据集的来源。与现有基准测试不同，RLMEval的数据来自真实的Lean形式化项目，这些项目通常由数学家和计算机科学家共同完成，包含了大量的研究级数学知识。因此，RLMEval能够更真实地反映模型在实际研究中的表现，并为未来的研究提供更有价值的参考。

关键设计：RLMEval包含来自6个Lean项目的613个定理。评估指标主要采用通过率，即模型成功证明定理的比例。论文没有详细描述具体的参数设置、损失函数或网络结构，因为RLMEval主要关注基准测试的构建和评估，而不是提出新的模型。

🖼️ 关键图片

img_0

📊 实验亮点

在包含613个定理的RLMEval基准测试中，现有最先进的模型仅取得了10.3%的通过率。这一结果表明，现有模型在人工基准上的良好表现并不能转化为在真实研究级数学问题上的有效性，突显了RLMEval的价值和必要性。

🎯 应用场景

RLMEval可用于评估和改进神经定理证明、自动形式化验证等领域的研究。通过更真实的基准测试，可以推动相关技术在数学、计算机科学等领域的应用，例如辅助数学家进行定理证明、验证软件代码的正确性等，最终提升科研效率和软件可靠性。

📄 摘要（原文）

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.