FVSpec: Lean 챌린지로서의 실제 환경 속 속성 기반 테스트

우리는 실제 환경의 형식 소프트웨어 검증 (formal software verification) 작업에 대해 AI 모델과 에이전트를 평가하기 위한 벤치마크를 제시합니다. 우리는 먼저 실제 Python 저장소로부터 11,039개의 속성 기반 테스트 (Property-Based Tests, PBTs)를 스크래핑한 다음, 그 중 2,772개 (25%)를 sorry 플레이스홀더가 포함된 9,415개의 Lean 4 명세 (specifications)로 자동 번역합니다 (PBT당 약 3개의 형식화 결과; 품질 지표에서 압도적인 것이 없을 경우 여러 시도를 유지합니다). PBT를 Lean 명세로 번역하는 것은 매우 도전적인 과제입니다. 이는 Lean에서 Python의 의미론 (semantics)을 모델링하고, 명령형 (imperative) PBT에 인코딩된 논리적 속성을 추론하며, 잘 사용되지 않는 언어에서 의존 타입 프로그래밍 (dependently-typed programming)의 내재된 어려움을 처리하는 것을 요구합니다. 우리는 PBT를 Lean 명세로 트랜스파일링 (transpiling)하기 위한 3-에이전트 LLM 파이프라인을 설명하고, 커버리지 및 품질 지표를 평가하며, 여러 자동화 및 모델 기반 접근 방식을 사용하여 증명 생성 (proof generation)을 위한 베이스라인을 제공합니다. 모든 코드 (스크래퍼 및 에이전트)와 데이터 (PBT 및 Lean 명세)는 오픈 소스입니다. 우리의 벤치마크는 AI가 전 세계 코드의 점점 더 많은 부분을 생성함에 따라 관심이 높아지고 있는, 아직 충분히 탐구되지 않은 문제인 실제 소프트웨어의 AI 지원 형식 검증 (AI-assisted formal verification) 분야의 발전을 도모하는 것을 목표로 합니다.