arXiv:2409.13082v2 宣布类型: 交叉替换 摘要：生成式AI已经在许多软件工程任务中展现了其价值。尽管如此，基于大规模语言模型（LLM）的证明生成仍落后于基于LLM的代码生成。在本文中，我们介绍了AutoVerus。AutoVerus使用LLM自动为Rust代码生成正确性证明。AutoVerus的设计旨在匹配Verus的特色，Verus是一个验证工具，可以使用证明和同样用Rust编写的规定来证明Rust代码的正确性。AutoVerus由一个LLM代理网络组成，该网络被定制和编排，以模拟人类专家在证明构建过程中的三个阶段：初步证明生成、由通用提示引导的证明细化、以及由验证错误引导的证明调试。为了全面评估AutoVerus并为这一领域的未来研究提供帮助，我们基于现有的代码生成基准和验证基准构建了一个包含150个非平凡证明任务的基准套件。我们的评估结果显示，AutoVerus可以自动为超过90%的证明任务生成正确的证明，其中一半以上可以在不到30秒或3次LLM调用内解决。