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

TL;DR

This paper presents a hybrid framework combining reasoning-optimized large language models and SMT solvers to automatically synthesize loop invariants, achieving perfect coverage on a standard benchmark with minimal proposals and time.

Contribution

The work introduces a novel hybrid approach that leverages LLMs and SMT solvers for loop invariant generation, surpassing previous methods in coverage and efficiency.

Findings

Achieved 100% coverage on Code2Inv benchmark with 133 tasks.

Outperformed previous best by synthesizing invariants for all tasks.

Required only 1-2 model proposals per task, taking 14-55 seconds.

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.