作者： Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar
摘要：
大型语言模型（LLMs）在使用 Lean 等证明助手证明形式化定理方面已显示出潜力。然而，由于私有代码、数据和庞大的计算需求，现有方法难以复现或在其基础上进行构建，这为定理证明的机器学习方法研究设置了巨大障碍。本文通过引入 LeanDojo 来消除这些障碍：这是一个开源的 Lean 实验平台，包含工具包、数据、模型和基准。LeanDojo 从 Lean 中提取数据，并支持以编程方式与证明环境交互。它包含证明中前提（premises）的细粒度标注，为定理证明的关键瓶颈——前提选择——提供了宝贵的数据。利用这些数据，我们开发了 ReProver（检索增强证明器）：一个基于 LLM 的证明器，通过检索从庞大的数学库中选择前提。它成本低廉，仅需一个 GPU 周的训练。我们的检索器利用 LeanDojo 的程序分析能力来识别可访问的前提和困难的负例，这大大提高了检索的有效性。此外，我们构建了一个新的基准，包含从 Lean 数学库中提取的 98,734 个定理和证明。该基准具有挑战性的数据划分，要求证明器能够泛化到依赖于训练中从未使用过的新前提的定理。我们使用该基准进行训练和评估，实验结果表明 ReProver 优于非检索基线模型和 GPT-4。因此，我们提供了第一套不依赖任何专有数据集的开源 LLM 定理证明器，并在宽松的 MIT 许可证下发布，以促进进一步研究。
主题/分类：
- 机器学习 (cs.LG)
- 人工智能 (cs.AI)
- 计算机科学中的逻辑 (cs.LO)
- 机器学习 (stat.ML)
提交/修订日期： 2023年6月27日提交，2023年10月27日修订 (v2)
备注： 本文被 NeurIPS 2023（数据集与基准赛道）接收为口头报告。数据、代码和模型可在 https://leandojo.org/ 获取。