arXiv:2404.12534v3 公告类型: 替换 摘要: 神经定理证明将大型语言模型（LLMs）与Lean等证明助手相结合，后者可以严格验证形式证明的正确性，没有幻觉的空间。尽管现有的神经定理证明者已经针对固定的数据集进行了预训练，并在某些时候提供了有价值的建议，但在完全自主模式下，它们仍然难以持续证明新颖的定理，这时候人类的见解可能是关键性的。本文我们探索了将LLMs作为辅助编程人员来协助证明定理的合作者。我们引入了Lean Copilot，这是一种在Lean中原生运行LLM推理的通用框架。它使程序员能够构建无缝集成到Lean用户工作流的各种LLM为基础的证明自动化工具。Lean用户可以使用我们预训练的模型或自己提供运行在本地（可能配有GPU）或云端的模型。使用Lean Copilot，我们构建了基于LLM的工具来建议证明步骤、完成证明目标并选择相关前提。在Lean教科书中的数学定理实验结果表明，我们的方法相比Lean中的基于规则的证明自动化（aesop）更加有效。在协助人类时，Lean Copilot平均只需手动输入2.08个证明步骤（aesop需要3.86个）；在自动化证明过程时，Lean Copilot平均自动化了74.2%的证明步骤，比aesop多出85%（aesop为40.1%）。我们以宽松的MIT许可证开源所有代码和资源，以促进进一步的研究。