arXiv:2502.05344v1 宣告类型: 交叉 摘要：将自动化形式化验证扩展到实际项目中需要解决跨模块依赖和全局上下文的问题，而现有的以函数为中心的方法忽视了这些问题。我们引入了RagVerus框架，该框架结合了检索增强生成与上下文感知提示，以自动化多模块仓库的证明合成。在我们新颖的RepoVBench基准测试中，该基准测试是首个针对Verus的仓库级数据集，包含383个证明完成任务，RagVerus实现了27%的相对改进。在受约束的语言模型预算下，RagVerus将现有基准的证明通过率提高三倍，证明了其可扩展性和样本效率的验证能力。