구조화된 신경기호 추론을 통한 다단계 프로그램의 구성적 루프 불변 추론

요약

본 논문은 다단계 프로그램의 루프 불변식 추론이라는 미해결 문제를 해결하기 위해 구조화된 신경기호 추론 프레임워크인 CLOVER를 제시합니다. CLOVER는 루프를 실행 시나리오로 구성적으로 분해하고, 각 시나리오별로 독립적인 하위 불변식을 생성하도록 LLM을 안내합니다. 또한 반례 기반 국소 정제를 통해 실패한 특정 부분만 수정하여 높은 추론 성능을 입증했습니다.

핵심 포인트

• CLOVER는 루프를 기호적 분기 시퀀스로 구성적으로 분해하는 것이 핵심입니다.
• LLM이 전체 루프가 아닌 단일 실행 시나리오에 집중하도록 유도합니다.
• 반례 기반 국소 정제를 통해 실패한 하위 불변식만 보존하며 수정할 수 있습니다.
• 54개 다단계 벤치마크 중 35개를 해결하여 기존 최고 성능을 크게 능가했습니다.