기술 요약: VeriScale: 검증 가능한 코드 생성을 위한 적대적 테스트 스위트 확장

문제 제기

대규모 언어 모델 (LLM) 이 소프트웨어 공학 분야에서 점차 널리 배포됨에 따라, 단순히 기능적인 코드뿐만 아니라 형식적으로 검증 가능한 명세와 증명 생성 능력을 평가하는 것이 중요해졌습니다. VERINA 및 CLEVER와 같은 기존 검증 가능 코드 생성 벤치마크는 명세 생성 (SpecGen) 및 코드 생성 (CodeGen) 을 평가하기 위해 테스트 스위트 평가에 크게 의존합니다. 그러나 이러한 벤치마크는 근본적인 한계를 겪고 있습니다. 특히 부정적 테스트 케이스(예상치 못한 입력과 예상치 못한 출력) 의 고품질 테스트 케이스 부족에 의해 제약받고 있습니다.

현재 벤치마크는 일반적으로 제한된 수의 긍정적 입력 - 출력 쌍만 제공합니다. 그 결과, 모델들은 프로그램 의도를 진정으로 포착하거나 생성된 명세의 건전성과 완전성을 보장하지 않은 채 이러한 희소한 테스트를 충족함으로써 부풀려진 통과율을 달성할 수 있습니다. 이는 테스트 스위트가 논리적 결함이나 경계 위반을 드러내지 못하기 때문에 잘못된 구현이나 건전하지 않은 명세가 평가를 통과하는, 모델 능력에 대한 과대평가를 초래합니다.

방법론: VeriScale 프레임워크

이러한 한계를 해결하기 위해 저자들은 검증 가능한 코드 생성을 위한 테스트スイ트를 체계적으로 확장하고 정제하기 위해 적대적 구현에 기반한 새로운 프레임워크인 VeriScale을 제안합니다. 이 프레임워크는 테스트 스위트 확장과 테스트 스위트 축소라는 두 가지 주요 단계로 운영됩니다.

1. 테스트 스위트 확장

이 단계의 목표는 예상된 입력 - 출력 쌍, 예상치 못한 입력, 그리고 예상치 못한 출력을 포함하는 다양하고 도전적인 테스트 케이스 풀을 구축하는 것입니다.

• 시드 생성 및 타입 인식 변이: EvalPlus 에서 영감을 받아, VeriScale 은 초기 시드 입력을 합성하기 위해 LLM 을 사용합니다. 이러한 시드들은 그런 다음 반복적이고 타입을 인식하는 변이 전략을 통해 확장됩니다. 이 프레임워크는 입력 타입을 유지하면서 구조적 교란을 도입하는 5-튜플 프로세스 ($M = (T, D, O, p, q)$) 로 변이를 형식화합니다. 여기에는 '재료 풀'에서 문맥적 값을 재사용하거나 타입별 휴리스틱을 적용하여 복잡한 엣지 케이스를 생성하는 작업이 포함됩니다.
• 전제조건 기반 입력 분류: 후보 입력들은 Lean 의 2 단계 검증 파이프라인을 사용하여 실제 전제조건에 대해 엄격하게 분류됩니다.
  • 구문 필터: 후보들이 구문적으로 유효한 Lean 표현식인지 확인합니다.
  • 양방향 검증: #guard decide와 타당한 증명 탐색을 사용하여 입력을 "예상된"(전제조건을 만족하는) 또는 "예상치 못한"(전제조건을 위반하는) 것으로 분류합니다.
• 예상치 못한 출력의 적대적 합성: 이것이 핵심 혁신입니다. LLM 이 임의의 잘못된 출력을 환각하도록 의존하는 대신, VeriScale 은 적대적 구현을 합성합니다.
  • 유능한 모델이 '레드 팀' 역할을 수행하여 문제의 형식 명세를 생성합니다.
  • 다른 모델 (또는 다른 역할의 동일한 모델) 은 이러한 명세의 약점을 악용하도록 설계된 적대적 구현을 제작하려 시도합니다.
  • 이러한 구현들은 예상된 입력에서 실행됩니다. 만약 적대적 구현이 실제 값과 다른 출력을 생성하지만 생성된 사후조건에 의해 부정확하게 수용된다면, 이 출력은 고품질의 "예상치 못한 출력"으로 유지됩니다. 이 프로세스는 테스트 케이스가 명세 건전성을 드러내는 데 진정으로 유익하도록 보장합니다.

2. 테스트 스위트 축소

확장된 스위트의 계산 비용을 관리하기 위해 VeriScale 은 대규모 풀을 간결하면서도 차별화된 스위트로 정제하기 위해 축소 전략을 사용합니다.

• 경계 보존 축소 (예상치 못한 입력용): 무작위 샘플링 대신, 이 전략은 빈 컨테이너, 0 값, 길이 불일치와 같은 일반적인 경계 위반에 해당하는 입력을 우선시합니다. 일반적인 전제조건 위반을 커버하기 위해 중요한 경계 버킷에서 대표 예제를 유지합니다.
• 적대자 제거 축소 (예상된 입력용): 이 전략은 확장 단계에서 합성된 적대적 구현을 재사용합니다. 각 예상된 입력 - 출력 쌍은 얼마나 많은 '돌연변이'(적대적) 구현을 '제거'(즉, 다른 출력을 생성) 할 수 있는지에 따라 평가됩니다. 축소는 집합 커버 문제로 형식화되어, 이전에 제거되지 않은 돌연변이들을 최대한 많이 커버하는 쌍을 탐욕적으로 선택합니다. 이는 축소된 스위트가 결함이 있는 명세를 구별할 수 있는 능력을 유지하도록 보장합니다.

