LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference

• URL: http://arxiv.org/abs/2607.27606v1
• Date: Thu, 30 Jul 2026 02:50:09 GMT
• Title: LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference
• Abstract summary: 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.
• Score: 10.534386090450276
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Loop invariant synthesis is a fundamental problem in program verification, yet the inherent undecidability makes it highly challenging. Recent studies have increasingly employed various machine learning techniques to generate loop invariants. However, most of these methods adopt a monolithic approach. Due to the inability to strictly constrain the learning process, learning-based methods struggle to simultaneously consider all necessary conditions and generate complete invariants when tackling complex problems. In fact, a loop invariant is often an ordered sequence of lemmas, rather than a single invariant formula. This motivates us to propose Incremental ICE, a novel learning framework for incremental synthesis. Our framework integrates the incremental philosophy of IC3 into the general invariant learning framework ICE. By defining a lemma-specific learning objective and introducing a counterexample filtering mechanism, we can achieve sound incremental learning. Under this framework, we instantiate a loop invariant synthesis tool, LimICE, which leverages LLMs to generate the ordered sequence of lemmas and incorporates ICE-DT as a fallback mechanism to complement the lemma sequence. Experiments on 367 linear benchmarks and 50 nonlinear benchmarks demonstrate the effectiveness of the proposed approach. LimICE solves 349 (out of 367) linear problems on an average of 15.2 seconds and 47 (out of 50) nonlinear problems on an average of 8.8 seconds. Compared to the state-of-the-art LLM-based baseline, our approach solves 12-24% more instances while running 36-63% faster across linear and nonlinear benchmarks. LimICE also consistently outperforms strong non-LLM baselines and solves at least 86 and 27 additional instances on the linear and nonlinear benchmarks, respectively.

Related papers

• SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification [2.6426981014417046]
  We introduce SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification.<n>We also introduce NLEquiv-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs.
  arXiv  Detail & Related papers  (2026-09-01T05:05:12Z)
• Not All Problems Are Best Modeled as MILP: A DSL-Centric Framework for Flexible and Accurate Optimization Modeling [18.793227025879993]
  We propose Opti, a framework that shifts the focus from rigid MILP formulations to domain-specific language representations.<n>By utilizing LLMs to map natural language onto standardized, domain-accepted structures, Opti decouples problem formulation from execution.
  arXiv  Detail & Related papers  (2026-08-07T09:50:52Z)
• Scaling Self-Play with Self-Guidance [62.13619253976748]
  Self-Guided Self-Play (SGS) is a self-play algorithm that guides the Conjecturer away from degeneracy.<n>SGS surpasses the solve rate of our strongest baseline in fewer than 80 rounds of self-play.
  arXiv  Detail & Related papers  (2026-04-22T05:50:23Z)
• $\ abla$-Reasoner: LLM Reasoning via Test-Time Gradient Descent in Latent Space [71.23672814629448]
  $nabla$-Reasoner is an iterative generation framework that integrates differentiable optimization over token logits into the decoding loop.<n>$nabla$-Reasoner achieves over 20% accuracy improvement on a challenging mathematical reasoning benchmark.
  arXiv  Detail & Related papers  (2026-03-05T08:42:54Z)
• Para-B&B: Load-Balanced Deterministic Parallelization of Solving MIP [50.917107318582715]
  Mixed-integer programming (MIP) extends linear programming by incorporating both continuous and integer decision variables.<n>This paper presents the first fully open-source implementation of deterministic parallel branch-and-bound for HiGHS, a high-performance MIP solver.<n>Our approach introduces a novel data-parallel architecture ensuring strict determinism by replicating complete solver state across worker threads.
  arXiv  Detail & Related papers  (2026-02-10T14:17:53Z)
• Inference-Aware Meta-Alignment of LLMs via Non-Linear GRPO [55.574265038358455]
  Inference-aware meta-alignment (IAMA) is a novel approach to align large language models to diverse human preferences.<n>IAMA trains a base model such that it can be effectively aligned to multiple tasks via different inference-time alignment algorithms.<n>We propose non-linear GRPO, which provably converges to the optimal solution in the space of probability measures.
  arXiv  Detail & Related papers  (2026-02-02T03:50:42Z)
• 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)
• OptiBench Meets ReSocratic: Measure and Improve LLMs for Optimization Modeling [62.19438812624467]
  Large language models (LLMs) have exhibited their problem-solving abilities in mathematical reasoning.<n>We propose OptiBench, a benchmark for End-to-end optimization problem-solving with human-readable inputs and outputs.
  arXiv  Detail & Related papers  (2024-07-13T13:27:57Z)
• Reinforcement Learning for Branch-and-Bound Optimisation using Retrospective Trajectories [72.15369769265398]
  Machine learning has emerged as a promising paradigm for branching. We propose retro branching; a simple yet effective approach to RL for branching. We outperform the current state-of-the-art RL branching algorithm by 3-5x and come within 20% of the best IL method's performance on MILPs with 500 constraints and 1000 variables.
  arXiv  Detail & Related papers  (2022-05-28T06:08:07Z)
• Multiblock ADMM for nonsmooth nonconvex optimization with nonlinear coupling constraints [3.2815423235774634]
  We propose a method of multipliers for solving a class of multiblock nonsmooth alternating optimization problem with nonlinear constraints. We employ a major sequenceization procedure in update of each block of the primal variables.
  arXiv  Detail & Related papers  (2022-01-19T15:31:30Z)
• 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.