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