기술 요약: 검증을 위한 다양화 (Diversifying to Verify)

문제 정의

대규모 언어 모델(LLM)이 자연어를 실행 가능한 코드로 합성하는 데는 효과적이지만, **형식적으로 검증된 소프트웨어(formally verified software)**를 생성하는 것은 여전히 큰 과제로 남아 있습니다. Why3와 같은 연역적 검증 프레임워크에서 정당성은 단순히 테스트 케이스를 통과하는 것으로 확립되지 않습니다. 이는 자동 정리 증명기(automated theorem prover)를 만족시키기 위해 형식적인 의미론적 명세(계약, 전제 조건, 사후 조건)와 충분한 증명 가이드(불변량, 변이, 보조 정리)를 요구합니다.

본 연구가 다루는 핵심 문제는 프로그램의 구현 구조—구체적으로 데이터 표현(예: 배열 vs 리스트) 및 제어 흐름(예: 재귀 vs 명령형)—이 **자동 검증 가능성(automated verifiability)**에 극적인 영향을 미칠 수 있다는 점입니다. 하나의 태스크 수준 의미론은 여러 구현체에 의해 충족될 수 있지만, 어떤 구조는 현재의 SMT 솔버가 처리하기 힘든 검증 조건을 생성하는 반면, 다른 구조는 쉽게 증명될 수 있습니다. 기존 방식들은 코드 생성을 단판 승부(single-shot) 작업으로 취급하여, "검증 친화적인" 산출물을 찾기 위한 **구현 다양성(implementation diversity)**의 잠재력을 활용하지 못하는 경우가 많습니다.

방법론: Diversify2Verify

저자들은 Why3 산출물을 생성하고 검증하기 위해 설계된 단계별 LLM 기반 파이프라인인 Diversify2Verify를 소개합니다. 이 파이프라인은 생성 과정을 세 가지 단계로 분해하며, 명세를 약화하거나 근본적인 태스크 의미론을 변경함으로써 검증 성공을 달성하는 것을 방지하기 위해 엄격한 경계를 강제합니다.

1. 파이프라인 아키텍처

• 단계 1: 계약 생성 (Contract Generation).
  • 입력: 자연어 태스크, 대상 시그니처, 구체적인 예시, 그리고 대상 표현 방식(배열 또는 리스트).
  • 과정: LLM은 표현 방식에 특화된 형식적 계약(전제 조건, 사후 조건, 헬퍼 술어)을 추론합니다.
  • 검증: 계약은 Why3에서 타입 체크되며, 구체적인 예시로부터 도출된 "테스트 보조 정리(test lemmas)"를 증명하려고 시도합니다.
  • 정책: 계약이 검증을 통과하면, 이는 **동결(frozen)**됩니다. 이는 후속 단계를 위한 불변의 의미론적 목표 역할을 합니다. 수정은 구문, 타입 또는 예시와의 의미론적 불일치를 해결하기 위해 동결 전 단계에서만 허용됩니다.
• 단계 2: 구현 생성 (Implementation Generation).
  • 과정: 파이프라인은 동일한 동결된 계약에 대해 실행 가능한 WhyML 후보들을 생성합니다.
  • 다양성 전략: 각 태스크에 대해 네 가지 서로 다른 구현 패밀리가 생성됩니다:
    1. 배열-재귀 (Array-Recursive)
    2. 배열-명령형 (Array-Imperative)
    3. 리스트-재귀 (List-Recursive)
    4. 리스트-명령형 (List-Imperative)
  • 검증: 후보들은 타입 체크를 통과하고 실행 가능한 테스트의 일부를 통과하는지에 따라 필터링됩니다.
  • 정책: 수정은 5회 시도로 제한되며, 동일한 표현 및 제어 구조 패밀리 내로 제한됩니다 (예: 배열-명령형 후보가 리스트-재귀로 수정될 수 없음).
• 단계 3: 전체 검증 및 수정 (Full Verification & Repair).
  • 과정: 동결된 계약과 테스트된 구현체가 결합됩니다. LLM은 로컬 프로그램 상태를 글로벌 계약으로 연결하기 위해 필요한 증명 어노테이션(루프 불변량, 변이, 고스트 코드, 단언문)을 추가합니다.
  • 검증: Why3(Z3, Alt-Ergo, CVC4와 같은 SMT 솔버 포함)가 모든 검증 조건을 해소하려고 시도합니다.
  • 수정 정책: 검증 실패 시, 제한된 수정(2회 시도)이 수행됩니다. 수정은 엄격하게 증명 지향적(불변량 강화, 보조 정리 추가)이어야 하며, 동결된 계약과 구현 패밀리를 반드시 유지해야 합니다.

2. 벤치마크 구축

저자들은 LeetCodeDataset에서 유도된 검증 지향적 벤치마크를 구축했습니다:

• 범위: 정수, 배열, 리스트를 포함하는 73개의 태스크.
• 선택 기준: 형식적 계약을 수용할 수 있고, 여러 가지 그럴듯한 구현을 지원하며, SMT 기반 추론에 적합한 태스크들로 필터링되었습니다.
• 규모: 이 벤치마크는 292개의 구현 변체(태스크당 4개)를 생성합니다.
• 참고: 이 벤치마크는 표현과 제어 구조가 검증 가능성에 미치는 영향을 격리하기 위해 의도적으로 SMT 친화적인 데이터 타입에 편향되어 있습니다.

