Towards Large Language Models as Copilots for Theorem Proving in Lean

定理证明是大型语言模型（LLMs）面临的一个重要挑战，因为形式证明可以被诸如Lean之类的证明助手严格检查，没有幻觉的空间。现有的基于LLM的证明器试图在完全自主的模式下证明定理，没有人类干预。在这种模式下，它们难以处理新颖和具有挑战性的定理，人类的洞察力可能是至关重要的。在本文中，我们探讨LLMs作为副驾驶员协助人类证明定理的可能性。我们介绍了Lean Copilot，一个在Lean中运行LLM推理的框架。它使程序员能够构建各种基于LLM的证明自动化工具，无缝集成到Lean用户的工作流程中。使用Lean Copilot，我们构建了工具，用于建议证明步骤（策略建议），完成中间证明目标（证明搜索）和选择相关前提条件（前提条件选择）使用LLMs。用户可以使用我们预训练的模型或带有或不带有GPU的本地或云端的模型。实验结果表明，与现有基于规则的Lean证明自动化相比，我们的方法在协助人类和自动化定理证明过程方面是有效的。我们在允许性的MIT许可下开源所有代码，以促进进一步的研究。

本论文旨在探索将大型语言模型（LLMs）作为协同工具，辅助人类证明定理。现有的基于LLMs的证明器尝试在完全自主模式下证明定理，但对于新颖和具有挑战性的定理而言，人类的洞见可能是至关重要的。

本文提出了Lean Copilot框架，将LLM推理引入Lean中，使程序员能够构建各种基于LLM的证明自动化工具，无缝集成到Lean用户的工作流程中。

本文介绍了三种工具：策略建议、证明搜索和前提选择。用户可以使用预训练的模型或自己的模型，这些模型可以在本地或云上运行。作者开源了所有代码，以促进进一步的研究。实验结果表明，相对于现有的基于规则的证明自动化方法，本文的方法在辅助人类和自动化定理证明过程方面具有有效性。

最近的相关研究包括：1）NeurIPS 2020上的“Proof Generalization in Coq via Abstract Interpretation and Deep Learning”；2）ICLR 2021上的“Neural Theorem Proving with Type Theory and Homotopy Theory”；3）ICLR 2020上的“Learning to Prove with Tactics”。