루프 불변성(Loop invariant) 추론은 프로그램 검증에서 근본적이면서도 어려운 문제입니다. 최근 LLM 기반의 추측 및 확인(guess-and-check) 기법들은 단일 루프 프로그램에서는 강력한 성능을 보여주었지만, 여러 개의 상호작용하는 루프를 포함하는 프로그램에는 종종 어려움을 겪습니다. 본 논문은 이러한 프로그램에 대한 불변성을 합성하기 위한 신경-기호적(neuro-symbolic) 프레임워크인 InvWeaver를 제시합니다. 핵심 아이디어는 루프 수준의 추상화, 의무(obligation)-유도 추론, 그리고 가장 약한 전제 조건 기반 정제(weakest-precondition-based refinement) 조합을 통해 루프 간 종속성을 노출하고 증명 의무(proof obligation)를 전파하는 것입니다. 우리는 클래식 알고리즘에서 파생된 새로 큐레이션된 데이터셋을 포함하여 포괄적인 벤치마크 스위트에서 InvWeaver를 평가했습니다. 실험 결과는 InvWeaver가 기존의 불변성 추론 방법들보다 현저히 우수하며, 82개의 멀티-루프 벤치마크 문제 중 72개를 해결하고 단일 루프 작업에서도 강력한 성능을 유지함을 보여줍니다.