2025_NIPS_LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

文章核心总结与创新点主要内容本文针对现有基于大语言模型（LLMs）的定理证明工具存在私有代码、数据封闭、计算成本高的问题，提出了开源工具包LeanDojo，包含数据提取、交互工具、基准数据集和检索增强型证明模型ReProver。LeanDojo可从证明助手Lean中提取细粒度数据（含前提标注），构建含98,734个定理的基准数据集，并提供可靠的程序化交互环境；ReProver通过检索数学库中的前提辅助定理证明，仅需单GPU训练一周，在多个数据集上表现优于无检索基线和GPT-4，还能生成Lean中缺失的证明。创新点开源工具链LeanDojo：首次实现对Lean的可靠数据提取（含前提定位）和程序化交互，将证明检查错误率从21.1%降至1.4%，支持Lean 3和Lean 4。检索增强证明模型ReProver：首个将检索融入LLM定理证明的模型，通过程序分析筛选可访问前提、构造难负例，解决前提选择瓶颈。挑战性基准数据集：设计“novel_premises”数据划分，要求模型泛化到训练中未见过的前提，避免依赖记忆完成证明。低资源高效训练：无需私有数据集和大规模预训练，单GPU一周即可完成训练，降低定理证明研究门槛。翻译部分（Markdown格式）Abstract大语言模型（LLMs）在使用Lean等证明助手进行形式化定理证明方面展现出潜力。然而，