REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

📄 arXiv: 2505.20613v3 📥 PDF

作者: Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, Haocheng Ju, Peihao Wu, Bryan Dai, Bin Dong

分类: cs.CL, cs.AI, cs.LG, cs.LO

发布日期: 2025-05-27 (更新: 2025-11-24)

💡 一句话要点

REAL-Prover：一种检索增强的Lean定理证明器，用于数学推理

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

关键词: 定理证明 大型语言模型 检索增强 Lean 4 数学推理

📋 核心要点

  1. 现有定理证明器在高数和竞赛级数学上取得进展，但在更高级数学问题上泛化能力不足。
  2. REAL-Prover通过微调LLM并集成检索系统，提升了解决大学水平数学问题的能力。
  3. 实验表明，REAL-Prover在ProofNet和FATE-M数据集上取得了有竞争力的结果，甚至是最先进的性能。

📝 摘要（中文）

本文提出了一种新的开源逐步定理证明器REAL-Prover，用于Lean 4，旨在突破现有定理证明器在高级数学问题上的局限性。该证明器基于微调的大型语言模型(REAL-Prover-v1)并集成了检索系统(Leansearch-PS)，显著提升了解决大学水平数学问题的性能。为了训练REAL-Prover-v1，我们开发了HERALD-AF数据提取管道，将自然语言数学问题转换为形式化陈述，并构建了一个新的开源Lean 4交互式环境(Jixia-interactive)以促进合成数据的收集。实验表明，仅使用监督微调的证明器在ProofNet数据集上取得了具有竞争力的结果，成功率为23.7%(Pass@64)，与最先进的模型相当。为了进一步评估该方法，我们引入了FATE-M，这是一个专注于代数问题的新基准，我们的证明器在该基准上实现了56.7%(Pass@64)的最先进成功率。

🔬 方法详解

问题定义：现有形式化定理证明器在解决高级数学问题，特别是大学水平的数学问题时，存在泛化能力不足的瓶颈。现有的方法难以有效地将自然语言描述的数学问题转化为形式化的证明过程，并且缺乏足够的训练数据来支持复杂数学推理的学习。

核心思路：REAL-Prover的核心思路是结合大型语言模型（LLM）的推理能力和检索系统的知识获取能力，通过检索相关的定理和证明步骤来辅助LLM进行定理证明。通过这种方式，可以有效地利用已有的数学知识，并提高证明的成功率。

技术框架：REAL-Prover的整体框架包括以下几个主要模块：1) 数据提取管道HERALD-AF，用于将自然语言数学问题转换为形式化陈述；2) Lean 4交互式环境Jixia-interactive，用于收集合成数据；3) 微调的大型语言模型REAL-Prover-v1，作为核心推理引擎；4) 检索系统Leansearch-PS，用于检索相关的定理和证明步骤。整个流程是，首先使用HERALD-AF将自然语言问题转化为形式化陈述，然后REAL-Prover-v1结合Leansearch-PS检索到的信息，逐步进行定理证明。

关键创新：REAL-Prover的关键创新在于将检索增强与大型语言模型相结合，用于形式化定理证明。此外，HERALD-AF数据提取管道和Jixia-interactive交互式环境的开发也为训练数据收集提供了新的途径。

关键设计：REAL-Prover-v1是基于大型语言模型进行微调的，具体的模型架构和训练细节（如损失函数、网络结构等）在论文中可能没有详细说明，属于未知信息。Leansearch-PS检索系统的具体实现细节也未知。HERALD-AF数据提取管道和Jixia-interactive交互式环境的设计细节也需要参考论文原文。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

REAL-Prover在ProofNet数据集上取得了23.7%(Pass@64)的成功率，与最先进的模型相当。更重要的是，在新的FATE-M基准上，REAL-Prover实现了56.7%(Pass@64)的最先进成功率，表明其在代数问题上具有显著优势。

🎯 应用场景

REAL-Prover的应用场景包括自动化定理证明、数学教育、形式化验证等领域。它可以辅助数学家进行研究，帮助学生学习数学，并用于验证软件和硬件系统的正确性。未来，该技术有望应用于更广泛的科学和工程领域，例如物理、化学、生物等。

📄 摘要（原文）

Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this paper, we present REAL-Prover, a new open-source stepwise theorem prover for Lean 4 to push this boundary. This prover, based on our fine-tuned large language model (REAL-Prover-v1) and integrated with a retrieval system (Leansearch-PS), notably boosts performance on solving college-level mathematics problems. To train REAL-Prover-v1, we developed HERALD-AF, a data extraction pipeline that converts natural language math problems into formal statements, and a new open-source Lean 4 interactive environment (Jixia-interactive) to facilitate synthesis data collection. In our experiments, our prover using only supervised fine-tune achieves competitive results with a 23.7% success rate (Pass@64) on the ProofNet dataset-comparable to state-of-the-art (SOTA) models. To further evaluate our approach, we introduce FATE-M, a new benchmark focused on algebraic problems, where our prover achieves a SOTA success rate of 56.7% (Pass@64).