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

Guangyuan Wu; Weining Cao; Zehui Tan; Yuan Yao; Hengfeng Wei; Taolue Chen; Xiaoxing Ma

cs.LGJul 6, 2026

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

Authors: Guangyuan Wu, Weining Cao, Zehui Tan, Yuan Yao, Hengfeng Wei, Taolue Chen, Xiaoxing Ma

Organizations: Nanjing University · Nanjing, China · Hunan University · Changsha, China · Birkbeck, University of London

Abstract

Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have shown strong performance on single-loop programs, but they often struggle with programs containing multiple interacting loops. This paper presents InvWeaver, a neuro-symbolic framework for synthesizing invariants for such programs. The key idea is to expose inter-loop dependencies and propagate proof obligations through a combination of loop-level abstraction, obligation-guided inference, and weakest-precondition-based refinement. We evaluate InvWeaver on a comprehensive benchmark suite, including a newly curated dataset derived from classic algorithms. Experimental results show that InvWeaver substantially outperforms existing invariant inference methods, solving 72 out of 82 multi-loop benchmark problems and maintaining strong performance on single-loop tasks.

Explore similar work

Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
Mar 16, 2026Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu +2Small Language Models Verifier
Certified Program Synthesis with a Multi-Modal Verifier
Apr 17, 2026Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein +5Mock-Interface Synthesis Verifier
Invariant Discovery for Networked Systems
Jul 24, 2026Hongyu Hè, Alexander Krentsel, Sylvia Ratnasamy +1Automatic Identification System Intrusion Detection

Mar 16, 2026 · cs.LGJ/K move · Enter open · S save

Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs

Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu, Nina Narodytska+1

Hebrew University of Jerusalem, Israel · Amherst Col · VMware Research by Broadcom, USA.

The synthesis of inductive loop invariants remains a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue, they often fail on complex programs, producing invariants that are invalid or computationally ineffective. Although fine-tuning is a natural strategy to address these limitations, obtaining high-quality training data remains an open challenge. We first formalize the properties required for a high-quality training invariant, and then present Wonda, a rigorous data curation pipeline that extracts such invariants from raw verifier output via AST-based normalization followed by LLM-driven semantic rewriting and augmentation with provable quality guarantees. Fine-tuning Small Language Models (SLMs) on Wonda-curated data yields consistent gains across the Qwen3, Llama-3.1, and Mistral families: the 4B and 8B Qwen3 models nearly double invariant correctness and double speedup rates, while Llama-3.1-8B triples both. On the challenging InvBench suite, the same 4B model outperforms an off-the-shelf model 20x its size and matches the end-to-end verification time of GPT-OSS-120B, while a 14B Qwen3 model matches that of the frontier model GPT-5.2, all without test-time compute overhead. Our code is publicly available on GitHub.

Small Language Models Verifier Training Data Invariance

Open paper Ask about it PDF

Abstract

Explore similar work

Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs

Certified Program Synthesis with a Multi-Modal Verifier

Invariant Discovery for Networked Systems