기술 요약: VerIbmc를 이용한 신경-기호적 소프트웨어 검증

문제 정의

루프 불변량 합성(Loop invariant synthesis)은 형식 소프트웨어 검증에서 핵심적인 병목 구간으로 남아 있습니다. 심볼릭 기법(예: 추상 해석, 제약 조건 해결)과 데이터 기반의 "추측 및 확인(guess-and-check)" 방식이 존재하지만, 이들은 종종 확장성, 표현력 또는 실제 코드의 다양성 측면에서 어려움을 겪습니다. 최근 대규모 언어 모델(LLM)은 코드 코퍼스에서 학습된 패턴을 활용하여 후보 불변량을 생성하는 데 유망한 가능성을 보여주었습니다. 그러나 기존의 신경-기호적 접근 방식은 일반적으로 외부 클라우드 API를 통해 액세스되는 독점적인 폐쇄형 모델에 의존합니다. 이러한 의존성은 산업적 배포에 있어 다음과 같은 중대한 장애물을 초래합니다:

1. 개인정보 보호 및 컴플라이언스: 소스 코드가 제3자 서비스로 전송되어야 하므로 기밀 유지 문제가 발생합니다.
2. 재현성: 외부 제공자에 대한 의존은 통제된 검증 파이프라인로의 통합을 복잡하게 만듭니다.
3. 비용 및 지속 가능성: 대규모 모델은 계산 비용이 많이 들고 에너지 집약적이어서, 지속적인 검증 워크플로우에 적용하기에는 실용성이 떨어집니다.

저자들은 이러한 과제들이 조직의 인프라 내에서 독점 코드를 노출하지 않고 완전히 작동할 수 있는, 로컬에 배포 가능한 오픈 웨이트(open-weight) 언어 모델로의 전환을 필요로 한다고 주장합니다.

방법론: VerIbmc 파이프라인

본 논문은 로컬에 호스팅된 오픈 웨이트 LLM과 심볼릭 추론을 결합하여 C 프로그램의 루프 불변량을 합성하도록 설계된 신경-기호적 파이프라인인 VerIbmc를 제시합니다. 이 시스템은 ESBMC(Efficient SMT-Based Context-Bounded Model Checker)를 검증 오라클로 사용합니다. 파이프라인은 LLM을 호출하기 전에 저렴하고 결정론적인 심볼릭 추론을 우선시하는 "필요할 때만 격상(escalate only when necessary)" 원칙에 따라 설계되었습니다.

핵심 아키텍처

파이프라인은 세 가지 별도의 단계로 작동합니다:

1. 단계 0 (베이스라인 검증): ESBMC가 주석이 없는 프로그램을 검증합니다. 프로그램이 사소하게 안전하거나 명백히 안전하지 않음이 증명되면, 불필요한 합성 노력을 피하기 위해 프로세스가 즉시 종료됩니다.
2. 단계 1 (심볼릭 후보 생성): 단계 0이 "Unknown"을 반환하는 경우, 시스템은 루프 진입 변수와 상수의 쌍별 비교를 통해 원자적(atomic) 후보 불변량을 심볼릭하게 열거합니다. 이 원자들은 ESBMC를 통해 귀납성(inductivity)을 검증받습니다. 시스템은 세 가지 저장소인 증명 가능($P$), 반증 가능($D$), 미정($U$)을 유지합니다. 모든 증명 가능한 원자들의 결합이 사후 조건(post-condition)을 입증하기에 충분하다면, 파이프라인은 LLM 호출 없이 성공적으로 종료됩니다.
3. 단계 2 (LLM 정교화 루프): 심볼릭 단계가 불충분한 경우, 파이프라인은 LLM이 새로운 불변량을 생성하도록 유도하는 반복 루프에 진입합니다.
   • 피드back 메커니즘: LLM은 현재 프로그램, $P$, $D$, $U$ 저장소의 내용이 담긴 구조화된 피드백, 그리고 퓨샷(few-shot) 예시를 전달받습니다.
   • 분해 및 재결합: LLM이 생성한 후보가 검증에 실패하면, 시스템은 이를 하위 공식(원자)으로 분해합니다. 각 원자는 개별적으로 검증되어 적절한 저장소에 추가됩니다. 현재 증명 가능한 모든 원자들의 결합이 다시 검증됩니다. 이를 통해 실패한 LLM 제안으로부터 유용한 구성 요소를 살려낼 수 있습니다.
   • 종료: 유효한 불변량이 발견되거나, 반복 예산이 소진되거나, 타임아웃이 발생할 때까지 루프가 계속됩니다.

추론 전략

저자들은 두 가지 설계 축을 기준으로 네 가지 추론 전략을 평가합니다:

1. 검증기 피드백 (심볼릭 우선순위):
   • Basic: 단계 1의 심볼릭 우선순위와 원자 수준의 필터링을 활용하여 전체 3단계 파이프라인을 실행합니다.
   • LLM-Only: 단계 1과 원자 수준의 분해를 건너뛰고, 오직 LLM이 전체로서 귀납적 불변량을 생성하도록 의존합니다. 이는 절제 연구(ablation)를 위한 베이스라인 역할을 합니다.
2. 추론 구조:
   • Chain-of-Thought (CoT): 단계별 추론 예시(귀납, 호어 논리, 혼(Horn) 절, 또는 직접 유도)를 포함한 표준 프롬프팅을 사용합니다.
   • Tree-of-Thoughts (ToT): "정찰(scouting)" 단계 동안 여러 유도 스타일을 병렬로 탐색하고, 생성된 증명 가능한 원자의 수를 기준으로 점수를 매긴 뒤, 상위 2개의 성능이 좋은 스타일에 남은 반복 예산을 집중합니다.