주요 기여

1. VeriScale 프레임워크: 저자들은 검증 가능한 코드 생성을 위한 테스트 스위트의 체계적인 확장과 축소를 주도하기 위해 적대적 구현을 활용하는 일반적 프레임워크를 제안합니다.
2. VERINAPLUS 및 VERINALITE: 이 프레임워크는 VERINA 벤치마크에 적용되어 두 가지 새로운 데이터셋을 생성합니다.
   • VERINAPLUS: 테스트 스위트가 83 배 이상 확장된 확장 벤치마크입니다 (구체적으로 예상된 입력은 62.83 배, 예상치 못한 출력은 87.79 배, 예상치 못한 입력은 183.08 배).
   • VERINALITE: 축소 전략을 통해 최적화된 경량 변형으로, 평가 비용을 낮추면서도 차별화 능력을 유지하도록 14 배 확장되었습니다.
3. 실증적 검증: 이 논문은 기존 벤치마크가 모델 능력을 현저히 과대평가하고 있음을 보여줍니다. 강화된 벤치마크는 이전에 숨겨져 있던 최첨단 LLM 의 상당한 약점을 드러냅니다.

실험 결과

저자들은 VERINA, VERINAPLUS, VERINALITE 에서 GPT-5.5, Claude-Sonnet-4.6, DeepSeek-V4-Pro 를 포함한 8 개의 최첨단 LLM 을 평가했습니다.

• 모델 약점 노출: 강화된 벤치마크는 급격한 성능 저하를 초래했습니다. 예를 들어, GPT-5.5는 VERINA 에서 **68.78%**였던 SpecGen 점수가 VERINAPLUS 에서 **44.44%**로 급락했고, CodeGen 점수도 **96.83%**에서 **86.24%**로 하락했습니다. 이는 기존 벤치마크의 희소한 테스트 케이스가 모델들이 진정한 이해 없이 통과할 수 있게 했음을 시사합니다.
• 평가 불확실성 감소: 확장된 테스트 스위트는 SpecGen 평가에서 오차 범위를 크게 좁혔습니다. 기존 벤치마크에서는 불확실한 검증 결과가 상한과 하한 사이에 넓은 간격 (예: Claude-Opus-4.7 의 경우 13.23% 간격) 을 만들었습니다. VERINAPLUS 에서는 이러한 모호함이 해결되어 간격이 **4.76%**로 축소되었으며, 이는 더 통계적으로 신뢰할 수 있는 평가를 제공합니다.
• 강건성 격차: 결과는 근본적인 불균형을 강조합니다. 모델들은 SpecGen 보다 CodeGen 에 훨씬 더 능숙합니다. CodeGen 점수는 moderate 한 하락을 보인 반면, SpecGen 점수는 급격히 하락하여 건전하고 완전한 형식 명세를 합성하는 것이 현재 LLM 에게 여전히 주요 병목 현상임을 시사합니다.
• 축소의 효율성: VERINALITE 는 VERINAPLUS 와 거의 동일한 성능 저하 프로파일을 달성하면서도 계산 오버헤드를 크게 줄였습니다. VERINALITE 의 평가 시간은 전체 VERINAPLUS 스위트의 1.80 배(SpecGen) 및 1.50 배(CodeGen)에 비해 각각 1.38 배(SpecGen) 및 1.05 배(CodeGen)의 기준 시간만 소요되었습니다.

중요성과 주장

이 논문은 VeriScale 이 LLM 기반 검증 가능 코드 생성을 발전시키기 위한 중요하고 매우 신뢰할 수 있는 기준을 제공한다고 주장합니다. 희소한 긍정적 테스트를 넘어 적대적으로 합성된 부정적 케이스를 포함함으로써, 이 프레임워크는 모델 능력을 과대평가하지 않도록 하는 더 엄격한 평가를 제공합니다.

저자들은 VeriScale 을 기존 노력과 보완적인 것으로 위치시킵니다. 새로운 작업을 도입하는 대신, 테스트 신호의 품질과 양을 확장함으로써 기존 벤치마크를 강화합니다. 이 작업은 현재 모델들의 형식 추론 작업에서의 취약성을 드러내기 위해 적대적 테스트 확장이 필수적임을 강조합니다.

인정된 한계:
저자들은 VeriScale 이 실제 전제조건과 참조 구현의 가용성에 의존한다고 지적합니다. 또한, 합성된 예상치 못한 출력의 품질은 '레드 팀' 역할을 수행하는 LLM 의 추론 능력에 의해 제한됩니다. 마지막으로, 구축 단계는 막대한 LLM 샘플링과 Lean 실행이 필요하여 계산 집약적입니다.

향후 작업:
저자들은 VeriScale 을 결함이 있는 명세를 수정하는 모델을 안내하는 폐쇄 루프 수리 시스템으로 발전시킬 것을 제안합니다. 또한, 전용 자동 형식화 모델을 위한 학습 코퍼스를 합성하기 위해 VeriScale 을 적대적 데이터 엔진으로 사용하고, Dafny 와 같은 다른 검증 백엔드로 프레임워크를 일반화할 계획을 가지고 있습니다.