본 논문은 복잡한 데이터 구조와 제어 흐름을 포함하는 실제 프로그램에 대한 루프 불변식 생성 문제를 해결하기 위해, 정적 분석과 대규모 언어 모델(LLM)을 결합한 자동화된 루프 불변식 생성 도구 ACInv를 제안합니다. ACInv는 정적 분석을 통해 각 루프에 필요한 정보를 추출하여 LLM 프롬프트에 포함하고, LLM을 이용하여 루프 불변식을 생성합니다. 생성된 불변식은 LLM 기반 평가기를 통해 검증하고, 정확성에 따라 강화, 약화 또는 거부하여 개선된 불변식을 얻습니다. 실험 결과, ACInv는 데이터 구조를 포함하는 데이터 세트에서 기존 도구보다 성능이 우수하며, 데이터 구조가 없는 수치 프로그램에서는 최첨단 도구 AutoSpec과 유사한 성능을 유지했습니다. 전체 데이터 세트에서 ACInv는 AutoSpec보다 21% 더 많은 예제를 해결하고 참조 데이터 구조 템플릿을 생성할 수 있었습니다.
