{"ID":6023960,"CreatedAt":"2026-07-08T01:00:23.257252134Z","UpdatedAt":"2026-07-09T14:33:30.924921582Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.05478","arxiv_id":"2607.05478","title":"InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs","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.","short_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 frame...","url_abs":"https://arxiv.org/abs/2607.05478","url_pdf":"https://arxiv.org/pdf/2607.05478v1","authors":"[\"Guangyuan Wu\",\"Weining Cao\",\"Zehui Tan\",\"Yuan Yao\",\"Hengfeng Wei\",\"Taolue Chen\",\"Xiaoxing Ma\"]","published":"2026-07-06T14:36:36Z","proceeding":"cs.LG","tasks":"[\"cs.LG\",\"cs.PL\"]","methods":"[\"Large Language Model\"]","has_code":false}