AI 에이전트의 정형 검증 코드 작성 능력, 저장소 단위로 측정한다

Vero 연구진의 공식 프로젝트 페이지와 arXiv 원문에 따르면 연구진은 AI 에이전트가 정형 검증 소프트웨어를 저장소 단위로 만들 수 있는지를 평가하는 새 벤치마크 ‘Vero’를 공개했다. 대상 언어는 정리 증명 보조기 Lean 4다.

Vero는 작은 함수 하나의 정답 여부를 따지는 기존 평가와 달리, 여러 모듈로 이뤄진 프로젝트에서 인터페이스와 명세를 맞추는 과정을 측정한다. 연구진은 실제 저장소를 바탕으로 선별한 43개 인스턴스에 743개 API와 2,705개 명세를 담았다고 밝혔다.

평가는 두 갈래다. ‘code-and-proof’ 모드에서는 에이전트가 API 구현과 각 명세의 증명을 모두 작성해야 한다. ‘proof’ 모드에서는 참조 구현이 주어진 상태에서 명세 증명에 집중한다. 두 모드를 나눠 모델이 코드를 만드는 문제와 이미 주어진 코드의 정확성을 증명하는 문제를 구분하려는 설계다.

채점은 에이전트가 수정한 전체 작업 공간을 그대로 신뢰하지 않는다. 프로젝트를 깨끗한 상태에서 다시 구성한 뒤 제출한 코드 조각만 끼워 넣어 빌드하고, 허용된 공리와 증명 방식을 검사한다. 연구진은 미완성 증명 표식이나 임의 공리 주입, 실행 기반 우회 등을 걸러내도록 구성했다고 설명했다.

정형 검증은 보안·암호·시스템 소프트웨어처럼 오류 비용이 큰 영역에서 오래 활용돼 왔지만, 코드와 증명을 함께 작성해야 하는 부담 때문에 적용 범위가 제한적이었다. Vero는 AI 코딩 에이전트가 그 부담을 어느 정도 줄일 수 있는지, 단순 코드 생성률이 아닌 저장소 전체의 검증 완료 여부로 확인하려는 시도다.

다만 이번 자료는 사전 공개 논문과 연구진 프로젝트 페이지를 기반으로 한다. 모델별 결과와 리더보드는 실행 설정과 후속 업데이트에 따라 달라질 수 있어, 실제 도입 판단에는 개별 과제에서의 재현 검증이 필요하다.

출처: Vero 연구진 공식 프로젝트 https://vero.verina.io/
출처: arXiv 연구자 원문 https://arxiv.org/abs/2608.13522