주요 기여

1. Diversify2Verify 파이프라인: 계약 추론, 구현 생성, 증명 어노테이션을 분리하고, 수정 과정 중 명세 드리프트(specification drift)를 방지하기 위해 "동결된 계약" 규율을 강제하는 단계별 LLM 파이프라인.
2. 다양한 구현 생성: 재귀 및 명령형 변체를 배열과 리스트 표현 모두에 대해 체계적으로 생성하여, 구조적으로 다른 프로그램들을 동일한 의미론적 목표와 직접 비교할 수 있게 함.
3. 검증 지향적 벤치마크: 수락된 계약, WhyML 구현 및 검증 로그를 포함하여 73개 태스크와 292개 생성된 산출물로 구성된 큐레이션된 벤치마크를 공개함.
4. 검증 가능성에 대한 실증적 연구: 구현 스타일과 표현에 따라 자동 검증 성공률이 어떻게 변하는지 정량화하고, 여러 변체를 생성함으로써 얻는 이득을 측정함.

결과

평가는 구현 다양성이 자동 검증 성공률을 유의미하게 향상시킨다는 것을 보여줍니다:

• 산출물 수준 검증 (Artifact-Level Verification):
  • 초기: 292개 산출물 중 96개(32.9%)가 수정 없이 검증됨.
  • 수정 후: 292개 산출물 중 154개(52.7%)가 두 번의 수정 패스 후에 검증됨.
  • 수정의 영향: 수정은 58개의 추가 산출물을 검증하는 데 기여했으며, 첫 번째 패스에서 가장 큰 이득이 발생했습니다.
• 태스크 수준 검증 (Task-Level Verification):
  • 최소 하나의 변체가 검증된 태스크는 73개 중 49개로, 태스크 수준에서 67.1%의 성공률을 달성했습니다.
  • 가장 강력한 개별 패밀리는 (Array-Recursive) 44개의 태스크를 검증했습니다.
  • 이는 다양성이 태스크 커버리지를 높이는 측정 가능한 증가를 제공함을 나타냅니다. 즉, 단일 구현 스타일에 의존하면 해결 가능한 많은 태스크를 놓치게 됩니다.
• 구조적 차이:
  • 재귀 vs 명령형: 재귀 변체(배열의 경우 60.3%, 리스트의 경우 54.8%)가 명령형 변체(둘 다 47.9%)보다 더 자주 검증되었습니다. 이는 재귀적 구현이 재귀적 명세와 더 잘 일치하는 반면, 명령형 구현은 가변 상태를 요약하기 위해 복잡한 루프 불변량을 필요로 하기 때문인 것으로 분석됩니다.
  • 배열 vs 리스트: 배열과 리스트의 총 검증율은 비슷했으며, 이는 이 문맥에서 제어 구조(재귀 vs 명령형)의 선택이 데이터 표현의 선택보다 더 뚜렷한 영향을 미친다는 것을 시사합니다.
• 실패 분석:
  • 검증되지 않은 대부분의 산출물(남은 138개)은 남은 증명 의무(remaining proof obligations)가 매우 적었습니다(평균 2.5개의 루트 목표). 이는 실패 원인이 근본적으로 잘못된 구현보다는 누락된 증명 스캐폴딩(예: 특정 불변량)에 있었음을 시사합니다.
  • 수동 감사를 통해 파이프라인이 292개 중 291개 사례에서 동결된 계약을 성공적으로 보존했음을 확인했습니다(LLM이 원래 계약에 없는 전제 조건을 추가한 경우는 단 한 건뿐이었습니다).

의의 및 주장

본 논문은 태스크와 동등한 구현들이 검증 가능성 면에서 크게 다를 수 있다고 주장합니다. 핵심 가설은 뒷받s습니다: 다양한 변체를 생성하는 것이 자동 연역 검증에 적합한 구조를 가진 구현을 찾을 확률을 높입니다.

저자들은 이 접근 방식이 단 하나의 "완벽한" 생성을 찾는 것이 아니라, 다양성을 검증 조건을 탐색하기 위한 실질적인 도구로 활용하는 것임을 강조합니다. 명세 생성과 구현 생성을 분리하고 수정 중에 엄격한 경계를 강제함으로써, 시스템은 명세를 약화하거나 태스크 의미론을 변경하여 검증 성공을 달성하는 것을 방지합니다.

이 연구는 LLM 지원 검증 프로그래밍에서 구현 다양성이 강력한 메커니즘이며, 특히 제한된 검증 가이드 수정과 결합될 때 태스크 커버리지를 개선할 수 있음을 시사합니다. 저자들은 이러한 발견이 Why3를 사용하는 정수 및 시퀀스 태스크의 맥락에 특화되어 있음을 언급하며, 향후 연구에서 더 풍부한 데이터 구조와 다른 검증 프레임워크를 탐구할 것을 제안합니다.