VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean

1. 연구 배경 및 문제 제기 (Problem)

• 현재의 한계: 대규모 언어 모델 (LLM) 을 활용한 상호작용적 정형 증명 (Interactive Theorem Proving, ITP) 은 Lean 환경에서 괄목할 만한 성과를 거두었습니다. 그러나 기존 벤치마크 (MiniF2F, ProofNet, PutnamBench 등) 는 주로 수학 (Mathlib) 생태계에서 파생된 데이터로 구성되어 있습니다.
• 소프트웨어 검증의 차이: 소프트웨어 검증 및 프로그래밍 언어 메타이론의 증명은 공유된 수학 라이브러리가 아닌, 방대한 프로젝트 특유의 코드베이스 (Repository) 내에서 수행됩니다. 이러한 환경은 다음과 같은 특징을 가집니다:
  • 프로젝트 고유의 추상화, 정의, 라이브러리가 풍부함.
  • 증명 목표가 여러 파일 간의 복잡한 의존성 (Cross-file dependencies) 에 의존함.
  • 기존 수학 중심 벤치마크는 이러한 "저장소 규모 (Repository-scale)"의 맥락과 구조적 복잡성을 반영하지 못함.
• 핵심 질문: 현재 개발된 증명 자동화 도구들이 공유된 수학 생태계가 아닌, 대규모 프로젝트 특화 라이브러리에 기반한 증명 환경에서도 일반화될 수 있는가?

2. 방법론 (Methodology)

이 논문은 VeriSoftBench라는 새로운 벤치마크를 제안하며, 다음과 같은 방법론을 사용합니다.

• 데이터셋 구성:

  • 규모: 오픈소스 형식 검증 (Formal Methods) 프로젝트 23 개에서 추출한 500 개의 Lean 4 증명 의무 (Proof Obligations).
  • 특징: 각 태스크는 원본 Git 커밋에서 추출되어, 프로젝트 특유의 추상화와 파일 간 의존성을 그대로 보존합니다.
  • 선정 기준:
    • sorry 나 admit 같은 증명 구멍이 없는 유효한 증명 스크립트가 존재해야 함.
    • 표준 자동화 (simp, omega 등) 만으로 해결되지 않는 비자명한 (Non-trivial) 목표여야 함.
    • 프로젝트 로컬 정의를 최소 1 개 이상 참조해야 함.
  • 난이도 척도: 증명 복잡성 (스크립트 길이) 과 문맥 의존성 (참조된 정의/정리 수) 을 기준으로 선정.

• 문맥 (Context) 구성 실험:
  모델이 저장소 내 문맥을 어떻게 활용하는지 분석하기 위해 두 가지 환경을 설정했습니다.

  1. Curated Context (선별된 문맥): 정답 증명에 직접적으로 필요한 의존성 (정의, 정리) 만을 포함합니다. 불필요한 노이즈를 제거하여 모델의 추론 능력을 평가합니다.
  2. Full Repository Context (전체 저장소 문맥): 해당 프로젝트의 전체 로컬 라이브러리를 제공합니다. 이는 실제 배포 환경을 시뮬레이션하며, 모델이 관련 정보를 스스로 찾아내야 하는 과제를 부여합니다. (일부 경우 수백만 토큰에 달할 수 있음)

• 평가 파이프라인:

  • 모델: GPT-5.2, Claude Opus 4.5, Gemini-3-Pro 와 같은 일반purpose LLM 과 Goedel-Prover-V2, Aristotle 와 같은 전문 증명기를 평가.
  • 프로세스: 생성 (Generation) $\rightarrow$ 검증 (Check, Lean 컴파일러 사용) $\rightarrow$ 수정 (Repair, 에러 메시지 피드백) 의 루프를 수행.
  • 데이터 유출 방지: 증명 본체 (Proof body) 는 제거하고 정의와 명제만 제공하여 모델이 정답을 암기하거나 유출받지 않도록 함.

3. 주요 기여 (Key Contributions)

1. VeriSoftBench 벤치마크 출시:
   • 프로젝트 컨텍스트와 파일 간 의존성을 보존한 500 개의 Lean 4 태스크를 공개했습니다. 이는 기존 수학 중심 벤치마크의 공백을 메우는 첫 번째 대규모 저장소 규모 벤치마크입니다.
