Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers

• URL: http://arxiv.org/abs/2508.00419v1
• Date: Fri, 01 Aug 2025 08:15:15 GMT
• Title: Loop Invariant Generation: A Hybrid Framework of Reasoning optimised LLMs and SMT Solvers
• Abstract summary: 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.
• Score: 2.0686733932673604
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Loop invariants are essential for proving the correctness of programs with loops. Developing loop invariants is challenging, and fully automatic synthesis cannot be guaranteed for arbitrary programs. Some approaches have been proposed to synthesize loop invariants using symbolic techniques and more recently using neural approaches. These approaches are able to correctly synthesize loop invariants only for subsets of standard benchmarks. In this work, we investigate whether modern, reasoning-optimized large language models can do better. We integrate OpenAI's O1, O1-mini, and O3-mini into a tightly coupled generate-and-check pipeline with the Z3 SMT solver, using solver counterexamples to iteratively guide invariant refinement. We use Code2Inv benchmark, which provides C programs along with their formal preconditions and postconditions. On this benchmark of 133 tasks, our framework achieves 100% coverage (133 out of 133), outperforming the previous best of 107 out of 133, while requiring only 1-2 model proposals per instance and 14-55 seconds of wall-clock time. These results demonstrate that LLMs possess latent logical reasoning capabilities which can help automate loop invariant synthesis. While our experiments target C-specific programs, this approach should be generalizable to other imperative languages.

Related papers

• LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference [10.534386090450276]
  We propose Incremental ICE, a novel learning framework for incremental synthesis.<n>Our framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE.<n>Under this framework, we instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas.
  arXiv  Detail & Related papers  (2026-07-30T02:50:09Z)
• Parallelizable Exact Synthesis of Quantum Circuits via Semi-Tensor Product [5.247996019685446]
  This paper introduces an exact framework for CNOT and undirected phase circuits.<n>By enumerating partial-gate topologies and solving the missing gate directions separately, we are able to parallelize both stages.<n>Our algorithm outperforms the SAT-based approach on 89% of cases in QASM.
  arXiv  Detail & Related papers  (2026-07-27T09:14:53Z)
• Protean Compiler: An Agile Framework to Drive Fine-grain Phase Ordering [2.5829132714658067]
  Protean Compiler is an agile framework to enable LLVM with built-in phase-ordering capabilities at a fine-grained scope.<n>The framework also comprises a complete library of more than 140 handcrafted static feature collection methods at varying scopes.<n>This paper showcases speedup gains of up to 4.1% on average and up to 15.7% on select Cbench applications wrt LLVM's O3.
  arXiv  Detail & Related papers  (2026-02-05T19:24:05Z)
