Evaluating LLM-Generated ACSL Annotations for Formal Verification

논문 개요

이 논문은 C 언어 프로그램에 대한 ACSL(ANSI/ISO C Specification Language) 명세를 자동으로 생성하고, 이를 형식 검증 (Formal Verification) 도구로 검증할 수 있는 정도를 실증적으로 평가한 연구입니다. 특히, 인간의 개입이나 학습 기반 보조 없이 대규모 언어 모델 (LLM) 과 기존 규칙 기반 도구가 생성한 명세의 품질, 검증 안정성, 그리고 SMT 솔버의 민감도를 비교 분석했습니다.

1. 연구 배경 및 문제 제기 (Problem)

• 형식 명세의 중요성: 신뢰할 수 있는 소프트웨어 구축을 위해 형식 명세는 필수적이지만, 실제 C 프로그램에 대해 정확하고 검증 가능한 명세를 작성하는 것은 매우 어렵습니다.
• LLM 의 한계: 최근 LLM 은 언어 이해와 생성 능력이 뛰어나지만,其行为가 불투명하고 안전성 보장이 부족합니다. 특히 형식 검증과 같은 고신뢰도 (High-assurance) 영역에서 LLM 이 생성한 명세가 실제로 검증 도구 (Proof) 를 통과할 수 있는지에 대한 체계적인 실증 데이터가 부족했습니다.
• 기존 연구의 차이: 이전 연구들은 주로 설문 조사나 소규모 데이터셋에 의존했으나, 본 논문은 2025 년 11 월에 공개된 최신 데이터셋 (CASP) 을 활용하여 자동화된 환경에서 LLM 과 전통적 도구를 직접 비교했습니다.

2. 연구 방법론 (Methodology)

• 데이터셋: Hertzberg et al. (2025) 이 공개한 506 개의 C 프로그램으로 구성된 'CASP' 데이터셋을 사용했습니다. (단, 355 개의 순수 C 파일만 실험에 사용됨).
• 생성 시스템 비교 (5 가지):
  1. 규칙 기반 Python 스크립트: 수동 규칙을 적용한 자동 생성.
  2. Frama-C RTE 플러그인: 런타임 오류 검출을 기반으로 한 도구 생성.
  3. DeepSeek-V3.2: 대형 언어 모델.
  4. GPT-5.2: 대형 언어 모델.
  5. OLMo 3.1 32B Instruct: 대형 언어 모델.
• 검증 환경:
  • 플랫폼: Frama-C WP (Weakest Precondition) 플러그인 사용.
  • SMT 솔버: Alt-Ergo, CVC4, CVC5, Z3 등 4 가지 솔버를 동일한 조건에서 실행.
  • 평가 지표: 증명 성공률 (Proof Success), 타임아웃 횟수 (Timeout), Qed 시간 (증명 완료 시간) 및 그 분산 (표준편차).

3. 주요 기여 (Key Contributions)

1. 최신 데이터셋 기반 통제 실험: 기존 설문 조사 중심의 연구와 달리, 506 개의 실제 C 프로그램을 대상으로 5 가지 생성 전략을 통제된 환경에서 비교했습니다.
2. 솔버 민감도 및 증명 안정성 분석: 단순히 명세가 '맞는지'뿐만 아니라, 생성된 명세가 다양한 SMT 솔버에서 얼마나 안정적으로 (Stable) 그리고 효율적으로 (Efficient) 증명되는지 분석했습니다.
3. 표현력 (Expressiveness) 과 검증 안정성 (Stability) 의 트레이드오프 규명: LLM 이 생성한 명세가 더 풍부할수록 검증 도구의 성능이 불안정해지는 경향을 실증적으로 증명했습니다.

4. 실험 결과 (Results)

가. 증명 성공률 및 솔버 성능

• 도구 기반 (Python Script, RTE): 가장 높은 증명 성공률 (평균 99% 이상) 과 낮은 타임아웃을 보였습니다. 특히 RTE 는 런타임 오류 기반의 보수적인 명세로 인해 매우 안정적이었습니다.
• LLM 기반:
  • DeepSeek: LLM 중에서는 가장 우수한 성능을 보였으며, 도구 기반 생성과 유사한 높은 성공률을 기록했습니다.
  • GPT-5: 성공률은 낮고 (약 80% 대), 타임아웃이 가장 많았습니다. 특히 Alt-Ergo 솔버에서 성능이 크게 저하되었습니다.
  • OLMo3: GPT-5 보다 안정적이었으나, 도구 기반보다는 성능이 떨어졌습니다.

나. 솔버별 특성

• CVC4/CVC5: 대부분의 설정에서 가장 일관된 성능을 보였습니다.
• Z3: 복잡한 LLM 생성 명세에서 중앙값 변동성은 낮았으나, 특정 인스턴스에서 큰 변동성을 보였습니다.
• Alt-Ergo: 여러 설정에서 가장 높은 타임아웃 빈도를 보였으며, 특히 GPT-5 생성 명세에서 취약했습니다.

다. Qed 시간 (Proof Discharge Time) 및 변동성

• 안정성: 규칙 기반 및 RTE 생성 명세는 Qed 시간이 매우 짧고 분산 (표준편차) 이 작아 예측 가능했습니다.
• 불안정성: GPT-5 와 DeepSeek 이 생성한 명세는 Qed 시간이 길고 분산이 매우 컸습니다. 이는 LLM 이 생성한 명세의 구조적 불일치나 복잡성이 솔버의 탐색 공간을 증가시켜 증명 시간을 불규칙하게 만들기 때문입니다.
• 트렌드: 규칙 기반 < OLMo3 < DeepSeek/GPT-5 순으로 명세의 복잡성과 검증 변동성이 증가했습니다.

5. 의의 및 결론 (Significance & Conclusion)

• 실용적 시사점: LLM 은 형식 명세 생성에 유망하지만, 현재 상태에서는 검증 안정성 (Verification Stability) 이 부족합니다. 대규모 자동 검증을 위해서는 명세의 풍부함 (Expressiveness) 보다 솔버가 처리하기 쉬운 구조화된 명세가 더 중요합니다.
• 솔버 선택의 중요성: 생성된 명세의 품질뿐만 아니라, 선택한 SMT 솔버의 특성이 검증 성공 여부에 결정적인 영향을 미칩니다.
• 미래 방향: LLM 기반 생성과 규칙 기반/도구 기반 생성을 결합한 하이브리드 워크플로우가 필요하며, 솔버의 민감도를 줄이고 일관된 성능을 보장하는 방향으로 연구가 진행되어야 함을 강조합니다.

요약하자면, 이 논문은 LLM 이 생성한 ACSL 명세가 형식 검증을 통과할 수 있음을 보여주지만, 도구 기반 생성에 비해 검증 시간의 변동성이 크고 솔버에 따라 성능 편차가 심하다는 중요한 실증적 증거를 제시했습니다. 이는 안전이 중요한 소프트웨어 개발에 LLM 을 적용할 때 신중한 검증 프로세스가 필요함을 시사합니다.