주요 기여

1. 신경-기호적 파이프라인: 로컬에 서빙되는 오픈 웨이트 LLM을 ESBMC와 통합하여 자동화된 루프 불변량 합성을 수행하는 완전한 시스템으로, 전체 과정을 내부 인프라 내에서 운영합니다.
2. 전략의 체계적 평가: 순수 LLM, 심볼릭 가이드, 그리고 Tree-of-Thoughts (ToT) 변형 간의 비교를 통해 심볼릭 피드백과 추론 구조의 영향을 체계적으로 입증했습니다.
3. 심볼릭 피드백의 이점: 증명 가능한 불변량 원자들을 LLM의 컨텍스트로 제공하는 것이 일관된 이득을 준다는 것을 입증했습니다. 특히 약한 모델(예: Llama-3.1-8B가 순수 LLM 베이스라인 대비 35개의 벤치마크를 더 해결함)에서 효과가 두드러졌습니다.
4. 프롬프트 엔지니어링 분석: 다양한 프롬프팅 스타일(CoT vs. ToT)과 추론 템플릿(귀납, 호어 논리, 혼 절)이 불변량 합성에 미치는 영향을 평가했습니다.
5. 대규모 벤치마킹: 5개의 오픈 웨이트 모델(7B ~ 120B 파라미터), 4개의 추론 전략, 5개의 벤치마크 패밀리(520개 문제, 유효한 것 499개)에 걸쳐 총 10,400개의 문제당 결과를 도출하는 광범위한 평가를 수행했습니다.

실험 결과

평가는 4개의 NVIDIA RTX A6000 GPU가 장착된 서버에서 5개의 오픈 웨이트 모델(GPT-OSS-120B, GPT-OSS-20B, Qwen2.5-32B, Qwen2.5-7B, Llama-3.1-8B)을 사용하여 진행되었습니다.

• 전반적인 성능: 최적의 단일 구성(GPT-OSS-120B와 Basic 전략)은 499개 문제 중 431개(86.4%)를 해결했습니다.
• 최첨단 기술(SOTA)과의 비교:
  • VerIbmc는 동일한 로컬 하드웨어에서 실행될 때 전통적인 심볼릭 도구(CPA-Checker, 2ls, ESBMC-Kind) 및 신경망 전용 도구(Code2Inv)보다 실질적으로 우수한 성능을 보였습니다.
  • 공유 벤치마크 세트에서 VerIbmc는 값비싼 외부 API(예: GPT-4)에 의존하는 강력한 LLM 증강 도구들(Clause2Inv, LaM4Inv, LORIS)과 대등하거나 약간 낮은 수준의 성능을 보였습니다. 주목할 점은 VerIbmc가 코드를 클라우드로 전송하지 않고도 이러한 결과를 달성했다는 것입니다.
  • VerIbmc는 프런트엔드 제한으로 인해 많은 경쟁 도구들이 표현하기 어려운 배열, 중첩 루프, 포인터가 포함된 전체 SV-COMP 벤치마크 세트(154개 문제)까지 독보적으로 확장 가능합니다.
• 심볼릭 단계의 영향: 심볼릭 단계 1은 LLM 호출 없이 75개의 문제를 해결했습니다. 약한 모델의 경우, 심볼릭 증강이 상당한 성능 향상(Llama-3.1-8B의 경우 최대 +35개 추가 문제 해결)을 제공했습니다.
• ToT vs. CoT: ToT 프롬프팅은 다양성과 정확도 사이의 트레이드오프를 보여주었습니다. ToT는 CoT가 접근할 수 없는 고유한 문제-모델 쌍에 도달할 수 있었지만, 종종 실행 시간(wall-clock time) 오버헤드를 발생시켰으며, 약한 모델의 경우 반복 예산 소진으로 인해 결과적으로 해결된 문제가 감소하기도 했습니다. 가장 강력한 모델(GPT-OSS-120B)의 경우, CoT와 ToT 간의 성능 차이는 미미했습니다.
• 모델 역량: 결과는 모델의 역량이 정확도의 주요 동인임을 나타냅니다. 가장 강력한 모델과 가장 약한 모델 사이의 격차는 동일한 모델 내에서 전략 변경으로 발생하는 성능 편차보다 훨씬 컸습니다.

의의 및 주장

본 논문은 VerIbmc가 개인정보를 보호하면서도 에너지 효율적인 방식으로 LLM 기반의 신경-기호적 접근법이 루프 불변량 합성에 효과적으로 적용될 수 있음을 입증한다고 주장합니다. 오픈 웨이트 모델을 사용하여 로컬 인프라에서 완전히 운영함으로써, 이 방식은 API에 묶인 값비싼 독점 프런티어 모델의 필요성을 제거합니다.

저자들은 이 방법이 **구조적으로 건전함(sound by construction)**을 강조합니다. 모든 후보 불변량은 수락되기 전에 공식 검증기(ESBMC)에 의해 검증됩니다. 비록 문제는 결정 불가능성(undecidability) 때문에 불완전할 수 있으나, 본 연구는 AI 지원 형식 검증을 위한 실용적이고 확장 가능하며 재현 가능한 경로를 제공합니다. 이 연구는 데이터 프라이버시와 자원 효율성이 중요한 요구 사항인 산업 현장용 검증 파이프라인을 향한 한 걸음을 내딛는 작업입니다.