RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912224284508160 |
|---|---|
| author | Zhong, Sicheng Zhu, Jiading Tian, Yifang Si, Xujie |
| author_facet | Zhong, Sicheng Zhu, Jiading Tian, Yifang Si, Xujie |
| contents | Scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are challenges overlooked by existing function-centric methods. We introduce RagVerus, a framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories, achieving a 27% relative improvement on our novel RepoVBench benchmark -- the first repository-level dataset for Verus with 383 proof completion tasks. RagVerus triples proof pass rates on existing benchmarks under constrained language model budgets, demonstrating a scalable and sample-efficient verification. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_05344 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation Zhong, Sicheng Zhu, Jiading Tian, Yifang Si, Xujie Software Engineering Artificial Intelligence Scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are challenges overlooked by existing function-centric methods. We introduce RagVerus, a framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories, achieving a 27% relative improvement on our novel RepoVBench benchmark -- the first repository-level dataset for Verus with 383 proof completion tasks. RagVerus triples proof pass rates on existing benchmarks under constrained language model budgets, demonstrating a scalable and sample-efficient verification. |
| title | RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation |
| topic | Software Engineering Artificial Intelligence |
| url | https://arxiv.org/abs/2502.05344 |