[Paper] VeriSoftBench: 레포지토리 규모 형식 검증 벤치마크 for Lean

Source: arXiv - 2602.18307v1

개요

이 논문은 VeriSoftBench라는 새로운 벤치마크 스위트를 소개한다. 이 스위트는 실제 오픈‑소스 소프트웨어‑검증 프로젝트에서 수집한 500개의 Lean 4 증명 과제로 구성되어 있다. 기존에 순수 수학(예: Mathlib)에 초점을 맞춘 LLM‑기반 정리‑증명 벤치마크와 달리, 이 데이터셋은 전체 저장소 컨텍스트—파일 간 임포트, 사용자 정의 라이브러리, 그리고 깊은 의존성 그래프—를 보존한다. 따라서 언어‑모델 기반 및 전통적인 자동 증명기 모두에 대해 보다 현실적인 테스트베드 역할을 한다.

주요 기여

• 레포지토리 규모 벤치마크: 다양한 공개 형식 방법 코드베이스에서 추출한 500개의 Lean 4 검증 과제.
• 컨텍스트 보존 패키징: 각 과제는 정확한 전이 의존성 클로저와 함께 제공되어 실제 개발 환경을 반영한 재현 가능한 실험을 가능하게 함.
• 포괄적 평가: 최첨단 대형 언어 모델(GPT‑4, Claude 등)과 특화된 프로버를 벤치마크하여 Mathlib 스타일 수학에서 소프트웨어 검증 코드로 전환할 때 나타나는 체계적인 격차를 밝혀냄.
• 실증적 통찰: 전이 가능성, 의존성 복잡성, 증명 자동화를 위한 선별된 컨텍스트의 가치에 관한 세 가지 핵심 관찰.
• 오픈소스 공개: 벤치마크 데이터, 평가 스크립트, 기본 결과가 GitHub에 공개되어 있음.

방법론

1. Data collection – The authors mined popular Lean 4 verification repositories (e.g., verification of compilers, operating‑system kernels, and security‑critical libraries). They extracted individual theorem/lemma statements that were not already proved automatically.
2. Dependency extraction – For each proof obligation, a static analysis pass identified all imported modules, definitions, and lemmas required to type‑check the statement. The full transitive closure was packaged as a self‑contained Lean project.
3. Benchmark design – Tasks were split into three difficulty tiers based on the size of their dependency closure (small, medium, large).
4. Evaluation pipeline –
   • LLM‑based provers: Prompts were constructed to feed the target statement plus either the whole repository, the curated dependency closure, or no extra context. The LLM generated proof scripts which were then type‑checked by Lean.
   • Specialized provers: Tools such as leanprover-community/lean4’s simp, omega, and external SAT/SMT back‑ends were run with identical context settings.
5. Metrics – Success rate (proof fully type‑checked), time‑to‑proof, and token usage for LLM prompts were recorded.

결과 및 발견

• Transfer gap: Mathlib 증명에 뛰어난 도구들이 저장소 중심 검증 작업에 직면하면 성공률이 크게 떨어집니다.
• Dependency depth matters: 많은 전이적 임포트를 필요로 하는 증명은 해결될 가능성이 대략 세 배 낮습니다.
• Curated context helps: 최소 종속성 클로저만 제공하면 전체 저장소에 비해 LLM 성능이 약 50 % 향상되지만, 절대 성공률은 여전히 낮아 보다 스마트한 컨텍스트 선택이나 추론 메커니즘의 개선 여지가 큽니다.

Practical Implications

• 산업 규모 검증을 위한 도구: 형식 검증된 소프트웨어(예: 안전‑중요 드라이버, 암호화 라이브러리)를 구축하는 기업은 이제 LLM‑지원 증명 자동화의 준비 상태를 평가하기 위해 “Mathlib‑only” 벤치마크에 의존할 수 없습니다. VeriSoftBench는 현실적인 기준을 제공합니다.
• 컨텍스트 관리 API: 연구 결과는 IDE와 CI 파이프라인이 자동 의존성‑제거 유틸리티를 도입하여 증명기에 필요한 Lean 파일만 제공함으로써 LLM API의 토큰 비용을 줄이고 지연 시간을 개선해야 함을 시사합니다.
• 하이브리드 증명기 아키텍처: 정제된 컨텍스트에서 얻은 다소 제한적인 향상은 두 단계 접근법—먼저 최소 클로저를 계산하는 빠른 정적 분석기, 그 다음 LLM 또는 SMT 백엔드—이 검증 파이프라인에서 표준 패턴이 될 수 있음을 암시합니다.
• 벤치마크 기반 연구: 새로운 프롬프트 전략, 검색‑보강 생성, 혹은 도메인‑특화 파인‑튜닝을 개발하는 연구자들은 이제 실제 코드베이스의 복잡성을 반영한 데이터셋을 기준으로 평가할 수 있어, 실용적인 검증 도우미 개발을 가속화할 수 있습니다.

Limitations & Future Work

• Domain coverage: 500개의 작업이 여러 검증 프로젝트에 걸쳐 있지만, 벤치마크는 여전히 학술용 오픈‑소스 저장소에 편향되어 있습니다; 산업용 독점 코드는 더 풍부한 의존성 그래프를 가질 수 있습니다.
• Static dependency extraction: 현재 접근 방식은 필요한 모든 import가 정적으로 발견 가능하다고 가정합니다; Lean의 동적 메타‑프로그래밍 패턴은 추가 요구사항을 숨길 수 있습니다.
• LLM prompting scope: 소수의 주요 LLM만 테스트되었습니다; 향후 작업에서는 체인‑오브‑쓰레드 프롬프트, 도구 사용 확장(예: Lean의 simp 자동 호출) 또는 검증 전용 코퍼스에 대한 파인‑튜닝을 탐색할 수 있습니다.
• Metric breadth: 성공률은 이진형이며; 증명 길이, 인간 가독성, 혹은 다운스트림 유지보수 비용과 같은 더 풍부한 지표는 측정되지 않았습니다.

The authors plan to expand VeriSoftBench with more projects, add multi‑language support (e.g., Coq, Isabelle), and provide a leaderboard to track progress across the community.

저자

• Yutong Xin
• Qiaochu Chen
• Greg Durrett
• Işil Dillig

논문 정보

• arXiv ID: 2602.18307v1
• Categories: cs.SE, cs.CL, cs.LG, cs.PL
• Published: 2026년 2월 20일
• PDF: Download PDF