• Provably Optimal Quantum Circuits with Mixed-Integer Programming [0.0]
  We present a depth-aware optimization framework for quantum circuit compilation.<n>For exact synthesis of a target unitary, we formulate a mixed-integer linear program (MILP) that linearly global-phase equivalence.<n>To scale beyond exact MILP, we propose a novel rolling-Circuit optimization (RHO) that rolls primarily in time, caps the active-qubits, and enforces per-qubit closure.
  arXiv  Detail & Related papers  (2025-10-01T08:25:43Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [18.40402135952776]
  This paper presents SymRTLO, a novel neuron-symbolic RTL optimization framework.<n>A symbolic module is proposed for analyzing and optimizing finite state machine (FSM) logic.<n> Experiments on the RTL-Rewriter benchmark with Synopsys Design Compiler and Yosys show that SymRTLO improves power, performance, and area (PPA) by up to 43.9%, 62.5%, and 51.1%, respectively.
  arXiv  Detail & Related papers  (2025-04-14T16:15:55Z)
• Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
  We introduce QAlign, a new test-time alignment approach.<n>As we scale test-time compute, QAlign converges to sampling from the optimal aligned distribution for each individual prompt.<n>By adopting recent advances in Markov chain Monte Carlo for text generation, our method enables better-aligned outputs without modifying the underlying model or even requiring logit access.
  arXiv  Detail & Related papers  (2025-04-04T00:41:40Z)
• Fully Autonomous Programming using Iterative Multi-Agent Debugging with Large Language Models [8.70160958177614]
  Program synthesis with Large Language Models (LLMs) suffers from a "near-miss syndrome"<n>We address this with a multi-agent framework called Synthesize, Execute, Instruct, Debug, and Repair (SEIDR)<n>We empirically explore these trade-offs by comparing replace-focused, repair-focused, and hybrid debug strategies.
  arXiv  Detail & Related papers  (2025-03-10T16:56:51Z)
• EquiBench: Benchmarking Large Language Models' Understanding of Program Semantics via Equivalence Checking [55.81461218284736]
  EquiBench is a new benchmark for evaluating large language models (LLMs)<n>It determines whether two programs produce identical outputs for all possible inputs.<n>We evaluate 19 state-of-the-art LLMs and find that the best accuracies are 63.8% and 76.2%, only modestly above the 50% random baseline.
  arXiv  Detail & Related papers  (2025-02-18T02:54:25Z)
• Ranking LLM-Generated Loop Invariants for Program Verification [14.7590099354867]
  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.
  arXiv  Detail & Related papers  (2023-10-13T18:13:52Z)
• 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)
• AMOM: Adaptive Masking over Masking for Conditional Masked Language Model [81.55294354206923]
  A conditional masked language model (CMLM) is one of the most versatile frameworks. We introduce a simple yet effective adaptive masking over masking strategy to enhance the refinement capability of the decoder. Our proposed model yields state-of-the-art performance on neural machine translation.
  arXiv  Detail & Related papers  (2023-03-13T20:34:56Z)
• A Fully Single Loop Algorithm for Bilevel Optimization without Hessian Inverse [121.54116938140754]
  We propose a new Hessian inverse free Fully Single Loop Algorithm for bilevel optimization problems. We show that our algorithm converges with the rate of $O(epsilon-2)$.
  arXiv  Detail & Related papers  (2021-12-09T02:27:52Z)
• Enabling Retargetable Optimizing Compilers for Quantum Accelerators via a Multi-Level Intermediate Representation [78.8942067357231]
  We present a multi-level quantum-classical intermediate representation (IR) that enables an optimizing, retargetable, ahead-of-time compiler. We support the entire gate-based OpenQASM 3 language and provide custom extensions for common quantum programming patterns and improved syntax. Our work results in compile times that are 1000x faster than standard Pythonic approaches, and 5-10x faster than comparative standalone quantum language compilers.
  arXiv  Detail & Related papers  (2021-09-01T17:29:47Z)
• A Reinforcement Learning Environment for Polyhedral Optimizations [68.8204255655161]
  We propose a shape-agnostic formulation for the space of legal transformations in the polyhedral model as a Markov Decision Process (MDP) Instead of using transformations, the formulation is based on an abstract space of possible schedules. Our generic MDP formulation enables using reinforcement learning to learn optimization policies over a wide range of loops.
  arXiv  Detail & Related papers  (2021-04-28T12:41:52Z)
• Static Neural Compiler Optimization via Deep Reinforcement Learning [1.458855293397494]
  In this paper, we employ a deep reinforcement learning approach to the phase-ordering problem. Provided with sub-sequences constituting LLVM's O3 sequence, our agent learns to outperform the O3 sequence on the set of source codes used for training. We believe that the models trained using our approach can be integrated into modern compilers as neural optimization agents.
  arXiv  Detail & Related papers  (2020-08-20T13:16:29Z)
• Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version) [19.87276407545565]
  We introduce a new neural architecture for general SMT learning, the Gated Continuous Logic Network (G-CLN) G-CLNs extend the Continuous Logic Network (CLN) architecture with gating units and dropout. We show G-CLNs have a convergence rate of $97.5%$ on quadratic problems, a $39.2%$ improvement over CLN models.
  arXiv  Detail & Related papers  (2020-03-17T21:44: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.