InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis?

• URL: http://arxiv.org/abs/2509.21629v1
• Date: Thu, 25 Sep 2025 21:47:02 GMT
• Title: InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis?
• Abstract summary: We introduce a principled framework for evaluating LLMs on invariant synthesis.<n>Our approach uses a verifier-based decision procedure with a formal soundness guarantee.<n>We evaluate 7 state-of-the-art LLMs, and existing LLM-based verifiers against the traditional solver UAutomizer.
• Score: 13.240989975977302
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Program verification relies on loop invariants, yet automatically discovering strong invariants remains a long-standing challenge. We introduce a principled framework for evaluating LLMs on invariant synthesis. Our approach uses a verifier-based decision procedure with a formal soundness guarantee and assesses not only correctness but also the speedup that invariants provide in verification. We evaluate 7 state-of-the-art LLMs, and existing LLM-based verifiers against the traditional solver UAutomizer. While LLM-based verifiers represent a promising direction, they do not yet offer a significant advantage over UAutomizer. Model capability also proves critical, as shown by sharp differences in speedups across models, and our benchmark remains an open challenge for current LLMs. Finally, we show that supervised fine-tuning and Best-of-N sampling can improve performance: fine-tuning on 3589 instances raises the percentage of speedup cases for Qwen3-Coder-480B from 8% to 29.2%, and Best-of-N sampling with N=16 improves Claude-sonnet-4 from 8.8% to 22.1%.

Related papers

• LLM-as-a-Verifier: A General-Purpose Verification Framework [74.40111651545979]
  We introduce LLM-as-a-Verifier, a general-purpose verification framework.<n>It provides fine-grained feedback for agentic tasks without requiring additional training.<n>It achieves state-of-the-art performance on several benchmarks.
  arXiv  Detail & Related papers  (2026-07-06T17:59:35Z)
• Mitigating Spurious Correlations in NLI via LLM-Synthesized Counterfactuals and Dynamic Balanced Sampling [0.0]
  Natural Language Inference (NLI) models frequently rely on spurious correlations rather than semantic reasoning.<n>Existing mitigation strategies often incur high annotation costs or trigger catastrophic forgetting during fine-tuning.<n>We propose an automated, scalable pipeline to address these limitations.
  arXiv  Detail & Related papers  (2025-12-20T18:30:54Z)
• LLM For Loop Invariant Generation and Fixing: How Far Are We? [9.510531513586322]
  The identification of loop invariants is a critical step to support automated program safety assessment.<n>Recent advancements in Large Language Models have demonstrated potential in diverse software engineering (SE) and formal verification tasks.<n>We report an empirical study of both open-source and closed-source LLMs of varying sizes to assess their proficiency in inferring inductive loop invariants for programs and in fixing incorrect invariants.
  arXiv  Detail & Related papers  (2025-11-09T21:47:45Z)
• Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
  We propose a lightweight alternative for step-level reasoning verification based on data-driven uncertainty scores.<n>Our findings suggest that the internal states of LLMs encode their uncertainty and can serve as reliable signals for reasoning verification.
  arXiv  Detail & Related papers  (2025-11-09T03:38:29Z)
• LaSeR: Reinforcement Learning with Last-Token Self-Rewarding [54.72617309922891]
  Reinforcement Learning with Verifiable Rewards (RLVR) has emerged as a core paradigm for enhancing the reasoning capabilities of Large Language Models (LLMs)<n>Previous practice requires the LLM to sequentially generate solutions and self-verifications using two separate prompt templates, which significantly reduces efficiency.<n>We propose LaSeR (Reinforcement Learning with Last-Token Self-Rewarding), an algorithm that simply augments the original RLVR loss with a MSE loss.
  arXiv  Detail & Related papers  (2025-10-16T17:55:11Z)
