用检索增强生成实现跨模块代码验证，提升真实项目验证效率。
RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
- 结合检索与上下文提示，自动合成多模块代码证明
- 在新基准上相对提升27%，证明通过率翻三倍
- 适合需要高效验证大型代码库的开发者
将自动化形式化验证扩展到真实项目，需解决跨模块依赖与全局上下文问题，现有函数级方法未能覆盖此类挑战。我们提出RagVerus框架，融合检索增强生成与上下文感知提示，实现多模块代码仓库的自动化证明合成，在全新构建的RepoVBench基准（含383个证明任务）上取得27%的相对提升。在受限语言模型预算下，该框架使现有基准的证明通过率提升三倍，展示了可扩展且样本高效的验证能力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。