Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

1. 문제 정의 (Problem)

프로그램 검증 (Program Verification) 은 소프트웨어가 의도한 대로 동작함을 형식적으로 보장하는 과정으로, 안전이 중요한 분야에서 필수적입니다. 이 과정에서 루프 불변식 (Loop Invariant) 의 자동 발견은 40 년 이상 해결되지 않은 핵심 난제입니다.

• 불변식의 중요성: 불변식은 루프의 각 반복 전후에 성립하는 조건으로, 검증의 핵심입니다. 단순히 '올바른 (Correct)' 불변식 (예: 항상 참인 조건) 을 찾는 것은 쉽지만, 검증 속도를 높이고 최종 명세를 증명할 수 있을 만큼 충분히 강력한 (Strong) 불변식을 찾는 것은 매우 어렵습니다.
• 기존 접근법의 한계:
  • 전통적 방법: 제약 조건 해결 (Constraint Solving), 추상 해석 (Abstract Interpretation) 등이 있으나 계산 비용이 크거나 정교한 설정이 필요합니다.
  • LLM 기반 기존 연구 (Pei et al., 2023 등): LLM 이 생성한 불변식을 검증할 때, Daikon(동적 분석 도구) 과 같은 도구를 사용하여 정확성을 확인하거나, 복잡한 후처리 (필터링, 재조합, Houdini 알고리즘 등) 를 거쳐야 했습니다. 이는 LLM 출력을 '노이즈가 많은 기호 자료'로 간주하여 과도한 보정 로직을 필요로 했으며, 동적 분석 기반의 검증은 형식적 무결성 (Soundness) 을 보장하지 못했습니다.

2. 방법론 (Methodology)

저자들은 Quokka라는 새로운 프레임워크를 제안합니다. 이는 LLM 기반 불변식 합성을 위한 평가 중심 (Evaluation-oriented) 설계로, 복잡한 후처리 대신 검증기 (Verifier) 와의 직접적인 상호작용을 통해 불변식의 유효성과 유용성을 즉시 판단합니다.

핵심 구성 요소

1. 검증기 기반 평가 알고리즘 (Verifier-Based Approach):

   • LLM 이 제안한 후보 불변식 $q$에 대해 두 가지 검증 쿼리를 병렬로 실행합니다.
     • $d_a$ (정확성 확인): $q$가 실제 루프 불변식인지 검증합니다.
     • $d_b$ (유용성 확인): $q$를 가정 (Assume) 으로 추가했을 때, 목표 속성 (Target Assertion) 이 증명되는지 검증합니다.
   • 이 방식은 LLM 출력을 복잡한 논리 연산으로 재구성하는 대신, 검증기가 직접 "이 불변식이 증명에 도움이 되는가?"를 판단하게 합니다.
   • 무결성 (Soundness): 검증기 (UAutomizer) 의 결과에 기반하므로, 증명된 결과는 형식적으로 보장됩니다.

2. 데이터셋 구축:

   • 평가 벤치마크: SV-COMP(소프트웨어 검증 대회) 최신 버전에서 파생된 866 개의 인스턴스로 구성된 대규모 데이터셋을 구축했습니다. 기존 연구보다 더 긴 코드, 다중 루프, 함수, 배열/포인터 등을 포함하여 난이도가 높습니다.
   • 학습 데이터: 검증기 기반 필터링을 통해 3,589 개의 합성 프로그램을 생성하고, 여기서 추출된 정답 불변식을 사용하여 Supervised Fine-Tuning (SFT) 데이터를 준비했습니다.

3. 성능 향상 기법:

   • Supervised Fine-Tuning (SFT): LoRA 를 사용하여 도메인 특화 학습을 수행했습니다.
   • Best-of-N Sampling: 여러 개의 후보 불변식을 생성하고, 검증 시간을 기준으로 가장 효과적인 하나를 선택하는 전략을 적용했습니다.

3. 주요 기여 (Key Contributions)

1. Quokka 프레임워크: LLM 생성 불변식을 검증하기 위해 복잡한 후처리 로직을 제거하고, 검증기 쿼리를 통해 직접 유효성과 증명 가속화 효과를 평가하는 간결하고 무결성이 보장된 (Sound) 프레임워크를 제안했습니다.
2. 대규모 벤치마크: 866 개의 인스턴스로 구성된 새로운 평가 세트를 공개했으며, 이는 현재까지 LLM 기반 검증기 평가에 사용된 데이터셋 중 가장 규모가 크고 복잡합니다.
3. 성능 검증 및 최적화: 9 가지 최신 LLM 을 평가하고, SFT 와 Best-of-N 샘플링이 검증 가속화에 유의미한 개선을 가져온 것을 실증했습니다.

4. 실험 결과 (Results)

• 모델 성능 비교: 9 가지 LLM (Llama, Qwen, Claude, GPT 시리즈 등) 을 평가한 결과, 모델 크기와 최신성이 성능과 비례하는 경향을 보였습니다. 가장 강력한 모델인 gpt-5.2는 60 초 타임아웃 기준 710 개의 올바른 불변식을 생성하고, 베이스 솔버 (UAutomizer) 가 풀지 못한 21 개의 인스턴스를 추가로 해결했습니다.
• 기존 연구 대비 우위:
  • LaM4Inv, Clause2Inv, LEMUR, Loopy 등 기존 LLM 기반 검증기들과 비교했을 때, Quokka 는 모든 타임아웃 구간 (30s ~ 500s) 에서 가장 많은 인스턴스를 해결하고 평균 해결 시간을 단축했습니다.
  • 특히 복잡한 다중 루프 프로그램에서 Quokka 의 단순한 접근 방식이 기존 연구들의 복잡한 탐색 전략보다 더 효과적이었습니다.
• 기법별 효과:
  • SFT: Qwen2.5-7B 모델에 미세 조정을 적용하면 정확성과 해결 인스턴스 수에서 소폭의 개선을 보였습니다.
  • Best-of-N: $N=8$일 때 최적의 성능을 보였으며, 추가적인 샘플링은 리소스 경쟁으로 인해 효과가 감소했습니다.
• 실패 모드 분석: 대부분의 실패는 불변식 자체의 오류가 아니라, 검증 시간 초과 (Timeout) 때문이었습니다. 이는 LLM 이 생성한 불변식이 논리적으로 올바르더라도, 검증기가 이를 처리하는 데 시간이 너무 오래 걸리는 경우가 많음을 시사합니다.

5. 의의 및 결론 (Significance)

• 패러다임 전환: 기존 연구가 LLM 출력을 '수정해야 할 노이즈'로 간주하고 복잡한 알고리즘으로 보정하려 했던 것과 달리, Quokka 는 **"검증기가 직접 판단하게 하라"**는 간결한 철학을 제시합니다. 모델의 능력이 향상됨에 따라 복잡한 후처리 대신 직접적인 검증이 더 효율적임을 증명했습니다.
• 새로운 SOTA 달성: Quokka 는 LLM 기반 프로그램 검증 분야에서 새로운 State-of-the-Art (SOTA) 를 달성했으며, 향후 연구에 대한 원칙적인 기초를 제공했습니다.
• 확장성: UAutomizer 뿐만 아니라 ESBMC 와 같은 다른 검증기에서도 동일한 가속화 효과를 보이며, 방법론의 일반성을 입증했습니다.

이 논문은 LLM 이 프로그램 검증의 병목 현상인 불변식 발견 문제를 해결하는 데 있어, 복잡한 기법보다는 직관적이고 검증 중심의 접근법이 더 효과적일 수 있음을 보여주는 중요한 연구입니다.