CLEVER: A Curated Benchmark for Formally Verified Code Generation
Created by
Haebom
저자
Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzche, Greg Durrett, Yisong Yue, Swarat Chaudhuri
개요
본 논문은 Lean을 사용한 종단 간 검증 코드 생성을 위한 고품질의 큐레이션된 벤치마크인 CLEVER를 소개합니다. CLEVER는 161개의 문제로 구성되며, 각 문제는 (1) 보류된 정답 사양과 일치하는 사양 생성 작업과 (2) 이 사양을 증명 가능하게 만족하는 Lean 구현 생성 작업으로 이루어집니다. 기존 벤치마크와 달리 CLEVER는 테스트 케이스 감독, LLM 생성 주석, 구현 논리를 유출하거나 공허한 솔루션을 허용하는 사양을 피합니다. 모든 출력은 Lean의 형식 검사기를 사용하여 사후 검증되어 기계로 확인 가능한 정확성을 보장합니다. 본 논문에서는 CLEVER를 사용하여 최첨단 언어 모델을 기반으로 하는 여러 몇 샷 및 에이전트 접근 방식을 평가합니다. 이러한 방법들은 모두 완전한 검증을 달성하는 데 어려움을 겪어 프로그램 합성 및 형식적 추론에 대한 어려운 최첨단 벤치마크임을 입증합니다. 벤치마크는 GitHub(https://github.com/trishullab/clever)와 HuggingFace(https://huggingface.co/datasets/amitayusht/clever)에서 확인 가능하며, 모든 평가 코드 또한 온라인(https://github.com/trishullab/clever-prover)에서 사용 가능합니다.
시사점, 한계점
•
시사점: 종단 간 검증 코드 생성을 위한 새로운 고품질 벤치마크 CLEVER를 제공합니다. 기존 벤치마크의 한계를 극복하고, 기계로 확인 가능한 정확성을 보장합니다. 최첨단 언어 모델 기반 접근 방식의 한계를 보여주며, 프로그램 합성 및 형식적 추론 분야의 새로운 연구 방향을 제시합니다.
•
한계점: 현재 벤치마크의 문제 수(161개)는 상대적으로 제한적일 수 있습니다. 평가된 모델들이 완전한 검증에 어려움을 겪는다는 것은 벤치마크의 난이도가 높다는 것을 의미하며, 모든 유형의 코드 생성 문제를 포괄하지 못할 수 있습니다.
