Search papers, labs, and topics across Lattice.
This paper introduces LimICE, an innovative framework that integrates large language models (LLMs) into the Incremental Counterexample-based Invariant Learning (ICE) framework to enhance loop invariant synthesis. By employing a lemma-specific learning objective and a counterexample filtering mechanism, LimICE effectively generates ordered sequences of lemmas, achieving significant improvements in both the number of problems solved and execution speed compared to existing methods. Experimental results show that LimICE solves 349 out of 367 linear benchmarks and 47 out of 50 nonlinear benchmarks, outperforming state-of-the-art LLM-based and non-LLM baselines by 12-24% in instance resolution while being 36-63% faster.
LimICE not only solves more loop invariant problems but does so significantly faster, redefining efficiency benchmarks in program verification.
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.
