기술 요약: VeriContest

문제 제기

대규모 언어 모델 (LLM) 은 자연어로부터 실행 가능한 코드를 생성하는 데 능숙함을 입증해 왔으나, 그 출력물은 형식적 정확성 보장을 결여하고 있습니다. 기존 테스트 기반 접근법은 프로그램 동작을 샘플링할 뿐 기능적 오류나 보안 결함의 부재를 보장하지 못합니다. 형식적 검증 (Formal Verification) 은 코드가 형식적 명세를 만족함을 기계가 검증 가능한 증명으로 요구함으로써 더 강력한 대안을 제시합니다. 그러나 "검증 가능한 코드 생성"—즉, 모델이 코드, 형식적 명세, 그리고 증명을 동시에 생성해야 하는 작업—의 진전은 엄격한 벤치마크의 부재로 인해 방해받고 있습니다. 현재 벤치마크들은 종종 규모가 작거나, 고립된 파이프라인 단계 (예: 코드 또는 증명만) 에 초점을 맞추거나, 기준이 되는 참증명 (ground-truth proofs) 이 없거나, 주류 소프트웨어 개발과 단절된 검증 환경을 대상으로 합니다.

방법론

저자들은 VeriContest를 소개합니다. 이는 LeetCode 와 Codeforces 에서 발췌한 946 개의 경쟁 프로그래밍 문제로 구성된 벤치마크로, Verus 검증 프레임워크를 사용하여 Rust로 검증 가능한 코드 생성을 위해 특별히 설계되었습니다.

벤치마크 구축 파이프라인

VeriContest 는 고품질과 규모를 보장하기 위해 3 단계 파이프라인을 통해 구축되었습니다:

1. 1 단계 (수동 구축): 전문가들이 91 개의 "시드 (seed)" 문제를 수동으로 구축했습니다. 각 문제에 대해 형식적 명세 (사전 조건 및 사후 조건), 심사자가 승인한 Rust 코드, 그리고 Verus 로 검증된 증명을 작성했습니다. 이러한 명세들은 정합성 (soundness, 모든 올바른 해결책이 명세를 만족함) 과 완전성 (completeness, 명세를 만족하는 모든 해결책이 올바름) 을 위해 엄격하게 검증되었습니다.
2. 2 단계 (반자동 확장): GPT-5.3-Codex 를 기반으로 한 LLM 에이전트가 벤치마크를 946 개 문제로 확장했습니다. 이 단계에는 "휴먼-인-더-루프 (human-in-the-loop)" 검토 프로세스가 적용되었습니다. 에이전트는 부동소수점 연산이나 복잡한 자료구조와 같이 지원되지 않는 Rust 기능을 요구하는 문제를 필터링하고, 명세, 코드, 증명을 생성했습니다. 인간 전문가들은 온라인 심사자 승인, 수동 명세 검토, 그리고 독립적인 Verus 검증을 통해 출력을 검증했습니다.
3. 3 단계 (테스트 케이스 생성 및 검증): 사후 조건의 완전성을 검증하기 위해 저자들은 양 (+) 과 음 (-) 테스트 세트를 생성했습니다.
   • 양성 테스트: 유효한 입력을 생성하는 Verus 검증 생성기 프로그램을 합성하여 생성되었습니다.
   • 음성 테스트: 변형 테스트 (의미론적, 구문론적, 직접 출력 변형) 를 통해 잘못된 출력과 짝을 이루는 입력을 생성하여 생성되었습니다.
   • Post2Exe: 지원되는 Verus 사후 조건을 실행 가능한 Rust 프로그램으로 변환하는 새로운 도구입니다. 이러한 프로그램은 음성 테스트 케이스와 함께 실행되어 부정확한 출력을 허용하는 불완전한 사후 조건을 자동으로 탐지하고 플래그를 지정하며, 이는 수정을 위해 다시 보내집니다.

평가 프로토콜

VeriContest 는 네 가지 핵심 작업에 걸쳐 고립된 (isolated) 과 구성적 (compositional) 평가를 모두 지원합니다:

• SpecGen: 자연어로부터 형식적 명세를 생성합니다.
• CodeGen: 자연어, 명세, 또는 둘 다로부터 실행 가능한 코드를 생성합니다.
• ProofGen: 주어진 명세와 코드에 대해 Verus 증명을 생성합니다.
• End-to-End: 자연어 설명으로부터 전체 검증된 프로그램 (명세, 코드, 증명) 을 생성합니다.

평가는 pass@1 정확도를 측정하며, 증명 수정 (repair@k) 과 샘플링 (pass@k) 을 위한 추가 지표를 포함합니다.

주요 기여

