LLM 在证明助理中的验证效果案例研究
编程语言
2025-08-27 v1 人工智能
摘要
大型语言模型 (LLM) 可能通过自动化证明来帮助使用证明助理，但 LLM 在此任务中的有效性尚不明确。本文基于两个成熟的 Rocq 项目：hs-to-coq 工具和 Verdi，进行了案例研究。我们对 LLM 在生成证明方面的效果进行了定量和定性分析。我们的研究发现：(1) 外部依赖项和同一源文件中的上下文对证明生成具有显著帮助；(2) LLM 在小型证明方面表现出色，但也会生成大型证明；(3) LLM 在不同的验证项目中的表现不同；(4) LLM 能够生成简洁且聪慧的证明，能够将经典技术应用于新定义，但也会出现奇怪的错误。
引用
@article{arxiv.2508.18587,
title = {A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants},
author = {Barış Bayazıt and Yao Li and Xujie Si},
journal= {arXiv preprint arXiv:2508.18587},
year = {2025}
}
备注
Accepted by LMPL 2025