Automating Formal Verification with Reinforcement Learning and Recursive Inference

• URL: http://arxiv.org/abs/2605.30914v1
• Date: Fri, 29 May 2026 06:59:28 GMT
• Title: Automating Formal Verification with Reinforcement Learning and Recursive Inference
• Abstract summary: We train open-source models in Dafny with verifiable rewards (RLVR) and verifier-guided inference-time search.<n>With a fixed base model, the full scaffold with proof reviser improves pass rate on an initial VeriCoding pilot set from 46.2% under direct repair to 69.2%.<n>We also introduce Dalek-Bench, a repository-scale Lean benchmark derived from the Rust $texttcurve25519-dalek$ verification project.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated formal verification remains challenging for large language models because data for proof assistants and verification-aware languages is scarce, and correctness depends on satisfying precise machine-checkable specifications rather than producing plausible code. This thesis studies how verifier environments can improve LLM generation of verified programs and proofs through reinforcement learning from verifiable rewards (RLVR) and verifier-guided inference-time search. First, we train open-source models in Dafny with RLVR using Group Relative Policy Optimization (GRPO) and related variants, assembling generated candidates into complete programs and scoring them with compiler and verifier outcomes. Initial experiments on an APPS-derived Dafny dataset increased verified reward from 2.2% to 58.1%, but revealed specification hacking, where models exploit weak formal specifications instead of implementing the intended solutions. After filtering underspecified and vulnerable tasks, multi-turn RLVR on the refined benchmark improves the verified pass rate from 9.7% to 31.1%. Second, we develop a verifier-guided inference scaffold in Lean that treats proof generation as structured search over decomposed subgoals, verifier feedback, diagnostics, and repair. With a fixed base model, the full scaffold with proof reviser improves pass rate on an initial VeriCoding pilot set from 46.2% under direct repair to 69.2%. On the larger VERINA dataset, whole-task decomposition plus proof reviser solves 7 of 42 previously unsolved tasks. We also introduce Dalek-Bench, a repository-scale Lean benchmark derived from the Rust $\texttt{curve25519-dalek}$ verification project; preliminary results remain weak, indicating that stronger progress evaluation and task-specific tool-use policies are still needed.

Related papers

• SEVA: Self-Evolving Verification Agent with Process Reward for Fact Attribution [6.908637308550535]
  SEVA is a structured verification agent that emits evidence alignments, step-by-step reasoning chains, calibrated confidence, and a six-category error diagnosis.<n>On ClearFacts, SEVA-3B matches GPT-4o-mini (69.0 vs. 69.8 F1) while producing substantially richer, auditable output.
  arXiv  Detail & Related papers  (2026-06-29T02:37:13Z)
• Verifier-First Evaluation of Agentic LLMs for Infrastructure-as-Code Generation [0.0]
  Infrastructure-as-Code (IaC) generation from natural language requires satisfying provider schemas, dependency planning, and organizational policy constraints.<n>We present a verifier-first empirical study of seven agentic strategies for Terraform generation evaluated on IaC-Eval v2, a modernized 186-task AWS/Terraform benchmark with Rego v1 policies.
  arXiv  Detail & Related papers  (2026-05-29T12:43:27Z)
• Agentic Proving for Program Verification [44.663012714194025]
  Agentic systems have emerged as state-of-the-art approaches for automated theorem proving in formal mathematics.<n>We evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation.
  arXiv  Detail & Related papers  (2026-05-22T15:41:27Z)
• Rewarding the Scientific Process: Process-Level Reward Modeling for Agentic Data Analysis [68.28714988482703]
  Process Reward Models (PRMs) have achieved remarkable success in augmenting the reasoning capabilities of Large Language Models (LLMs)<n>We present a study revealing that general-domain PRMs struggle to supervise data analysis agents.<n>We introduce DataPRM, a novel environment-aware generative process reward model.
  arXiv  Detail & Related papers  (2026-04-27T09:00:30Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  Large Language Models show promise in automated software engineering, yet their guarantee of correctness is frequently undermined by erroneous or hallucinated code.<n>We provide the NaturalLanguage2VerifiedCode dataset: a collection of 60 complex algorithmic problems.<n>We evaluate 11 randomly selected problem sets across seven open-weight LLMs using a tiered prompting strategy.<n>Our results show that while contextless prompting leads to near-universal failure, structural anchors and iterative self-healing facilitate a dramatic performance turnaround.
  arXiv  Detail & Related papers  (2026-04-24T14:28:10Z)
• Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification [34.98335927187393]
  Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness.<n>We propose a hierarchical proof search framework for automated code verification in Lean4.<n>We train Goedel-Code-Prover-8B, a single unified policy for both decomposition and completion.
  arXiv  Detail & Related papers  (2026-03-18T18:42:04Z)
• HLE-Verified: A Systematic Verification and Structured Revision of Humanity's Last Exam [63.84155758655084]
  Humanity's Last Exam (HLE) has become a widely used benchmark for evaluating frontier large language models.<n>We introduce HLE-Verified, a verified and revised version of HLE with a transparent verification protocol and fine-grained error taxonomy.<n>We evaluate seven state-of-the-art language models on HLE and HLE-Verified, observing an average absolute accuracy gain of 7--10 percentage points.
  arXiv  Detail & Related papers  (2026-02-15T02:50:15Z)
• PRIME: A Process-Outcome Alignment Benchmark for Verifiable Reasoning in Mathematics and Engineering [71.15346406323827]
  We introduce PRIME, a benchmark for evaluating verifiers on Process-Outcome Alignment verification.<n>We find that current verifiers frequently fail to detect derivation flaws.<n>We propose a process-aware RLVR training paradigm utilizing verifiers selected via PRIME.
  arXiv  Detail & Related papers  (2026-02-12T04:45:01Z)
• CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
  Code verifiers play a critical role in post-verification for LLM-based code generation.<n>Existing supervised fine-tuning methods suffer from data scarcity, high failure rates, and poor inference efficiency.<n>We show that naive RL with only functionality rewards fails to generate effective unit tests for difficult branches and samples.
  arXiv  Detail & Related papers  (2026-01-30T10:33:29Z)
• Continuous Self-Improvement of Large Language Models by Test-time Training with Verifier-Driven Sample Selection [6.471199527741301]
  We introduce a new framework called VDS-TTT - Verifier-Driven Sample Selection for Test-Time Training.<n>We use a learned verifier to score a pool of generated responses and select only from high ranking pseudo-labeled examples for fine-tuned adaptation.<n>We fine-tune only low-rank LoRA adapter parameters, ensuring adaptation efficiency and fast convergence.
  arXiv  Detail & Related papers  (2025-05-26T03:54:47Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• TACRED Revisited: A Thorough Evaluation of the TACRED Relation Extraction Task [80.38130122127882]
  TACRED is one of the largest, most widely used crowdsourced datasets in Relation Extraction (RE) In this paper, we investigate the questions: Have we reached a performance ceiling or is there still room for improvement? We find that label errors account for 8% absolute F1 test error, and that more than 50% of the examples need to be relabeled.
  arXiv  Detail & Related papers  (2020-04-30T15:07:37Z)

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.