用大模型生成再修复，大幅提升形式化证明成功率
Proof Automation with Large Language Models
- 先让大模型生成初始证明，再用符号方法逐层修复细节错误
- 在超1万定理数据集上，比现有方法多证明76.6%至180.4%的定理
- 可适配不同大模型，适用于形式化验证与自动化推理场景
交互式定理证明器（如Coq）能严格保证软件正确性，但使用成本高且依赖专家。尽管大语言模型（LLMs）在自然语言证明生成上表现良好，但在生成形式化证明方面仍显不足。本文对GPT-3.5生成的520个证明错误进行分析，发现其常能识别正确高层结构，却难以处理底层细节。基于此，我们提出PALM——一种‘生成-修复’新范式：先由大模型生成初始证明，再通过针对性符号方法迭代修正低级错误。在包含超过1万定理的数据集上评估，PALM显著优于现有方法，成功证明的定理数量提升76.6%至180.4%，并额外攻克1270个此前无法解决的定理。实验还验证了PALM在不同大模型间的泛化能力。
原文摘要 · Abstract (English)
Interactive theorem provers such as Coq are powerful tools to formally guarantee the correctness of software. However, using these tools requires significant manual effort and expertise. While Large Language Models (LLMs) have shown promise in automatically generating informal proofs in natural language, they are less effective at generating formal proofs in interactive theorem provers. In this paper, we conduct a formative study to identify common mistakes made by LLMs when asked to generate formal proofs. By analyzing 520 proof generation errors made by GPT-3.5, we found that GPT-3.5 often identified the correct high-level structure of a proof, but struggled to get the lower-level details correct. Based on this insight, we propose PALM, a novel generate-then-repair approach that first prompts an LLM to generate an initial proof and then leverages targeted symbolic methods to iteratively repair low-level problems. We evaluate PALM on a large dataset that includes more than 10K theorems. Our results show that PALM significantly outperforms other state-of-the-art approaches, successfully proving 76.6% to 180.4% more theorems. Moreover, PALM proves 1270 theorems beyond the reach of existing approaches. We also demonstrate the generalizability of PALM across different LLMs.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。