기술 요약: VeriFast를 위한 LLM 생성 명세에 관한 경험적 연구

문제 정의

VeriFast와 같은 분리 논리(Separation Logic, SL) 기반의 정적 검증 도구는 산업 규모의 소프트웨어에 대해 기능적 정확성과 메모리 안전성을 검증할 수 있는 능력을 갖추고 있다. 그러나 명세를 작성하는 데 막대한 인간의 노동력이 필요하다는 점이 도입의 걸림돌이 되고 있다. 비-SL 검증기와 달리, SL 검증기는 힙 구조와 소유권(ownership)을 추론하기 위해 루프 불변량(loop invariants), 귀납적 보조 정리(inductive lemmas), 그리고 술어의 명시적인 '폴드(fold)' 및 '언폴드(unfold)'(열기 및 닫기)를 포함한 복잡한 보조 명세를 요구한다. 최근 연구들이 비-SL 검증기(예: Dafny, Frama-C)를 위한 명세 생성에 대규모 언어 모델(LLM)을 성공적으로 적용해 왔으나, 힙의 불연속성(disjointness)과 소유권에 관한 독특한 추론 패턴을 요구하는 SL 기반 검증기용 명세 생성 능력에 대한 경험적 평가 연구는 부족한 실정이다.

방법론

저자들은 VeriFast의 명세를 생성하는 데 있어 LLM의 성능을 평가하기 위해 2단계로 구성된 경험적 연구를 수행하였다.

데이터셋 구축:
본 연구는 60개의 C 프로그램에서 추출한 303개의 함수 데이터셋을 활용하였다. 각 함수에 대해 네 가지 버전을 생성하였다:

1. Ground Truth (실제 정답): VeriFast로 완전히 명세되고 검증된 버전.
2. Natural Language (NL, 자연어): 동작에 대한 비공식적인 자연어 설명이 포함된 소스 코드.
3. Functional Behavior (FB, 기능적 동작): VeriFast의 명세 언어로 작성된 공식적인 전제 조건(preconditions) 및 사후 조건(postconditions)이 포함된 소스 코드.
4. Functional Behavior Plus (FBP, 기능적 동작 플러스): 검증에 필요한 추가적인 구성 요소(예: 메모리 할당 상태, 정수 범위)가 포함된 공식 전제/사후 조건이 포함된 소스 코드.

실험 설계:
연구는 두 단계로 진행되었다:

1. 파일럿 연구 (Pilot Studies): 최적의 구성을 선택하기 위해 10개의 저자 개발 프로그램에서 추출한 45개의 함수 하위 집합을 대상으로 수행되었다.
   • 프롬프팅 접근 방식: Basic, Chain-of-Thought (CoT), RAG-sparse, RAG-dense를 포함한 8가지 접근 방식을 테스트하였으며, 입력 입도(전체 프로그램 vs 단일 함수)에 따른 변형을 두었다.
   • LLM 선택: 10개의 LLM을 평가하였다. 검증 성공률, 오류 심각도, 기능적 동작 보존 여부를 바탕으로 세 가지 모델을 최종 연구를 위해 선정하였다: Claude 3.7 Sonnet, Gemini 2.5 Pro, GPT-4o.
   • 선택 결과: 가장 효과적인 프롬프팅 전략으로 입력 분할(input splitting)(함수를 하나씩 처리)을 적용한 RAG-sparse 방식이 선정되었다.
2. 본 연구 (Full Study): 선정된 프롬프트와 세 가지 LLM을 세 가지 입력 유형(NL, FB, FBP)에 대해 전체 데이터셋인 303개 함수에 적용하여 총 2,727개의 출력 함수를 생성하였다.

분석 지표:

• RQ1 (기능적 동작): LLM이 소스 코드를 변경했는지, 혹은 입력값과 비교하여 전제/사후 조건을 약화하거나 강화했는지에 대한 질적 분석.
• RQ2 (검증 가능성): 생성된 명세 중 VeriFast를 통해 성공적으로 검증된 비율에 대한 정량적 측정.
• RQ3 (오류): 언어적 특징의 분포를 대표하도록 샘med된 354개의 실패 함수에 대한 심층 분석. 오류를 수동으로 수정하여 심각도(Compile, Practical, Theoretical)와 위치(예: 술어, 루프 불변량, open/close 문)별로 분류하였다.

주요 기여

