AutoVerus: Automated Proof Generation for Rust Code
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915456070189056 |
|---|---|
| author | Yang, Chenyuan Li, Xuheng Misu, Md Rakib Hossain Yao, Jianan Cui, Weidong Gong, Yeyun Hawblitzel, Chris Lahiri, Shuvendu Lorch, Jacob R. Lu, Shuai Yang, Fan Zhou, Ziqiao Lu, Shan |
| author_facet | Yang, Chenyuan Li, Xuheng Misu, Md Rakib Hossain Yao, Jianan Cui, Weidong Gong, Yeyun Hawblitzel, Chris Lahiri, Shuvendu Lorch, Jacob R. Lu, Shuai Yang, Fan Zhou, Ziqiao Lu, Shan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_13082 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | AutoVerus: Automated Proof Generation for Rust Code Yang, Chenyuan Li, Xuheng Misu, Md Rakib Hossain Yao, Jianan Cui, Weidong Gong, Yeyun Hawblitzel, Chris Lahiri, Shuvendu Lorch, Jacob R. Lu, Shuai Yang, Fan Zhou, Ziqiao Lu, Shan Software Engineering Artificial Intelligence Formal Languages and Automata Theory 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. |
| title | AutoVerus: Automated Proof Generation for Rust Code |
| topic | Software Engineering Artificial Intelligence Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2409.13082 |