Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean

📄 arXiv: 2404.12534v3 📥 PDF

作者: Peiyang Song, Kaiyu Yang, Anima Anandkumar

分类: cs.AI, cs.LG, cs.LO, stat.ML

发布日期: 2024-04-18 (更新: 2025-05-11)

备注: Published at NeuS 2025. All code and artifacts open-sourced at https://github.com/lean-dojo/LeanCopilot. All evaluation details are made public at https://github.com/Peiyang-Song/mathematics_in_lean/tree/full-scale-experiment

💡 一句话要点

提出Lean Copilot以解决自动定理证明中的人机协作问题

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

关键词: 大型语言模型 定理证明 Lean 神经网络 自动化工具 人机协作 数学证明 开源软件

📋 核心要点

  1. 现有神经定理证明器在固定数据集上预训练，难以在完全自主的模式下持续证明新定理，且人类的洞察力可能至关重要。
  2. 本文提出Lean Copilot框架，作为人类的助手，支持在Lean中原生运行LLM推理，帮助用户构建多种证明自动化工具。
  3. 实验结果显示，Lean Copilot在辅助人类时平均只需2.08个手动输入步骤，自动化定理证明时自动化步骤比例达到74.2%，大幅优于现有方法。

📝 摘要（中文）

神经定理证明结合了大型语言模型（LLMs）与如Lean等证明助手，确保形式证明的正确性。现有的神经定理证明器在固定数据集上预训练，难以在完全自主的模式下持续证明新定理。本文提出Lean Copilot框架，作为人类证明定理的助手，支持在Lean中原生运行LLM推理。Lean Copilot允许用户使用预训练模型或自定义模型，构建多种基于LLM的证明自动化工具。实验结果表明，Lean Copilot在辅助人类时平均只需2.08个手动输入的证明步骤，显著优于现有方法aesop的3.86个步骤，并且在自动化定理证明过程中，Lean Copilot的自动化步骤比例达到74.2%，比aesop提升85%。

🔬 方法详解

问题定义：本文旨在解决现有神经定理证明器在固定数据集上预训练的局限性，导致其在自主证明新定理时的能力不足。现有方法如aesop在自动化程度和人机协作方面存在明显短板。

核心思路：Lean Copilot通过将大型语言模型作为人类证明定理的助手，提供实时建议和自动化支持，旨在提升定理证明的效率和准确性。该框架允许用户在Lean环境中灵活使用预训练或自定义的LLM。

技术框架：Lean Copilot的整体架构包括LLM推理模块、用户交互接口和证明步骤建议模块。用户可以通过该框架接入不同的LLM，进行实时的证明步骤建议、目标完成和相关前提选择。

关键创新：Lean Copilot的主要创新在于其将LLM与证明助手Lean的无缝集成，提供了一种新的人机协作模式，显著提升了定理证明的自动化程度和用户体验。

关键设计：在设计中，Lean Copilot支持本地和云端模型运行，允许用户根据需求选择不同的计算资源。模型的训练和推理过程经过优化，以确保在Lean环境中的高效运行。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，Lean Copilot在辅助人类时平均只需2.08个手动输入步骤，相较于aesop的3.86步骤减少了46.5%；在自动化定理证明过程中，Lean Copilot的自动化步骤比例达到74.2%，比aesop的40.1%提升了85%。

🎯 应用场景

Lean Copilot的研究成果在数学、计算机科学及相关领域的定理证明中具有广泛的应用潜力。通过提高定理证明的自动化程度和人机协作效率，该框架能够帮助研究人员和工程师更快速地验证复杂理论，推动相关领域的发展。

📄 摘要（原文）

Neural theorem proving combines large language models (LLMs) with proof assistants such as Lean, where the correctness of formal proofs can be rigorously verified, leaving no room for hallucination. With existing neural theorem provers pretrained on a fixed collection of data and offering valuable suggestions at times, it is challenging for them to continually prove novel theorems in a fully autonomous mode, where human insights may be critical. In this paper, we explore LLMs as copilots that assist humans in proving theorems. We introduce Lean Copilot, a general framework for running LLM inference natively in Lean. It enables programmers to build various LLM-based proof automation tools that integrate seamlessly into the workflow of Lean users. Lean users can use our pretrained models or bring their own ones that run either locally (with or without GPUs) or on the cloud. Using Lean Copilot, we build LLM-based tools that suggest proof steps, complete proof goals, and select relevant premises. Experimental results on the Mathematics in Lean textbook demonstrate the effectiveness of our method compared to existing rule-based proof automation in Lean (aesop). When assisting humans, Lean Copilot requires only 2.08 manually-entered proof steps on average (3.86 required by aesop); when automating the theorem proving process, Lean Copilot automates 74.2% proof steps on average, 85% better than aesop (40.1%). We open source all code and artifacts under a permissive MIT license to facilitate further research.