1. SL 검증기에 대한 첫 번째 경험적 연구: 8가지 프롬프팅 접근 방식, 10개의 LLM, 3가지 입력 유형을 포괄하여 SL 검증기(VeriFast)를 위한 명세를 생성하는 LLM을 평가한 최초의 철저한 연구이다.
2. 포괄적인 데이터셋: 향후 연구를 촉진하기 위해 네 가지 명세 변형(실제 정답 포함)을 특징으로 하는 60개의 C 프로그램(303개 함수)으로 구성된 공개 가능한 데이터셋을 제공한다.
3. 세밀한 오류 분석: 컴파일 오류, 실무적 추론 실패(예: 누락된 open/close 문), 이론적 논리 불일치를 구분하는 상세한 오류 분류 체계(taxonomy)와 인간이 작성한 수정안을 제시한다.
4. 실행 가능한 통찰력: 공식적인 입력 명세의 이점과 VeriFast의 자동화 기능의 유용성을 포함하여, LLM 기반 검증 환경을 최적화하기 위한 구체적인 가이드를 제공한다.

결과

기능적 동작 보존 (RQ1):

• LLM은 의도된 기능적 동작을 대체로 잘 보존하였다.
• 소스 코드: 출력의 91.0%가 변경되지 않았으며, 9.0%에서 변경이 발견되었다(주로 미미한 의미론적 편집 또는 헤더 할루시네이션).
• 명세: 전제 및 사후 조건의 92%가 기능적 동작을 보존하였다(동등하거나 강화됨).
• 입력의 영향: 공식적인 입력(FB/FBP)이 자연어(NL) 입력보다 더 높은 보존율을 보였다. Gemini 2.5 Pro가 모호성에 대해 가장 높은 강건성을 보였다.

검증 가능성 (RQ2):

• 전체 검증 성공률은 31.4%(약 3개 함수 중 1개)였다.
• 입력 유형: 성공률은 입력의 완전성과 상관관계가 있었다: FBP (39.9%) > FB (29.5%) > NL (24.6%).
• 모델 성능: Gemini 2.5 Pro가 평균 39.7%의 성공률을 기록하며 Claude 3.7(29.8%) 및 GPT-4o(24.5%)를 앞질렀다.
• 복잡도: 복잡한 기능에서는 성공률이 크게 하락하였다: 일반 SL (51.2%) > 재귀적 술어 (30.9%) > 병행성 (12.3%) 및 루프 (11.4%).

오류 분석 (RQ3):

• 오류 분포: 분석된 1,652개의 오류 중 71%는 Practical(자동 추론에 불충분한 경우, 예: open/close 문 누락)이었고, 23%는 Compile 오류였으며, 단 6%만이 Theoretical(논리적 불일치) 오류였다.
• 근본 원인: 오류의 94%는 일반적인 논리적 추론 실패가 아니라, SL 검증기의 메커니즘(구문, 힙 추론, 소유권 추적)에 대한 도메인 특화 지식의 부족에서 기인하였다.
• 구체적 실패 사례: malloc_block 주석 누락, 전제/사후 조건의 잘못된 배치, 힙 세그먼트의 전이성을 위한 필요한 루프 불변량이나 보조 정리를 제공하지 못하는 문제 등이 공통적으로 나타났다.
• 모델 간 차이: Gemini 2.5는 모든 범주, 특히 이론적 및 실무적 추론에서 가장 적은 오류를 생성하였다.

의의 및 주장

본 논문은 LLM이 소스 코드와 명세의 기능적 동작을 보존할 수는 있지만, 현재로서는 분리 논리 도구를 위한 완전히 검증 가능한 명세를 생성하는 데 있어 **완만한 성공(modest success)**만을 거두고 있다고 주장한다. 주요 병목 구간은 일반적인 추론 능력이 아니라, SL 검증기 고유의 보조 명세 패턴(예: open/close를 통한 힙 소유권 관리 및 보조 정리 활용)에 대한 특정 지식의 부재이다.

저자들의 결론은 다음과 같다:

1. 공식 입력의 중요성: 자연어보다 공식 계약(FB/FBP)을 제공하는 것이 성공률을 크게 높인다.
2. 모델 선택의 결정적 역할: 비용이 더 높더라도 Gemini 2.5 Pro가 병행성 및 루프와 같은 복잡한 기능에 대해 현재 가장 우수한 모델이다.
3. 도구 개선 방향: LLM의 성능을 높이기 위해, SL 검증기는 수리 루프(repair loops) 중에 LLM에 더 나은 디버깅 정보(예: 심볼릭 힙 상태)를 노출해야 하며, 단순한 open/close 생성을 담당하는 심볼릭 도구(VeriFast의 자동화 기능 등)와 복잡한 추론을 담당하는 LLM 간의 하이브리드 접근 방식을 활용해야 한다.

이 연구는 LLM이 현재 SL 검증을 위한 인간 전문가를 대체할 수 있다고 주장하는 것이 아니라, 미래의 AI 지원 검증 환경을 구축하기 위한 기준점(baseline)과 구체적인 가이드를 제공하는 데 목적이 있다.