arXiv:2409.14274v1 公告类型: 交叉 摘要: 交互式定理证明器如Coq是正式保证软件正确性的强大工具。然而，使用这些工具需要大量的手动努力和专业知识。尽管大型语言模型(LLMs)在自动生成自然语言的非正式证明方面显示出潜力，但它们在生成交互式定理证明器中的正式证明方面效果较差。在本文中，我们进行了一项形成性研究，以识别LLMs在生成正式证明时常见的错误。通过分析GPT-3.5生成的520个证明错误，我们发现GPT-3.5通常能够识别证明的高层次结构，但在低层次细节上遇到困难。基于这一洞察，我们提出了PALM，一种新颖的生成-修复方法，首先提示LLM生成初始证明，然后利用有针对性的符号方法迭代修复低层次问题。我们在包含超过10K个定理的大型数据集上评估了PALM。结果显示，PALM显著优于其他最先进的方法，成功证明了76.6%到180.4%更多的定理。此外，PALM证明了1270个现有方法无法证明的定理。我们还展示了PALM在不同LLMs之间的通用性。