Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors

TL;DR

This paper introduces LORIS, a framework that enhances LLMs in loop invariant synthesis by providing targeted feedback based on formal verification of reasoning steps, significantly improving success rates.

Contribution

It presents a novel feedback mechanism for LLMs that detects local reasoning errors via formal verification, leading to more accurate loop invariant synthesis.

Findings

LORIS solved 93.1% of the main benchmark programs.

The approach is robust on non-linear property benchmarks.

Formal verification of reasoning steps improves LLM performance.

Abstract

We propose a novel framework that provides constructive feedback to an LLM in the "guess-and-check" paradigm by formally verifying its own thinking process and detecting local reasoning errors. We apply this framework to the loop invariant synthesis problem. We prompt the model to produce a step-by-step natural language proof justifying its thinking process for the failed verification condition of its generated loop invariants. Then, we use an LLM to translate the reasoning steps into first-order logic implications, which can be checked automatically. An invalid implication pinpoints the exact logical flaw in the LLM's thinking process, which we then use to construct targeted feedback for refinement. We have implemented our approach in a tool called LORIS and evaluated it on a main benchmark suite of 460 C programs and an additional benchmark suite of 50 C programs each of which involves non-linear properties. On the main benchmark suite, LORIS solved 445 of the programs, and achieved an overall success rate of $93.1\%$. LORIS also demonstrates robustness on the challenging non-linear benchmark suite.