• MCTS-Refined CoT: High-Quality Fine-Tuning Data for LLM-Based Repository Issue Resolution [18.314436803012434]
  The paper proposes MCTS-INE, an enhanced Monte Carlo Tree Search (MCTS)-based algorithm that dynamically validates and optimize intermediate reasoning steps.<n> Experiments on SWE-bench Lite and SWE-bench Verified demonstrate that LLMs fine-tuned with our CoT dataset achieve substantial improvements over baselines.
  arXiv  Detail & Related papers  (2025-06-15T05:42:01Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [8.056359341994941]
  APOLLO is a modelagnostic pipeline that combines the strengths of the Lean compiler with an LLM's reasoning abilities.<n>A set of agents analyze the proofs, fix the syntax errors, identify the mistakes in the proofs using Lean.<n>The repaired subproofs are recombined and reverified, iterating up to a usercontrolled maximum number of attempts.
  arXiv  Detail & Related papers  (2025-05-09T03:38:31Z)
• LLM2: Let Large Language Models Harness System 2 Reasoning [65.89293674479907]
  Large language models (LLMs) have exhibited impressive capabilities across a myriad of tasks, yet they occasionally yield undesirable outputs.<n>We introduce LLM2, a novel framework that combines an LLM with a process-based verifier.<n>LLMs2 is responsible for generating plausible candidates, while the verifier provides timely process-based feedback to distinguish desirable and undesirable outputs.
  arXiv  Detail & Related papers  (2024-12-29T06:32:36Z)
• Language Models are Hidden Reasoners: Unlocking Latent Reasoning Capabilities via Self-Rewarding [74.31981011985681]
  Large language models (LLMs) have shown impressive capabilities, but still struggle with complex reasoning tasks requiring multiple steps. We introduce LaTent Reasoning Optimization (LaTRO), a principled framework that formulates reasoning as sampling from a latent distribution. We validate LaTRO through experiments on GSM8K and ARC-Challenge datasets using multiple model architectures.
  arXiv  Detail & Related papers  (2024-11-06T22:02:30Z)
• Enhancing Mathematical Reasoning in LLMs by Stepwise Correction [39.67266805233599]
  Best-of-N decoding methods instruct large language models (LLMs) to generate multiple solutions, score each using a scoring function, and select the highest scored as the final answer to mathematical reasoning problems. We propose a novel prompting method named Stepwise Correction (StepCo) that helps LLMs identify and revise incorrect steps in their generated reasoning paths. The verify-then-revise process not only improves answer correctness but also reduces token consumption with fewer paths needed to generate.
  arXiv  Detail & Related papers  (2024-10-16T18:18:42Z)
• Adaptive Inference-Time Compute: LLMs Can Predict if They Can Do Better, Even Mid-Generation [51.127054971591924]
  We introduce a new generative self-evaluation scheme designed to adaptively reduce the number of generated samples. We demonstrate that 74% of the improvement from using 16 samples can be achieved with only 1.2 samples on average.
  arXiv  Detail & Related papers  (2024-10-03T17:47:29Z)
• Generative Verifiers: Reward Modeling as Next-Token Prediction [29.543787728397643]
  We propose training verifiers using the ubiquitous next-token prediction objective, jointly on verification and solution generation.<n>Compared to standard verifiers, such generative verifiers (GenRM) can benefit from several advantages of LLMs.<n>We observe improvements of 28% $rightarrow$ 44.6% on MATH, and 37.9% $rightarrow$ 53.5% on MMLU abstract algebra.
  arXiv  Detail & Related papers  (2024-08-27T17:57:45Z)
• Let's Sample Step by Step: Adaptive-Consistency for Efficient Reasoning and Coding with LLMs [60.58434523646137]
  A popular approach for improving the correctness of output from large language models (LLMs) is Self-Consistency. We introduce Adaptive-Consistency, a cost-efficient, model-agnostic technique that dynamically adjusts the number of samples per question. Our experiments show that Adaptive-Consistency reduces sample budget by up to 7.9 times with an average accuracy drop of less than 0.1%.
  arXiv  Detail & Related papers  (2023-05-19T17:49:25Z)

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.