VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation

Motivation

• Known: 기존에는 LLM 기반 코드 생성 평가가 HumanEval, MBPP 등 단순 기능적 정확성 테스트에서 Lean 기반 formal verification을 포함하는 VERINA, CLEVER 같은 검증 가능 코드 생성(verifiable code generation) 벤치마크로 발전해 왔으며, EvalPlus 등 test-suite 확장 기법이 seed generation과 type-aware mutation을 통해 테스트 케이스를 늘려온 바 있다.
• Gap: 기존 검증 가능 코드 생성 벤치마크는 positive/negative test case의 수와 품질이 제한적이어서, 특히 잘못된 입력이나 출력을 거부하는지 검증할 고품질 unexpected input/output이 부족해 모델의 SpecGen·CodeGen 능력이 과대평가되는 문제가 있다.
• Why: test-suite의 양과 질이 벤치마크 신뢰도를 좌우하는 상황에서, 부실한 negative test case로 인해 실제로는 취약한 명세나 구현이 통과되어 모델 성능이 과대 평가되면 고위험 소프트웨어 응용에서 LLM 신뢰성 판단이 왜곡될 수 있으므로 이를 바로잡는 것이 중요하다.
• Approach: VeriScale은 적대적 구현(adversarial implementation)을 핵심 동력으로 사용해 test-suite expansion(다양하고 도전적인 테스트 생성)과 test-suite reduction(경계 보존 및 adversary-killing 축약을 통한 효율화)의 두 단계로 구성된 프레임워크를 제안한다.

Achievement

Figure 5. Performance comparison of eight models on VERINA, VERINAPLUS, and VERINALITE. The top panel shows the Code

1. VeriScale 프레임워크 제안: adversarial implementation을 활용해 test suite의 체계적 확장과 축약을 동시에 구동하는 새로운 프레임워크를 제시했다.
2. VERINAPLUS/VERINALITE 구축: VERINA에 적용해 원본 test suite를 83배 이상 확장한 VERINAPLUS와 14배 규모의 경량 VERINALITE를 만들었다.
3. 모델 취약점 노출 입증: 8개의 최신 LLM에 대해 VERINAPLUS가 SpecGen과 CodeGen에서 급격한 점수 하락을 유발함을 보였고(GPT-5.5는 SpecGen 68.78%→44.44%, CodeGen 96.83%→86.24%), 이는 기존 벤치마크의 과대평가를 드러낸다.
4. 효율적 축약 검증: VERINALITE가 VERINAPLUS와 유사한 변별력을 훨씬 적은 평가 비용으로 유지함을 실험적으로 확인했다.

How

Figure 2. A full trajectory of candidate input classification.

• 각 문제에 대해 문제 설명, ground-truth precondition, 참조 구현(reference implementation), 기존 base input을 입력으로 사용.
• Seed Generation & Type-aware Mutation: EvalPlus에서 영감을 받아 LLM으로 seed input을 생성하고 타입 인식 변이(mutation)를 적용해 대규모 후보 입력 풀을 구성.
• Classification: 생성된 후보 입력을 ground-truth precondition 기준으로 expected/unexpected input으로 분류.
• Expected input-output 생성: expected input에 대해 참조 구현을 실행하여 정답 출력 쌍을 확보.
• Adversarial Synthesis (unexpected output 생성): LLM이 생성한 명세(specification)의 허점을 노리는 adversarial implementation을 합성, expected input에 대해 실행하여 참조 출력과 다르면서도 생성된 postcondition에 의해 잘못 수락되는 출력만 선별해 unexpected output으로 채택.
• Test-Suite Reduction: 확장된 test case를 boundary-preserving reduction과 adversary-killing reduction을 통해 경계 조건과 변별력을 보존하면서 test suite 크기를 축소.
• 8개의 state-of-the-art LLM에 대해 SpecGen, CodeGen 과제로 VERINA, VERINAPLUS, VERINALITE 세 벤치마크에서 성능 비교 실험 수행.

Originality

• adversarial implementation을 test-suite 확장뿐 아니라 축약(reduction)의 구동 원리로도 재사용하는 이중 활용 아이디어가 독창적이다.
• 기존 EvalPlus류의 mutation 기반 확장 기법을 단순 코드 생성 평가를 넘어 formal specification의 soundness/completeness까지 검증하도록 precondition-guided classification과 결합해 확장했다.
• unexpected output을 무작위 생성이 아니라 명세의 허점을 실제로 공략하는 adversarial implementation을 통해 도출함으로써 negative test case의 정보성을 크게 높인 점이 새롭다.

Limitation & Further Study

• VeriScale의 효과가 현재 VERINA라는 단일 벤치마크(및 Lean 기반 검증 환경)에 대해서만 실증되어, 다른 언어(Dafny, Verus 등)나 벤치마크로의 일반화 검증이 부족하다.
• adversarial implementation 합성과 seed generation 자체가 LLM에 의존하므로, 이 과정에서 발생하는 편향이나 품질 한계가 test suite 품질에 그대로 반영될 위험이 있다.
• ProofGen 태스크에 대한 적용 및 평가는 다루지 않아, 검증 가능 코드 생성의 세 가지 축(SpecGen, CodeGen, ProofGen) 전체에 대한 완전한 검증이 이루어지지 않았다.
• 후속 연구로는 다양한 검증 프레임워크·언어로의 확장, adversarial implementation 생성 자체의 신뢰성 및 다양성 평가, ProofGen을 포함한 통합적 검증 체계 구축이 필요하다.

Evaluation

총평: 검증 가능 코드 생성 벤치마크의 근본적 한계인 test-suite 품질 문제를 adversarial implementation이라는 일관된 원리로 확장과 축약 모두에 적용해 해결한 실용적이고 잘 설계된 연구로, 벤치마크 신뢰성 향상에 실질적으로 기여한다.