LLMs在形式化验证中能自动生成证明，但效果受项目和上下文影响。
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
- 利用代码上下文与外部依赖提升证明生成质量
- 对小型证明表现优异，也能生成大型复杂证明
- 适合研究形式化验证与LLM融合的开发者参考
大型语言模型（LLMs）有望通过自动化证明来辅助使用证明助手进行形式化验证。然而，其在该任务中的实际效果尚不明确。本文基于两个成熟的Rocq项目——hs-to-coq工具和Verdi，开展案例研究，通过定量与定性分析评估LLMs生成证明的有效性。研究发现：（1）外部依赖和同一源文件中的上下文信息显著有助于证明生成；（2）LLMs在小型证明上表现良好，也能生成大型证明；（3）不同验证项目中，LLMs表现存在差异；（4）LLMs可生成简洁且巧妙的证明，能将经典技术应用于新定义，但也可能产生奇怪错误。
原文摘要 · Abstract (English)
Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we perform a case study based on two mature Rocq projects: the hs-to-coq tool and Verdi. We evaluate the effectiveness of LLMs in generating proofs by both quantitative and qualitative analysis. Our study finds that: (1) external dependencies and context in the same source file can significantly help proof generation; (2) LLMs perform great on small proofs but can also generate large proofs; (3) LLMs perform differently on different verification projects; and (4) LLMs can generate concise and smart proofs, apply classical techniques to new definitions, but can also make odd mistakes.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。