Towards Repository-Level Program Verification with Large Language Models

• URL: http://arxiv.org/abs/2509.25197v1
• Date: Sun, 31 Aug 2025 02:44:04 GMT
• Title: Towards Repository-Level Program Verification with Large Language Models
• Authors: Si Cheng Zhong, Xujie Si,
• Abstract summary: scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts.<n>We introduce RVBench, the first verification benchmark explicitly designed for repository-level evaluation, constructed from four diverse and complex open-source Verus projects.<n>RagedVerus is a framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof for multi-module repositories.
• Score: 8.05666536952624
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Architecture-Aware Multi-Design Generation for Repository-Level Feature Addition [53.50448142467294]
  RAIM is a multi-design and architecture-aware framework for repository-level feature addition.<n>It shifts away from linear patching by generating multiple diverse implementation designs.<n>Experiments on the NoCode-bench Verified dataset demonstrate that RAIM establishes a new state-of-the-art performance.
  arXiv  Detail & Related papers  (2026-03-02T12:50:40Z)
• DiffuRank: Effective Document Reranking with Diffusion Language Models [71.16830004674513]
  We propose DiffuRank, a reranking framework built upon diffusion language models (dLLMs)<n>dLLMs support more flexible decoding and generation processes that are not constrained to a left-to-right order.<n>We show dLLMs achieve performance comparable to, and in some cases exceeding, that of autoregressive LLMs with similar model sizes.
  arXiv  Detail & Related papers  (2026-02-13T02:18:14Z)
• Towards Mixed-Modal Retrieval for Universal Retrieval-Augmented Generation [72.34977512403643]
  Retrieval-Augmented Generation (RAG) has emerged as a powerful paradigm for enhancing large language models (LLMs) by retrieving relevant documents from an external corpus.<n>Existing RAG systems primarily focus on unimodal text documents, and often fall short in real-world scenarios where both queries and documents may contain mixed modalities (such as text and images)<n>We propose Nyx, a unified mixed-modal to mixed-modal retriever tailored for Universal Retrieval-Augmented Generation scenarios.
  arXiv  Detail & Related papers  (2025-10-20T09:56:43Z)
• Retrieval-Augmented Code Generation: A Survey with Focus on Repository-Level Approaches [6.740646039135986]
  Retrieval-Augmented Generation (RAG) has emerged as a powerful paradigm that integrates external retrieval mechanisms with LLMs.<n>We provide a comprehensive review of research on Retrieval-Augmented Code Generation (RACG), with an emphasis on repository-level approaches.<n>Our goal is to establish a unified analytical framework for understanding this rapidly evolving field and to inspire continued progress in AI-powered software engineering.
  arXiv  Detail & Related papers  (2025-10-06T15:20:03Z)
• Loong: Synthesize Long Chain-of-Thoughts at Scale through Verifiers [103.4410890572479]
  We introduce the Loong Project: an open-source framework for scalable synthetic data generation and verification.<n>LoongBench is a curated seed dataset containing 8,729 human-vetted examples across 12 domains.<n>LoongEnv is a modular synthetic data generation environment that supports multiple prompting strategies to produce new question-answer-code triples.
  arXiv  Detail & Related papers  (2025-09-03T06:42:40Z)
• SaraCoder: Orchestrating Semantic and Structural Cues for Profit-Oriented Repository-Level Code Completion [37.66834526941521]
  Retrieval-augmented generation (RAG) for repository-level code completion commonly relies on superficial text similarity.<n>We introduce Saracoder, a Hierarchical Feature-d retrieval framework.
  arXiv  Detail & Related papers  (2025-08-13T11:56:05Z)
• 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)
• Crossing the Reward Bridge: Expanding RL with Verifiable Rewards Across Diverse Domains [92.36624674516553]
  Reinforcement learning with verifiable rewards (RLVR) has demonstrated significant success in enhancing mathematical reasoning and coding performance of large language models (LLMs)<n>We investigate the effectiveness and scalability of RLVR across diverse real-world domains including medicine, chemistry, psychology, economics, and education.<n>We utilize a generative scoring technique that yields soft, model-based reward signals to overcome limitations posed by binary verifications.
  arXiv  Detail & Related papers  (2025-03-31T08:22:49Z)
• Thinking Longer, Not Larger: Enhancing Software Engineering Agents via Scaling Test-Time Compute [61.00662702026523]
  We propose a unified Test-Time Compute scaling framework that leverages increased inference-time instead of larger models.<n>Our framework incorporates two complementary strategies: internal TTC and external TTC.<n>We demonstrate our textbf32B model achieves a 46% issue resolution rate, surpassing significantly larger models such as DeepSeek R1 671B and OpenAI o1.
  arXiv  Detail & Related papers  (2025-03-31T07:31:32Z)
• Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation [24.081573908824353]
  First-order logic (FOL) reasoning is pivotal for intelligent systems.<n>Existing benchmarks often rely on extensive human annotation or handcrafted templates.<n>We propose a novel framework called ProverGen that synergizes the generative strengths of Large Language Models with the rigor and precision of symbolic provers.
  arXiv  Detail & Related papers  (2025-02-10T15:31:54Z)
• RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation [4.934638689939017]
  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.
  arXiv  Detail & Related papers  (2025-02-07T21:30:37Z)
• 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)

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.