FVSpec: Real-World Property-Based Tests as Lean Challenges

기술 요약: FVSpec

문제 정의

본 논문은 실제 세계의 소프트웨어를 위한 AI 지원 형식 검증(Formal Verification, FV) 분야의 결정적인 공백을 다룹니다. AI 안전성 제안들은 점차 자율 에이전트가 AI가 생성한 코드를 형식적으로 검증하는 것에 의존하고 있지만, 현재의 벤치마크들은 이 목표를 지원하기에 부족합니다. 기존 벤치마크(예: Minif2f, PutnamBench)는 수학 올림피아드 문제나 전문가가 작성한 정리 증명기(Theorem Prover) 코드에 집중되어 있으며, 이는 "일반적인" 소프트웨어 엔지니어링 환경과는 크게 다릅니다. 실제 세계의 소프트웨어는 복잡한 의존성 트리, 블랙박스 외부 API, 그리고 서로 다른 언어로 작성된 컴포넌트들을 포함하며, 이는 폐쇄형 모놀리식 시스템보다 본질적으로 검증하기 더 어렵습니다. 또한, 형식 검증 의도 없이 엔지니어들이 작성한 코드로 구성된 고품질의 대규모 데이터셋이 부족하며, 이는 모델이 학습 데이터와 대비하여 "분포 외(out-of-distribution)" 상황에서 작동할 수 있는 에이전트를 훈련하는 데 필수적입니다.

방법론

저자들은 실제 세계의 속성 기반 테스트(Property-Based Tests, PBT)를 Lean 4 기반의 형식 검증 과제로 변환하는 벤치마크 생성 파이프라인인 FVSpec을 소개합니다. 이 과정은 세 가지 주요 단계로 구성됩니다:

1. 데이터 수집 (FVSpec:PBT):

   • 팀은 Hypothesis 프레임워크를 사용하여 333개의 오픈 소스 Python 저장소로부터 11,039개의 고유한 PBT를 스크래핑했습니다.
   • 저장소는 허용 가능한 라이선스를 기준으로 필터링되었으며, 다양성을 확보하기 위해 중복 항목(포크 포함)을 제거했습니다.
   • 결과물인 코퍼스는 단순한 단언(assertion)부터 복잡한 다중 전략 테스트에 이르기까지, "평범한" 소프트웨어 엔지니어링을 나타냅니다.

2. 에이전트 기반 트랜스파일링 (FVSpec:FV):

   • 세 개의 에이전트로 구성된 LLM 파이프라인이 Python PBT와 관련 코드를 Lean 4로 번역합니다.
   • 함수 발견 (Function Discovery): tree-sitter를 사용하여 테스트 대상 함수(Function Under Test, FUT)와 그 국소적 의존성들의 추이적 폐쇄(transitive closure)를 추출합니다.
   • 번역 (Translation): 공식화 에이전트는 두 개의 파일, 즉 Impl.lean(함수의 계산 가능한 포팅 버전)과 Spec.lean(PBT 단언에 대응하는 정리 문구이며, 증명은 sorry 플레이스홀더로 남겨둠)을 생성합니다.
   • 반복 수선 (Iterative Repair): 파이프라인은 LSP(Language Server Protocol) 루프를 활용합니다. 생성된 Lean 코드가 컴파일에 실패하면(lake build 사용), 컴파일러 진단 결과가 에이전트에게 피드백되어 수정을 유도합니다. 이 루프는 최대 16회 반복됩니다.
   • 부작용 처리 (Handling Effects): 부작용(예: Redis, 파일 I/O)이 포함된 코드의 경우, 에이전트는 이러한 외부 시스템을 해석되지 않는 인터페이스(uninterpreted interfaces)로 공리화(axiomatize)합니다. 정리는 이러한 공리들을 바탕으로 기술되며, 이를 통해 구체적인 구현 세부 사항은 추상화되더라도 코드의 로직에 대한 증명 의무가 유의미하게 유지되도록 합니다.

3. 사후 생산 및 필터링:

   • 생성된 샘플들은 엄격한 검증 과정을 거칩니다. 실패 사례는 유형별(예: 타임아웃, 타입 불일치, 알 수 없는 식별자)로 분류됩니다.
   • 다섯 가지 하위 지표(파라미터 커버리지, 타입 대응성, 전략 커버리지, 단언 커버리지, 의존성 커버리지)를 기반으로 "구조적 충실도(structural faithfulness)" 점수를 계산합니다.
   • 보정된 LLM 판사(claude-haiku-4-5)를 사용하여 샘플의 난이도(Easy/Hard)를 등급화합니다.
   • 단일 시도가 품질 지표에서 압도적이지 않을 경우, 하나의 PBT당 여러 개의 공식화 버전을 유지하도록 하여, 최종적으로 2,772개의 고유한 PBT로부터 유도된 9,415개의 챌린지를 확보합니다.

