一句话：提出 PALM：让 LLM 先生成证明，再用符号方法迭代修复低层错误，大幅提升 Coq 形式证明自动化成功率。
Coq 等交互式定理证明器能形式化保证软件正确性，但使用门槛高、需大量人工与专业知识。已有大语言模型（LLM）虽能生成自然语言非形式证明，却在生成形式证明时表现不佳。本文通过形成性研究分析 GPT-3.5 产生的 520 个证明生成错误，发现模型常能把握证明的高层结构，但低层细节频繁出错。据此提出 PALM：先由 LLM 生成初始证明，再用针对性的符号方法迭代修复低层问题。作者在含 1 万余条定理的大规模数据集上评估，PALM 比现有最优方法多证明 76.6% 至 180.4% 的定理，并额外证明 1270 条现有方法无法处理的定理；实验还表明该方法可泛化到不同 LLM。
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.