2. 저장소 의존성과 증명 성공의 상관관계 분석:
   • 수학 중심 벤치마크에 최적화된 증명기가 프로젝트 기반 환경에서는 성능이 급격히 떨어짐을 규명했습니다.
   • 전이적 의존성 (Transitive Dependence): 증명 성공률은 의존성 체인의 깊이 (Depth) 와 밀접한 음의 상관관계를 보입니다. 즉, 여러 단계를 거쳐 연결된 복잡한 정의 체인을 추론할 때 모델의 성능이 저하됩니다.
3. 문맥 제공 방식의 영향 분석:
   • 전체 저장소를 제공하는 것보다 정답에 필요한 문맥만 선별 (Curated) 해서 제공하는 것이 성능을 향상시키지만, 여전히 해결되지 않은 과제가 많습니다. 이는 문맥 검색 (Retrieval) 만으로는 부족하며, 복잡한 추론 능력이 필요함을 시사합니다.

4. 실험 결과 (Results)

• 모델 성능:
  • 일반 LLM: Gemini-3-Pro 가 Curated Context 에서 41.0%, Full Context 에서 34.8% 의 성공률을 보이며 가장 우수했으나, 전체적으로 낮은 성능을 보였습니다.
  • 전문 증명기: 수학 문제에 특화된 Goedel-Prover-v2 는 저장소 규모 환경에서 0% 성공률을 기록했습니다. 이는 프로젝트 특화 추상화에 대한 적응 실패를 의미합니다.
  • Aristotle: 제한된 하위 집합 (Same-file helper lemma 포함) 에서 69% 성공률을 보였으나, 이는 보조 정리가 포함된 비교적 쉬운 환경이었습니다.
• 문맥의 영향:
  • Curated Context 보다 Full Context 에서 성능이 하락했으나, 예상보다 그 격차가 작았습니다. 전체 저장소에는 목표 정리와 직접 관련되지 않더라도 유사한 추상화 패턴이나 증명 구조를 가진 파일들이 포함되어 있어, 모델이 힌트를 얻을 수 있었기 때문입니다.
• 의존성 구조의 영향:
  • 직접 의존성보다는 전이적 의존성 (Transitive Dependency) 의 깊이가 성능 저하의 주요 원인입니다. 약 50% 의 정리가 5 단계 이상의 의존성 체인을 가지며, 이는 모델이 계층적 추상화를 따라가야 하는 어려움을 가중시킵니다.
• 증명 패턴 차이:
  • 수학 벤치마크 (Verina 등) 에서는 unfold 와 simp 같은 자동화 위주의 증명이 많았으나, VeriSoftBench 에서는 케이스 분석 (Case analysis) 과 분기 구조가 훨씬 더 빈번하게 나타났습니다. 이는 프로젝트 특유의 복잡한 논리를 처리하기 위해 더 정교한 전략이 필요함을 보여줍니다.

5. 의의 및 결론 (Significance & Conclusion)

• 벤치마크의 필요성: 기존 수학 중심 벤치마크는 소프트웨어 검증의 실제 난이도 (프로젝트 특화 라이브러리, 복잡한 의존성) 를 과소평가하고 있습니다. VeriSoftBench 는 이러한 격차를 해소하고 실제 검증 환경에 적합한 평가 기준을 제공합니다.
• 향후 방향:
  • 단순한 문맥 검색 (Retrieval) 을 넘어, 계층적 추상화를 통한 다단계 추론 (Multi-hop reasoning) 능력이 증명 자동화의 핵심 과제로 부각되었습니다.
  • 대규모 저장소를 효과적으로 탐색하고 프로젝트 고유의 맥락을 이해할 수 있는 새로운 LLM 아키텍처 및 학습 방법론의 개발이 요구됩니다.

결론적으로, 이 논문은 형식 검증 분야에서 LLM 의 현재 한계를 명확히 드러내며, 실제 소프트웨어 공학 환경에 부합하는 새로운 벤치마크와 평가 체계를 제시함으로써 연구 방향을 전환시키는 중요한 역할을 합니다.