주요 기여

1. FVSpec:PBT: 오픈 소스 저장소에서 스크래핑한 11,039개의 중복 제거된 Python PBT 코퍼스로, 일반적인 소프트웨어 개발(경쟁 프로그래밍이나 큐레이션된 ITP 코드 제외)에서 추출한 최초의 대규모 라이선스 클린 데이터셋입니다.
2. FVSpec:FV: 9,415개의 Lean 4 형식 검증 챌린지 데이터셋입니다. 각 챌리지는 원본 Python 코드, 원본 PBT, Lean 구현체, 그리고 증명 의무가 포함된 Lean 정리 문구를 포함합니다. 이 데이터셋은 중앙값 0.65의 구조적 충실도를 가지며, 62%의 챌린지가 "Hard"로 분류되었습니다.
3. 베이스라인 평가: 프런티어 모델들(Claude Sonnet 4.6, Claude Opus 4.7, GPT-5.4)에 대한 성능 지표를 제공합니다. 모델들은 "Easy" 문제에서 평균 70%, "Hard" 문제에서 49%의 성공률을 기록하여, 벤치마크가 아직 포화되지 않았음을 보여주었습니다.
4. 오픈 소스 공개: 전체 파이프라인(스크레이퍼, 의존성 추출기, 공식화 에이전트 및 스크립트)과 데이터셋을 MIT/Apache 이중 라이선스로 공개합니다.

결과

• 파이프라인 수율: 트랜스파일링 파이프라인은 초기 11,039개의 PBT 중 25%(9,415개 샘플)를 유효한 Lean 챌린지로 성공적으로 변환했습니다.
• 품질 지표: 구조적 충실도의 중앙값은 0.65입니다. 타입 대응성(1.00)과 단언 커버리지(0.97)는 높지만, 파라미터 커버리지(0.24)와 의존성 커버리지(0.48)는 낮아 번역 충실도가 가변적인 영역을 나타냅니다.
• 모델 성능: 베이스라인 모델들은 Easy 샘플의 70%, Hard 샘플의 49%를 해결했습니다. 거절률(Refusal rate)은 낮았으며(Easy 4–8%, Hard 3–25%), 이는 모델들이 일반적으로 과업을 수행하려고 시도함을 시사합니다.
• 복잡도: 샘플의 중앙값은 6개의 정리를 포함합니다. 데이터셋은 단순한 정렬 알고리즘부터 타임아웃과 상태 전이를 포함하는 복잡한 워크플로우 작업 스케줄러에 이르기까지 넓은 범위의 복잡도를 포함합니다.

의의 및 주장

본 논문은 FVSpec이 실제 세계의 소프트웨어를 위한 AI 지원 형식 검증을 발전시키는 데 필요한 토대를 제공한다고 주장합니다. 전문가가 작성한 증명이나 수학적 문제에 의존하는 기존 벤치마크와 달리, FVSpec은 형식 검증 의도가 없었던 엔지니어들로부터 명세를 도출합니다. 이는 모델의 학습 데이터와 대비하여 "분포 외(out-of-distribution)" 상황을 보장하며, 에이전트의 일반화 능력을 더욱 엄격하게 테스트합니다.

저자들은 이 연구를 "보장된 안전한 AI(Guaranteed Safe AI)"와 "확장 가능한 형식적 감독(Scalable Formal Oversight)"을 향한 단계로 규정합니다. 여기서 자율 에이전트는 소프트웨어를 작성하는 것만큼 빠르고 효과적으로 검증할 수 있어야 합니다. 현실적인 대규모 벤치마크을 제공함으로써, FVSpec은 합성 벤치마크에서 흔히 무시되는 외부 의존성 및 부작용을 포함한 현대 소프트웨어 생태계의 복잡성을 다룰 수 있는 에이전트 훈련의 발전을 도모하고자 합니다. 논문은 공리화 과정이 특정 부작용의 의미론을 놓칠 가능성과 난이도 보정을 위한 인간 전문가 베이스라인의 부재와 같은 한계점을 겸허히 인정하고 있습니다.