用大模型实现整个代码库的自动验证，突破单函数局限。
Towards Repository-Level Program Verification with Large Language Models
- 结合检索增强生成与上下文感知提示，跨模块协同生成证明。
- 在复杂库级任务上证明通过率提升27%，推理资源受限下仍高效。
- 首个专为库级验证设计的基准测试RVBench，推动真实项目验证研究。
大型语言模型（LLM）在代码与证明生成方面展现出巨大潜力。然而，将自动化形式化验证扩展到真实项目时，仍需解决跨模块依赖和全局上下文问题，而现有基于LLM的方法多聚焦于孤立的函数级验证任务，忽视了这些关键挑战。为此，我们提出RVBench，首个专为库级验证设计的评估基准，基于四个多样且复杂的开源Verus项目构建。同时引入RagVerus框架，融合检索增强生成与上下文感知提示，实现多模块库的自动化证明合成。RagVerus在现有基准上的证明通过率提升三倍，在更具挑战性的RVBench上实现27%的相对提升，展示了可扩展且样本高效的验证方案。
原文摘要 · Abstract (English)
Recent advancements in large language models (LLMs) suggest great promises in code and proof generations. However, scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are crucial challenges overlooked by existing LLM-based methods with a special focus on targeting isolated, function-level verification tasks. To systematically explore and address the significant challenges of verifying entire software repositories, we introduce RVBench, the first verification benchmark explicitly designed for repository-level evaluation, constructed from four diverse and complex open-source Verus projects. We further introduce RagVerus, an extensible framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories. RagVerus triples proof pass rates on existing benchmarks under constrained model inference budgets, and achieves a 27% relative improvement on the more challenging RVBench benchmark, demonstrating a scalable and sample-efficient verification solution.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。