Papers·2주 전
Galois, 실제 Python PBT에서 Lean4 명세 9,415개 생성 — AI 형식 검증 벤치마크 공개
Galois 팀이 실제 Python 저장소에서 11,039개의 property-based test(PBT)를 수집하고, 이 중 2,772개를 Lean4 명세로 자동 변환한 벤치마크를 공개했습니다. PBT당 평균 3.4개의 명세를 생성했으며, 3-에이전트 LLM 파이프라인으로 Python 시맨틱을 Lean에 모델링하고 논리 속성을 추론했습니다. 코드와 데이터는 모두 오픈소스이며, AI 기반 실제 소프트웨어 형식 검증 연구를 위한 기반을 제공합니다.
Galois 팀이 실제 Python 코드의 property-based test를 Lean4 명세로 변환한 대규모 벤치마크를 공개했습니다.
핵심 결론
- 데이터 — 11,039 PBT 중 2,772개를 Lean4 명세로 변환, 총 9,415개의 명세 생성 (PBT당 평균 3.4개).
- 변환율 — 25%의 PBT만 자동 변환 가능 — Python 시맨틱과 의존 타입의 차이가 주요 병목.
- 공개 — 스크래퍼, 에이전트 코드, 데이터셋 모두 오픈소스로 공개.
방법
- 파이프라인 — 3-에이전트 LLM 파이프라인: 하나는 Python PBT 분석, 하나는 Lean 명세 초안, 하나는 검증 및 수정.
- 명세 구조 — 각 명세는 sorry 플레이스홀더를 포함해 증명되지 않은 상태로 제공 — 증명 생성 벤치마크로 사용 가능.
- 변환 과정에서 Python의 동적 타입과 부수 효과를 Lean의 순수 함수형 모델로 매핑하는 것이 핵심 과제였습니다.
한계·조건
- 커버리지 — 25%만 변환 가능 — 나머지 75%는 LLM이 처리하지 못한 복잡한 패턴이나 라이브러리 의존성 때문.
- 품질 — 자동 변환된 명세 중 일부는 Python 원본의 의미를 완전히 포착하지 못할 수 있음.
- 벤치마크 — 증명 생성 baseline은 제공하지만, 아직 인간 전문가 수준의 형식 검증과는 거리가 있음.
편집자 한 줄
AI 생성 코드가 늘어나는 시점에서 실제 소프트웨어에 대한 형식 검증 벤치마크가 공개된 점은 의미 있습니다. 다만 변환율 25%는 아직 갈 길이 멀다는 걸 보여주네요.
- #formal-verification
- #lean4
- #python
- #galois
- #benchmark
Galois Inc