Loop invariant inference is a fundamental yet challenging problem in program verification. Recent LLM-aided guess-and-check techniques have demonstrated strong performance on single-loop programs, but struggle with multi-loop programs (e.g., multiple nested and/or sequential loops), which are prevalent in classic algorithms and real-world programs. In this paper, we present InvWeaver, a novel neuro-symbolic framework that synthesizes invariants for multi-loop programs. The key insight is to explicitly expose inter-loop dependencies and systematically propagate proof obligations through a principled combination of abstraction and deductive reasoning. We evaluate InvWeaver on a comprehensive benchmark suite, including a newly curated dataset derived from classic algorithms. Experimental results show that InvWeaver substantially outperforms the existing methods. In particular, InvWeaver solves 72 out of 82 multi-loop benchmark problems, exceeding the strongest competitor by 32 problems, while maintaining superior performance on single-loop tasks.
