Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis

Motivation

• Known: 전통적으로 loop invariant 발견은 constraint solving, abstract interpretation, dynamic analysis 등으로 연구되어 왔으며, 최근 LaM4Inv, LOOPY, LEMUR, Clause2Inv 등 LLM 기반 verifier들은 LLM 출력을 노이즈가 많은 symbolic 자료로 취급해 predicate filtering, Houdini pruning, backtracking 등 복잡한 알고리즘으로 재구성한다.
• Gap: 기존 최초 평가 연구(Pei et al., 2023)는 Daikon이라는 dynamic analysis 도구와의 비교만으로 정확성을 판단해 불건전(unsound)하며 invariant의 강도(strength), 즉 실제 검증 가속 효용을 평가하지 못했고, 후속 LLM 기반 verifier들은 복잡한 harness-heavy 알고리즘에 의존해 LLM이 점점 강력해지는 상황에서 그러한 복잡성이 정말 필요한지에 대한 의문이 남는다.
• Why: LLM이 생성한 invariant의 실제 유용성(검증 가속 여부)을 sound하게 평가할 수 있는 프레임워크가 있으면, 프로그램 검증이라는 40년 이상 지속된 난제에 LLM을 실질적이고 신뢰성 있게 적용할 수 있는 길을 열 수 있다.
• Approach: Quokka는 LLM이 제안한 invariant를 verifier(UAutomizer 기반)에 직접 질의해 유효성과 목표 assertion 증명에의 기여(속도 향상)를 판단하는 단순하고 evaluation-centric한 파이프라인을 채택하며, SV-COMP 기반 866개 벤치마크와 3589개 학습 인스턴스를 구축해 supervised fine-tuning과 Best-of-N sampling의 효과를 검증한다.

Achievement

Figure 3. Number of instances solved by different methods over

1. Sound한 evaluation 프레임워크 제안: Daikon 기반의 불건전한 비교 대신 verifier 질의를 통해 invariant의 정확성과 검증 가속 효용을 동시에 sound하게 측정하는 Quokka를 제시했다.
2. 대규모 벤치마크 구축: SV-COMP 최신판 기반 866개 인스턴스로 구성된, LLM 기반 verifier 평가로는 현재까지 최대 규모의 데이터셋을 구축했다.
3. 9개 LLM 대상 종합 평가: 여러 모델 패밀리에 걸친 9개 SOTA LLM을 평가해 모델 역량을 효과적으로 구분할 수 있는 도전적인 설정을 제공했다.
4. 성능 향상 기법 검증: 3589개 인스턴스의 검증기 기반 필터링 학습 데이터를 구축하여 supervised fine-tuning과 Best-of-N sampling이 검증 가속 성능을 측정 가능하게 향상시킴을 보였다.
5. 기존 LLM 기반 verifier 대비 SOTA 달성: LaM4Inv, LOOPY, LEMUR, Clause2Inv 등 복잡한 후처리 알고리즘을 사용하는 기존 방법들보다 단순한 설계로 일관되게 더 나은 성능을 보였다.

How

Figure 2. Effect of Best-of-N sampling on the number of ∆in-

• Hoare logic 기반으로 loop invariant synthesis 문제를 형식화하고, LLM이 프로그램 위치(location)와 predicate를 제안하도록 유도
• 제안된 invariant를 verifier(UAutomizer)에 질의하여 (1) invariant 자체의 유효성(soundness)과 (2) 해당 invariant를 활용했을 때 target assertion 증명이 가능해지는지(strength/가속 효과)를 두 단계 verifier query로 직접 판별
• 복잡한 filtering/reassembly/Houdini/backtracking 알고리즘을 제거하고 병렬 verifier 질의만으로 평가를 수행하는 단순화된 파이프라인 설계
• SV-COMP 최신 edition으로부터 866개 평가 인스턴스와 3589개 학습 인스턴스를 구성하되, 학습 데이터는 verifier 기반 필터링으로 품질 보장
• 9개 SOTA LLM(여러 model family)에 대해 zero-shot 평가를 수행하고, 이후 supervised fine-tuning과 Best-of-N sampling을 적용해 성능 변화를 측정하고 기존 LLM 기반 verifier들과 비교

Originality

• 기존 LLM 기반 invariant synthesis 연구들이 LLM 출력을 "노이즈가 있는 symbolic 재료"로 보고 복잡한 알고리즘(query-filter-reassemble, Houdini, backtracking)으로 재구성하려 한 것과 달리, LLM 출력을 verifier에 직접 질의해 평가하는 근본적으로 단순한 패러다임 전환을 제시
• 정확성(correctness)뿐 아니라 강도(strength, 즉 실제 검증 가속 기여도)까지 sound하게 측정하는 이중 기준 평가체계를 최초로 도입
• Daikon 기반의 불건전한 기존 평가 방식의 한계(동치 invariant의 오분류 등)를 명확히 지적하고 verifier 기반 대안을 제시
• LLM 기반 invariant synthesis에 SOTA LLM 9종에 대한 대규모 벤치마크와 fine-tuning/Best-of-N 연구를 결합한 최초의 종합적 실증 연구

Limitation & Further Study

• 벤치마크가 SV-COMP 기반으로 구성되어 있어 실제 산업 규모 소프트웨어나 더 복잡한 자료구조(배열, 포인터, 동시성 등)를 포함한 프로그램에 대한 일반화 가능성이 명확히 검증되지 않음
• 사용된 verifier(UAutomizer)에 대한 의존성이 있어, 다른 verifier와의 호환성 및 verifier 자체의 한계(타임아웃, 불완전성)가 평가 결과에 미치는 영향에 대한 심층 분석이 부족할 수 있음
• Best-of-N sampling과 fine-tuning의 개선폭이 어느 정도인지, 그리고 계산 비용 대비 효율성에 대한 정량적 트레이드오프 분석이 발췌 내용에서는 충분히 드러나지 않음
• 후속 연구로는 더 복잡한 프로그램 구조(배열 invariant, 재귀, 동시성 프로그램)로의 확장, 다양한 verifier와의 통합, invariant 생성을 위한 강화학습 기반 fine-tuning 등이 필요할 것으로 보임

Evaluation

총평: 복잡한 symbolic 후처리 없이 verifier 직접 질의만으로 LLM 생성 invariant를 sound하게 평가하는 단순하지만 효과적인 프레임워크로, 대규모 벤치마크 구축과 함께 LLM 기반 프로그램 검증 연구에 실질적인 기여를 한다.