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

• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• eSapiens: A Real-World NLP Framework for Multimodal Document Understanding and Enterprise Knowledge Processing [6.450269621190948]
  We introduce eSapiens, a unified question-answering system designed for enterprise settings.<n>eSapiens bridges structured databases and unstructured corpora via a dual-module architecture.<n>We evaluate eSapiens on the RAGTruth benchmark, analyzing performance across key dimensions such as completeness, hallucination, and context utilization.
  arXiv  Detail & Related papers  (2025-06-20T06:07:20Z)
• SPARE: Single-Pass Annotation with Reference-Guided Evaluation for Automatic Process Supervision and Reward Modelling [70.01883340129204]
  Single-Pass.<n>with Reference-Guided Evaluation (SPARE)<n>Novel structured framework that enables single-pass, per-step annotation by aligning each solution step to one or multiple steps in a reference solution, accompanied by explicit reasoning for evaluation.<n>SPARE achieves competitive performance on challenging mathematical datasets while offering 2.6 times greater efficiency, requiring only 38% of the runtime.
  arXiv  Detail & Related papers  (2025-06-18T14:37:59Z)
• ImpRAG: Retrieval-Augmented Generation with Implicit Queries [49.510101132093396]
  ImpRAG is a query-free RAG system that integrates retrieval and generation into a unified model.<n>We show that ImpRAG achieves 3.6-11.5 improvements in exact match scores on unseen tasks with diverse formats.
  arXiv  Detail & Related papers  (2025-06-02T21:38:21Z)
• 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.