INVWEAVER: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs

Loop invariant inference is essential for formal program verification, but existing LLM-aided approaches struggle with programs containing multiple interacting loops. These methods often suffer from local under-specification, where intermediate loops lack sufficient context to capture global semantic dependencies, leading to the generation of invariants that are locally plausible but globally insufficient. This paper asks: how can we systematically integrate deductive reasoning with LLM-based inference to synthesize correct invariants for complex, multi-loop programs?

The authors introduce InvWeaver, a neuro-symbolic framework that models programs using a Loop-level Call Graph (LCG). The LCG explicitly maps inter-loop dependencies and state transitions, providing a structured context for the inference process. InvWeaver employs an obligation-guided strategy where the Weakest Precondition (WP) calculus is used to identify specific proof failures. When a candidate invariant fails verification, the system uses these failures as explicit repair targets, propagating proof obligations across loop boundaries. This allows the LLM to refine invariants in a way that ensures consistency across the entire loop hierarchy, rather than treating each loop as an isolated problem.

InvWeaver was evaluated on a comprehensive benchmark suite, including a newly curated dataset derived from classic algorithms (e.g., sorting, dynamic programming, and graph algorithms). The results show that InvWeaver solves 72 out of 82 multi-loop benchmark problems, which is 32 more than the strongest competing method. The framework also maintains high performance on single-loop tasks, demonstrating that the LCG-based approach effectively bridges the contextual gap in multi-loop reasoning.

By successfully handling multi-loop structures, InvWeaver addresses a major bottleneck in automated formal verification. Its ability to generate expressive invariants for complex algorithms makes it a significant step toward verifying real-world software that relies on nested or sequential loop structures, where manual invariant annotation is often prohibitively difficult.