명세의 90%를 증명해도 완성된 저장소는 0개일 수 있다: Vero의 채점 경계
부분 명세 통과율과 저장소 완성을 같은 분모로 혼동하지 않는다. 명세가 두 저장소에 어떻게 분포하는지와 요구사항 자체의 누락을 예제로 설명한다.
부분 증명과 저장소 완성을 나누어 채점하기
Vero는 여러 모듈의 구현과 증명을 함께 유지하면서 저장소 전체를 빌드할 수 있는지 평가한다. 개별 명세 통과율뿐만 아니라 원본 상태에서의 재빌드, 사용한 공리의 출처, 모든 명세를 통과한 full solve 여부까지 함께 확인한다.
Lean 4로 구성한 43개 과제의 범위
Zhe Ye 외 10명이 2026.08.13 공개한 Vero 논문(arXiv v1)과 공식 저장소는 43개 multi-module Lean 4 과제, 743개 채점 대상 API, 2,705개 specification을 명시된 에이전트·모델·90분 실행 조건에서 평가한다.
일반 코딩 과제 성공률이나 인간이 작성한 소프트웨어의 형식 검증 비용은 비교하지 않는다. 대신 모델 간 단순 순위보다 저장소 완성(repository completion)의 정의와 검증 방식에 초점을 맞춘다.
수정 영역만 옮겨 독립적으로 재검사하기
proof-only 모드는 주어진 기준 구현이 모든 명세를 만족한다는 Lean 4 증명을 작성하고, code-and-proof 모드는 API 구현과 증명을 함께 만든다. 후자는 증명하기 쉬운 구현을 택할 수 있지만, 한 모듈의 변경이 다른 모듈의 증명을 깨뜨릴 수 있다.
채점기는 허용된 수정 영역만 추출해 깨끗한 원본 과제에 삽입한 뒤 다시 빌드한다. 이어서 정리의 공리 의존성을 검사하고, 명세를 무력화하거나 실행 동작과 증명 대상을 분리하는 선언이 없는지 확인한다. 모든 명세가 이 검사를 통과해야 full solve로 인정된다.
높은 통과율에도 남은 미완성 과제
GPT-5.5 (xhigh)는 code-and-proof에서 27/43, proof-only에서 25/43 저장소를 full solve했으며, 개별 specification 통과율은 각각 87.3%와 85.8%였다. 8개 에이전트-모드 구성을 모두 동원해도 10개 과제는 끝내 해결되지 않아, 높은 부분 통과율과 저장소 전체 완성 사이에 큰 간극을 보였다.
완성된 저장소들은 개별 증명을 고립시켜 처리하지 않았다. 82개 full solve 중 80개는 에이전트가 만든 helper theorem 하나를 최소 두 명세에서 재사용했다. helper theorem은 증명 코드 줄 수 중앙값 기준 code-and-proof의 73.6%, proof-only의 71.6%를 차지했다. 연구진은 미해결 과제의 원인이 국소적인 증명 기술 부족보다 공유 불변량(shared invariant)을 찾아 재사용 가능한 보조정리 라이브러리로 유지하는 능력에 있다고 분석한다.
독립 재빌드와 수정 경계를 평가에 반영하기
형식 검증 에이전트를 평가할 때는 specification pass rate와 repository full solve를 분리해야 한다. 제출물을 원본에서 다시 빌드하고 수정 가능 영역을 제한하며, 증명이 허용된 공리(axiom)에만 의존하는지 확인해야 한다. 에이전트의 작업 샌드박스를 그대로 채점하면 명세나 보조정리를 임의로 바꾼 우회(shortcut)를 놓칠 수 있다.
일반 코딩 에이전트 평가에도 같은 원리를 적용할 수 있다. 테스트 통과 개수만 보는 대신 clean checkout에 패치만 적용한 뒤 빌드·테스트·린트·보안 게이트와 최종 상태 검증기를 다시 실행해 평가 경계를 엄격히 통제하는 방식이다.
가상의 저장소 A와 B에 각각 명세가 10개 있다고 하자. 두 저장소에서 9개씩 통과하면 개별 명세 통과율은 18/20=90%지만 full solve는 0/2다. 같은 18개 통과라도 A에서 10개, B에서 8개를 통과했다면 full solve는 1/2다. 명세 총통과율이 같아도 실제로 완료된 저장소 수는 다르다. 이는 Vero 실험을 재계산한 값이 아니라 집계 단위의 차이를 보여 주는 예시다.
남은 하나의 의무가 여러 모듈이 공유하는 불변량이라면 국소 수정이 서로 충돌할 수 있다. 예를 들어 삽입과 삭제가 모두 자료구조의 정렬 조건을 유지해야 한다면, 공통 정리를 바꾸는 순간 양쪽 증명을 다시 확인해야 한다. 어떤 정리가 어디에서 재사용되는지 의존 관계를 기록하면 실패를 단순히 고립된 정리 개수로만 보지 않을 수 있다.
명세 자체도 검토 대상이다. 정렬 함수에 ‘출력이 오름차순이다’만 요구하고 ‘입력 원소를 같은 개수로 보존한다’를 빠뜨리면, 빈 배열을 반환하는 함수도 첫 조건은 만족할 수 있다. 올바른 증명 검사기는 잘못 선택한 요구사항까지 대신 고쳐 주지 않는다. clean 재빌드와 공리 검사로 증명의 유효 범위를 확인한 뒤, 그 명세가 사용자 요구를 빠짐없이 표현하는지는 별도로 살펴야 한다.
증명이 현실 요구의 완전성까지 보장하지는 않는다
Vero는 Lean 4만 다루며 Lean 구조로 옮기기 쉬운 코드에 편향돼 있다. 동시성·시간 논리 프로토콜과 점진적 유지보수 과제도 제외됐다. 공리와 충족 가능성을 검사하더라도 명세 자체가 현실의 요구사항을 빠짐없이 반영했는지는 보장하지 못하므로 사람의 검토가 필요하다.
평가표에는 87.3% 같은 부분 통과율과 저장소 전체 완성 여부를 나란히 기록해야 한다. 남은 미증명 의무와 독립 재빌드 결과를 함께 확인해야 제출물의 실제 검증 범위를 판단할 수 있다.
참고 자료
Vero: Can AI Agents Build Formally Verified Software Repositories?
Vero official repository