[논문] ConVer: 계약과 루프 불변식 합성을 활용한 확장 가능한 형식 소프트웨어 검증

Source: arXiv - 2605.27051v1

개요

이 논문은 C 프로그램에 대한 제한 모델 검사(BMC)에서 고전적인 “상태 공간 폭발” 문제를 해결하는 새로운 검증 프레임워크 ConVer를 소개한다. 대규모 언어 모델(LLM)을 이용해 함수 계약을 자동으로 생성하고 반복적으로 정제함으로써, ConVer는 기존 BMC 도구보다 훨씬 크고 복잡한 코드베이스를 검증할 수 있다.

주요 기여

• 탑‑다운 합성 검증: 전체 프로그램 증명을 함수‑단위 검증 계층으로 분해하여 각 BMC 실행이 탐색해야 하는 코드 양을 감소시킨다.
• LLM‑구동 계약 합성: 대규모 언어 모델을 사용해 고수준 사양으로부터 전제조건, 후조건, 루프 불변식을 만든다.
• CEGAR‑CEGIS 루프와 SMART ICE 학습: 검증 시도가 실패하면, 시스템이 자동으로 ICE(Implication‑Counterexample) 학습자를 활용한 반례‑유도 귀납 합성(CEGIS)으로 계약을 정제한다.
• ESBMC‑LF 전처리기: LF(Logical Framework) 모델을 C 코드로 변환하면서 그 속성을 보존한다. 이를 통해 C‑중심 검증기에 새로운 종류의 벤치마크를 제공한다.
• 광범위한 실증 평가: 네 개의 벤치마크 스위트(Frama‑C, X.509 파서, LF2C‑Simple, VerifyThis)를 대상으로 한 실험에서 ConVer는 최첨단 도구와 동등하거나 이를 능가했으며, 대부분 한 번의 정제로 수렴했다.

방법론

1. 입력 및 속성 추출 – 사용자는 C 프로그램과 최상위 어설션(예: “파서는 절대 크래시하지 않는다”)을 제공한다.
2. 계약 생성 – LLM(예: GPT‑4, Claude, LLaMA)에 소스 코드와 속성을 프롬프트로 전달한다. 모델은 각 함수에 대한 후보 계약을 반환한다:
   • 전제조건 (호출 전에 반드시 만족해야 하는 조건)
   • 후조건 (호출 후에 반드시 만족해야 하는 조건)
   • 루프 불변식 (각 반복마다 유지되는 속성)
3. 시스템‑레벨 검사 – 최상위 어설션을 BMC 엔진(ESBMC)으로 인코딩하고, 생성된 계약을 가정함으로써 탐색해야 할 상태 공간을 크게 축소한다.
4. 함수‑레벨 검사 – 각 함수는 자신의 계약을 이용해 독립적으로 검증된다. 함수가 실패하면 구체적인 반례가 생성된다.
5. CEGAR‑CEGIS 루프 – 반례를 SMART ICE 학습기에 다시 입력하면, 더 강력한 계약을 합성해 허위 실패를 제거한다. 프로그램이 안전함이 증명되거나 실제 버그가 발견될 때까지 이 과정을 반복한다.
6. 반복 정제 – 시스템‑레벨 검사와 함수‑레벨 검사를 교차하며 진행한다. 대부분의 계약은 첫 번째 정제 이후에 충분히 정확해지므로 빠르게 수렴한다.

이 워크플로우는 완전 자동화되어 있다. 개발자는 코드와 검증하고자 하는 속성만 ConVer에 지정하면 된다.

결과 및 발견

주요 관찰점:

• 계약 품질이 핵심 – 추론 능력이 뛰어난 LLM(GPT‑4 등)은 검증 성공률을 크게 높였다.
• 원샷 정제 – 대부분의 경우 첫 번째 계약만으로 충분했으며, CEGAR‑CEGIS 루프가 두 번 이상 수행되는 경우는 드물었다.
• 확장성 – 전체 프로그램에 걸친 중첩 루프 전체 전개를 피함으로써, 전통적인 BMC 도구가 시간 초과나 메모리 부족으로 포기하던 프로그램들을 ConVer가 검증했다.

실용적 함의

• CI‑스타일 검증 가속 – 팀은 ConVer를 CI 파이프라인에 통합해 파서, 암호 라이브러리, 임베디드 펌웨어 등 핵심 C 구성 요소의 안전성을 자동으로 증명할 수 있다.
• 수동 어노테이션 부담 감소 – 계약을 직접 작성하는 대신 LLM이 자동으로 생성하므로 보일러플레이트 작업과 전문 지식 요구가 크게 줄어든다.
• 레거시 코드 적용 – ESBMC‑LF 프론트엔드를 통해 기존 LF 사양 등 형식 모델을 그대로 검증할 수 있어, 별도 재작성 없이도 검증이 가능하다.
• 목표 지향 버그 탐색 – ConVer가 실제 반례를 보고하면, 실패한 함수와 계약을 정확히 지목해 개발자가 빠르게 디버깅할 수 있다.
• 언어‑중립 확장 가능성 – 탑‑다운 합성 아이디어와 LLM‑구동 계약 합성은 적절한 프론트엔트만 있으면 Rust, Go, 혹은 고수준 언어에도 적용할 수 있다.

제한 사항 및 향후 연구

• LLM 의존성 – 계약 품질은 사용된 모델에 크게 좌우된다. 부적절한 프롬프트나 작은 모델은 중요한 불변식을 놓쳐 성공률을 낮춘다.
• 확장성 한계 – 중간 규모 프로그램에는 잘 동작하지만, 깊은 재귀나 복잡한 포인터 별칭이 많은 초대형 코드베이스는 여전히 BMC 엔진의 한계에 부딪힌다.
• 동시성 지원 부족 – 현재 구현은 순차 C에 초점을 맞추고 있어, 멀티스레드 프로그램에 적용하려면 인터리빙에 대한 추가 논리가 필요하다.
• 벤치마크 다양성 – 평가가 학술용 벤치마크에 집중돼 있어, 실제 산업 현장(예: 커널 모듈) 코드에 대한 검증은 아직 미진하다.
• 향후 방향 – 저자들은 LLM과 심볼릭 실행의 tighter integration, 가장 유망한 계약 정제 전략의 자동 선택, 그리고 분산 검증 파이프라인으로의 확장을 제안한다.

저자

• Muhammad A. A. Pirzada
• Weiqi Wang
• Yiannis Charalambous
• Konstantin Korovin
• Lucas C. Cordeiro

논문 정보

• arXiv ID: 2605.27051v1
• 분류: cs.SE, cs.AI
• 발표일: 2026년 5월 26일
• PDF: PDF 다운로드