Ranking LLM-Generated Loop Invariants for Program Verification

• URL: http://arxiv.org/abs/2310.09342v3
• Date: Mon, 12 Feb 2024 20:25:31 GMT
• Title: Ranking LLM-Generated Loop Invariants for Program Verification
• Abstract summary: Large Language Models are capable of synthesizing loop invariants for a class of programs in a 0-shot setting. This can lead to a large number of calls to a program verifier to establish an invariant. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts.
• Score: 14.7590099354867
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a {\it re-ranking} approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier. The source code and the experimental data for this paper are available in \url{https://github.com/microsoft/NeuralInvariantRanker}.

Related papers

• Overcoming the Weakest-Link Effect in LLM-Driven Program Optimization via Heterogeneous Edit Recombination [59.679182823718556]
  HERO is a program that generates diverse, non-overlapping atomic edits and then systematically selects and composes them into coherent program improvements using evaluator scores.<n>We evaluate HERO across algorithmic problems, strategy games, the design of LLM-based agentic systems, and robotic path planning.
  arXiv  Detail & Related papers  (2026-07-31T02:05:45Z)
• 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)
• One Pass, Any Order: Position-Invariant Listwise Reranking for LLM-Based Recommendation [2.5827686695037335]
  Large language models (LLMs) are increasingly used for recommendation reranking, but their listwise predictions can depend on the order in which candidates are presented.<n>This creates a mismatch between the set-based nature of recommendation and the sequence-based computation of decoder-only LLMs.<n>We propose InvariRank, a permutation-invariant listwise reranking framework that addresses this dependence at the architectural level.
  arXiv  Detail & Related papers  (2026-04-30T08:49:44Z)
• 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)
• Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers [2.0686733932673604]
  We investigate whether modern, reasoning-optimized large language models can do better than symbolic approaches.<n>We integrate OpenAI's O1, O1-mini, and O3-mini into a tightly coupled generate-and-check pipeline with the Z3 SMT solver.<n>Our framework achieves 100% coverage (133 out of 133), outperforming the previous best of 107 out of 133.
  arXiv  Detail & Related papers  (2025-08-01T08:15:15Z)
• On the Query Complexity of Verifier-Assisted Language Generation [35.43462431990329]
  We develop a framework for reasoning about constrained generation using a pre-trained language model generator oracle. Access to a verifier can render an intractable problem (information-theoretically or computationally) to a tractable one. We show even simple algorithms, like tokenwise rejection sampling, can enjoy significant benefits from access to a verifier.
  arXiv  Detail & Related papers  (2025-02-17T18:46:32Z)
• Inference Scaling for Bridging Retrieval and Augmented Generation [47.091086803980765]
  Retrieval-augmented generation (RAG) has emerged as a popular approach to steering the output of a large language model (LLM) We show such bias can be mitigated, from inference scaling, aggregating inference calls from the permuted order of retrieved contexts. We showcase the effectiveness of MOI on diverse RAG tasks, improving ROUGE-L on MS MARCO and EM on HotpotQA benchmarks by 7 points.
  arXiv  Detail & Related papers  (2024-12-14T05:06:43Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• Generative Verifiers: Reward Modeling as Next-Token Prediction [29.543787728397643]
  Verifiers or reward models are often used to enhance the reasoning performance of large language models (LLMs) We propose training verifiers using the ubiquitous next-token prediction objective, jointly on verification and solution generation. We demonstrate that GenRM outperforms discriminative, DPO verifiers, and LLM-as-a-Judge.
  arXiv  Detail & Related papers  (2024-08-27T17:57:45Z)
• Code Repair with LLMs gives an Exploration-Exploitation Tradeoff [16.80314690163063]
  Iteratively improving and repairing source code with large language models (LLMs) has emerged as a popular way of generating programs that would be too complex to construct in one shot. We show here that refinement exposes an explore-exploit tradeoff: exploit by refining the program that passes the most test cases, or explore by refining a lesser considered program.
  arXiv  Detail & Related papers  (2024-05-26T04:00:30Z)
• Finding Inductive Loop Invariants using Large Language Models [14.846222005558666]
  Finding inductive loop invariants is an undecidable problem. Despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models in offering a new solution.
  arXiv  Detail & Related papers  (2023-11-14T06:58:09Z)
• Winning Prize Comes from Losing Tickets: Improve Invariant Learning by Exploring Variant Parameters for Out-of-Distribution Generalization [76.27711056914168]
  Out-of-Distribution (OOD) Generalization aims to learn robust models that generalize well to various environments without fitting to distribution-specific features. Recent studies based on Lottery Ticket Hypothesis (LTH) address this problem by minimizing the learning target to find some of the parameters that are critical to the task. We propose Exploring Variant parameters for Invariant Learning (EVIL) which also leverages the distribution knowledge to find the parameters that are sensitive to distribution shift.
  arXiv  Detail & Related papers  (2023-10-25T06:10:57Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  Large language models (LLMs) excel at implementing code from functionality descriptions but struggle with algorithmic problems. We propose ALGO, a framework that synthesizes Algorithmic programs with LLM-Generated Oracles to guide the generation and verify their correctness. Experiments show that when equipped with ALGO, we achieve an 8x better one-submission pass rate over the Codex model and a 2.6x better one-submission pass rate over CodeT.
  arXiv  Detail & Related papers  (2023-05-24T00:10:15Z)
• Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
  Large language models (LLMs) have shown strong reasoning ability in several natural language processing tasks. LLMs with chain of thought (CoT) prompting require multi-step prompting and multi-token prediction, which is highly sensitive to individual mistakes. We propose and prove that LLMs also have similar self-verification abilities.
  arXiv  Detail & Related papers  (2022-12-19T15:51:52Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  We propose fault-aware neural code rankers that can predict the correctness of a sampled program without executing it. Our fault-aware rankers can significantly increase the pass@1 accuracy of various code generation models.
  arXiv  Detail & Related papers  (2022-06-04T22:01:05Z)
• Discovering Non-monotonic Autoregressive Orderings with Variational Inference [67.27561153666211]
  We develop an unsupervised parallelizable learner that discovers high-quality generation orders purely from training data. We implement the encoder as a Transformer with non-causal attention that outputs permutations in one forward pass. Empirical results in language modeling tasks demonstrate that our method is context-aware and discovers orderings that are competitive with or even better than fixed orders.
  arXiv  Detail & Related papers  (2021-10-27T16:08:09Z)

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.