用AI自动生成Rust代码的正确性证明，准确率超90%。
AutoVerus: Automated Proof Generation for Rust Code
- 设计多智能体系统模拟人类写证明的三阶段过程
- 在150个任务中90%以上生成正确证明，半数<30秒完成
- 适合做Rust安全验证和形式化方法研究者使用
生成式AI在软件工程中展现价值，但基于大语言模型（LLM）的证明生成仍落后于代码生成。本文提出AutoVerus，利用LLM自动为Rust代码生成正确性证明。AutoVerus针对Verus这一可使用Rust编写证明与规范的验证工具进行设计，由一组精心构建并协调的LLM智能体组成，模拟人类专家的三个证明构建阶段：初步证明生成、基于通用提示的证明优化，以及基于验证错误的调试。为全面评估AutoVerus并推动该方向研究，我们基于现有代码生成与验证基准构建了一个包含150个非平凡证明任务的评测集。评估结果显示，AutoVerus可在超过90%的任务中自动生成正确证明，其中超过一半任务在30秒内或3次LLM调用内完成。
原文摘要 · Abstract (English)
Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLMs to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。