1. VeriContest 벤치마크: 전문가 검증 Verus 명세, 심사자 승인 Rust 코드, 기준 참증명 (ground-truth Verus proofs), 그리고 포괄적인 양/음성 테스트 세트를 갖춘 946 개의 경쟁 프로그래밍 문제로 구성된 대규모 데이터셋.
2. 구축 파이프라인: 수동 시드 생성, 휴먼 검토를 통한 반자동 확장, 그리고 Post2Exe 를 통한 사후 조건 완전성의 자동 테스트 기반 검증을 결합한 확장 가능한 3 단계 방법론.
3. 모듈식 평가 프레임워크: 명세, 코드, 증명 생성을 고립시키면서도 엔드투엔드 합성을 평가하여 병목 현상을 세밀하게 분석할 수 있는 프로토콜.
4. 실증 분석: GPT-5.5, Claude Opus 4.7, DeepSeek V4 를 포함한 10 개의 최첨단 LLM 에 대한 평가로, 표준 코딩과 검증 가능한 코드 생성 간의 상당한 성능 격차를 드러냄.

결과

VeriContest 에 대한 10 개의 최첨단 모델 평가는 코드 생성에서 전체 검증으로 작업 복잡도가 증가함에 따라 성능이 급격히 저하됨을 보여줍니다:

• 코드 생성 (CodeGen): 모델들은 상대적으로 잘 수행합니다. 가장 강력한 모델인 GPT-5.5는 자연어-코드 생성에서 **92.18%**의 정확도를 달성합니다. 그러나 입력이 형식적 명세만일 경우 성능은 크게 하락하여 (67.65%), 모델들이 자연어 문제 진술보다는 형식적 논리 제약에 더 익숙하지 않음을 시사하는 훈련 분포 불일치를 나타냅니다.
• 명세 생성 (SpecGen): 성능이 급격히 떨어집니다. GPT-5.5 는 자연어-명세 생성에서 **48.31%**만 달성하며, 오픈소스 모델들은 훨씬 더 나쁜 성능을 보입니다 (예: Qwen 3.6 의 0.32%). 이는 LLM 이 코드보다 형식적 명세 구문과 의미론에 훨씬 덜 익숙함을 나타냅니다.
• 증명 생성 (ProofGen): 이는 주요 병목 현상으로 식별됩니다. 기준 참명세와 코드가 제공되더라도 GPT-5.5 는 **13.95%**의 정확도만 달성합니다. 대부분의 모델은 8% 미만으로 머뭅니다.
• End-to-End: 처음부터 완전히 검증된 프로그램을 생성하는 성공률은 극히 낮습니다. GPT-5.5 는 **5.29%**에 불과합니다. 저자들은 엔드투엔드 성공은 명세, 코드, 증명이 완벽하게 정렬되어야 하며, 단일 구성 요소의 실패가 전체 파이프라인의 실패로 이어진다고 지적합니다.

오류 분석:

• CodeGen: 강력한 모델들의 경우 잘못된 출력이 주된 오류이나, 형식적 명세가 포함되면 구문 오류로 전환됩니다.
• ProofGen: 지배적인 실패 모드는 검증 실패 (Verification Failure, 증명이 검증기를 만족하지 못함) 와 명세/코드 수정 (Spec/Code Modification, 모델을 증명 추가 대신 제공된 코드/명세를 변경함) 입니다.
• SpecGen: 오류는 Verus 의 구문 오류가 압도적으로 많으며, 이어 사전/사후 조건 불일치가 뒤따릅니다.

중요성과 주장

이 논문은 VeriContest 가 기계가 검증 가능한 정확성을 갖춘 코드를 생성할 수 있는 미래 시스템을 측정하고 훈련하기 위한 엄격한 플랫폼을 확립한다고 주장합니다. 저자들은 다음과 같이 주장합니다:

• 증명 및 명세 생성은 현재 LLM 의 검증 가능한 코드 생성 파이프라인에서의 핵심 병목 현상입니다.
• 모델이 코드를 작성하는 능력과 이를 형식적으로 검증하는 능력 사이에는 상당한 격차가 존재합니다.
• 엔드투엔드 성공은 현재 코드 생성뿐만 아니라 명세, 코드, 증명을 일관된 전체로 정렬하는 어려움에 의해 제한됩니다.
• 이 벤치마크는 단순한 기능적 정확성을 넘어 형식적 보장을 목표로 검증 가능한 코드 생성에 대한 모델 훈련을 위한 감독 자료 역할을 합니다.

저자들은 범위에 대해 겸손하게 접근하며, VeriContest 가 Rust/Verus 와 경쟁 프로그래밍 문제로 제한되며 시스템 코드, 분산 프로토콜, 또는 Dafny 나 Lean 과 같은 다른 검증 프레임워크를 아직 다루지 않는다고 인정합니다. 그들은 향후 연구가 도구와 모델 능력의 향상과 함께 더 많은 언어와 영역으로 확장되어야 한다고 제안합니다.