RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation

• URL: http://arxiv.org/abs/2502.05344v1
• Date: Fri, 07 Feb 2025 21:30:37 GMT
• Title: RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
• Authors: Sicheng Zhong, Jiading Zhu, Yifang Tian, Xujie Si,
• Abstract summary: We introduce RagVerus, a framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories.<n>R RagVerus triples proof pass rates on existing benchmarks under constrained language model budgets.
• Score: 4.934638689939017
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• REAL-MM-RAG: A Real-World Multi-Modal Retrieval Benchmark [16.55516587540082]
  We introduce REAL-MM-RAG, an automatically generated benchmark designed to address four key properties essential for real-world retrieval. We propose a multi-difficulty-level scheme based on query rephrasing to evaluate models' semantic understanding beyond keyword matching. Our benchmark reveals significant model weaknesses, particularly in handling table-heavy documents and robustness to query rephrasing.
  arXiv  Detail & Related papers  (2025-02-17T22:10:47Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  Iterative refinement has emerged as an effective paradigm for enhancing the capabilities of large language models (LLMs) on complex tasks. We propose Context-Wise Order-Agnostic Language Modeling (COrAL) to overcome these challenges. Our approach models multiple token dependencies within manageable context windows, enabling the model to perform iterative refinement internally.
  arXiv  Detail & Related papers  (2024-10-12T23:56:19Z)
• SFR-RAG: Towards Contextually Faithful LLMs [57.666165819196486]
  Retrieval Augmented Generation (RAG) is a paradigm that integrates external contextual information with large language models (LLMs) to enhance factual accuracy and relevance. We introduce SFR-RAG, a small LLM that is instruction-textual with an emphasis on context-grounded generation and hallucination. We also present ConBench, a new evaluation framework compiling multiple popular and diverse RAG benchmarks.
  arXiv  Detail & Related papers  (2024-09-16T01:08:18Z)
• RAGEval: Scenario Specific RAG Evaluation Dataset Generation Framework [69.4501863547618]
  This paper introduces RAGEval, a framework designed to assess RAG systems across diverse scenarios. With a focus on factual accuracy, we propose three novel metrics Completeness, Hallucination, and Irrelevance. Experimental results show that RAGEval outperforms zero-shot and one-shot methods in terms of clarity, safety, conformity, and richness of generated samples.
  arXiv  Detail & Related papers  (2024-08-02T13:35:11Z)
• DiscoveryBench: Towards Data-Driven Discovery with Large Language Models [50.36636396660163]
  We present DiscoveryBench, the first comprehensive benchmark that formalizes the multi-step process of data-driven discovery. Our benchmark contains 264 tasks collected across 6 diverse domains, such as sociology and engineering. Our benchmark, thus, illustrates the challenges in autonomous data-driven discovery and serves as a valuable resource for the community to make progress.
  arXiv  Detail & Related papers  (2024-07-01T18:58:22Z)
• On the Impacts of Contexts on Repository-Level Code Generation [5.641402231731082]
  We present RepoExec, a novel benchmark designed to evaluate repository-level code generation.<n>We focus on three key aspects: executability, functional correctness through comprehensive test case generation, and accurate utilization of cross-file contexts.
  arXiv  Detail & Related papers  (2024-06-17T10:45:22Z)
• RQ-RAG: Learning to Refine Queries for Retrieval Augmented Generation [42.82192656794179]
  Large Language Models (LLMs) exhibit remarkable capabilities but are prone to generating inaccurate or hallucinatory responses. This limitation stems from their reliance on vast pretraining datasets, making them susceptible to errors in unseen scenarios. Retrieval-Augmented Generation (RAG) addresses this by incorporating external, relevant documents into the response generation process.
  arXiv  Detail & Related papers  (2024-03-31T08:58:54Z)
• Repoformer: Selective Retrieval for Repository-Level Code Completion [30.706277772743615]
  Recent advances in retrieval-augmented generation (RAG) have initiated a new era in repository-level code completion. In this paper, we propose a selective RAG framework to avoid retrieval when unnecessary. We show that our framework is able to accommodate different generation models, retrievers, and programming languages.
  arXiv  Detail & Related papers  (2024-03-15T06:59:43Z)
• Continual Referring Expression Comprehension via Dual Modular Memorization [133.46886428655426]
  Referring Expression (REC) aims to localize an image region of a given object described by a natural-language expression. Existing REC algorithms make a strong assumption that training data feeding into a model are given upfront, which degrades its practicality for real-world scenarios. In this paper, we propose Continual Referring Expression (CREC), a new setting for REC, where a model is learning on a stream of incoming tasks. In order to continuously improve the model on sequential tasks without forgetting prior learned knowledge and without repeatedly re-training from a scratch, we propose an effective baseline method named Dual Modular Memorization
  arXiv  Detail & Related papers  (2023-11-25T02:58:51Z)
• Reference Twice: A Simple and Unified Baseline for Few-Shot Instance Segmentation [103.90033029330527]
  Few-Shot Instance (FSIS) requires detecting and segmenting novel classes with limited support examples. We introduce a unified framework, Reference Twice (RefT), to exploit the relationship between support and query features for FSIS.
  arXiv  Detail & Related papers  (2023-01-03T15:33:48Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.