버클리 Vero 벤치마크, 43개 중 27개만 완전 해결

버클리 RDI 연구소가 Vero라는 새 벤치마크를 공개했다. 이 벤치마크는 AI 에이전트에게 코드베이스 전체 규모에서 두 가지를 동시에 요구한다. 필요한 API를 전부 구현하는 것, 그리고 주어진 각 사양이 성립함을 증명하는 것이다. 이 과정에서 코드와 증명, 빌드는 시종일관 일치해야 한다. 지금까지의 형식 검증 벤치마크는 대체로 단일 정리나 단일 함수 수준에 머물러 있었고, 저장소 수준 벤치마크는 이번이 처음이다.

시험 대상은 Python, Dafny, Verus, Coq의 기존 코드에서 이식된 43개의 다중 모듈 Lean 4 프로젝트로, 총 743개의 API와 2,705개의 형식 사양을 포괄한다. 평가는 두 가지 모드로 진행된다. 증명 전용 모드에서는 참조 구현이 주어지고 에이전트는 증명만 담당하며, 구현과 증명 모드에서는 에이전트가 직접 구현을 작성한 뒤 그것이 사양을 만족함을 증명해야 한다.

점수표

90분의 시간 예산 내에서 완전히 해결한 인스턴스 수(만점 43):

1행과 3행 사이의 격차는 눈여겨볼 만하다. 동일한 GPT-5.5, 동일한 Codex를 쓰면서 추론 설정만 medium에서 xhigh로 올렸을 뿐인데, 구현과 증명 모드 점수는 2에서 27로 뛰어올랐다. 이런 유형의 과제에서는 추론 예산을 늘리는 것의 한계 효용이 아직 전혀 포화되지 않았다는 뜻이다.

어려운 것은 개별 증명이 아니다

1위 행에는 또 다른 숫자 쌍이 숨어 있다. GPT-5.5(xhigh)는 구현과 증명 모드에서 개별 사양의 87.3%를, 증명 전용 모드에서는 85.8%를 통과한다. 하지만 기준을 “인스턴스 전체를 완전히 끝냈는가”로 바꾸면 그 수치는 27/43, 25/43으로 떨어진다. 연구진의 결론은 분명하다. 개별 사양을 증명하는 것 자체는 더 이상 어려운 지점이 아니며, 증명 저장소 전체의 일관성을 유지하는 것이 진짜 난관이라는 것이다.

이 두 수치 사이의 간극에는 실질적인 엔지니어링적 함의가 있다. 개별 사양 기준 87%의 통과율은, 수십 개의 사양을 가진 프로젝트에서는 거의 모든 프로젝트가 몇 개의 사양에서 막힌 채 남는다는 뜻이다. 그리고 형식 검증은 전부 아니면 전무의 세계다. 단 하나의 사양이라도 증명되지 않으면 저장소 전체가 빌드되지 않으며, 앞서 올바르게 증명한 부분에도 부분 점수는 전혀 주어지지 않는다. 이는 단위 테스트를 87% 통과한 프로젝트도 출시될 수 있는 것과는 완전히 다른 이야기다.

또 하나 주목할 세부 사항은 증명 코드의 구성이다. 완전히 해결된 실행 결과들을 보면, 보조 정리(lemma)가 증명 코드의 중앙값 기준 73.6%를 차지했다. 즉 에이전트가 작성한 것의 4분의 3은 주 증명을 떠받치기 위해 임시로 세운 발판에 불과하다는 뜻이다. 이 비율은 현재의 모델들이 깔끔한 증명 구조를 찾아내기보다는, 보조 정리를 쌓아 밀어붙이는 너비 우선 방식을 택하고 있음을 시사한다.

알고리즘을 직접 고르면, 도움 5번에 방해 17번

구현과 증명 모드는 에이전트에게 한 가지 자유도를 더 준다. 구현을 직접 작성할 수 있다는 것은 증명하기 더 쉬운 알고리즘을 스스로 고를 수 있다는 뜻이기도 하다. 연구진은 짝지어진 비교를 통해 이 자유도의 순효과를 측정했다. 그 결과 알고리즘을 바꿔서 성공한 경우가 5건, 오히려 실패의 원인이 된 경우가 17건이었다.

이 5 대 17이라는 숫자는 많은 것을 말해준다. 이론적으로는 직접 구현을 고를 수 있는 자유가 손해가 될 이유는 없다. 최악의 경우 참조 구현을 그대로 베끼면 그만이기 때문이다. 그러나 실제로는 모델이 스스로 “영리하다”고 판단한 구현을 자주 선택했고, 그것이 결국 훨씬 증명하기 어려운 것으로 드러나 90분 내내 거기서 빠져나오지 못하는 경우가 많았다. 코드를 작성하는 능력과 어떤 코드가 증명하기 쉬운지 알아보는 능력은 서로 다른 능력이며, 현재의 에이전트는 그중 앞의 것만 갖추고 있다.

순위표에는 한 가지가 더 남아 있다. 43개 인스턴스 중 10개는 모든 구성, 두 모드 전부에서 단 한 번도 해결되지 않았다. 이 인스턴스들은 현재 방법론의 확고한 한계선을 보여주며, 다음 연구가 가장 주목해야 할 지점이기도 하다.

AI 코딩 도구를 만드는 사람들에게 Vero의 가치는 순위 자체가 아니라, 그동안 경험적으로만 판단할 수 있었던 “저장소 수준의 일관성”을 측정 가능한 지표로 바꿔냈다는 데 있다. SWE-bench 같은 벤치마크가 측정하는 것은 버그 하나를 제대로 고칠 수 있는가이지만, Vero가 측정하는 것은 하나의 엔지니어링 프로젝트가 지닌 제약 전체를 견뎌낼 수 있는가다. 두 가지는 애초에 난이도의 급이 다르다.

참고 출처: 버클리 RDI 연구소 공식 블로그, CocoLoop; 벤치마크 규모, 두 모드의 완전 해결 수, 사양별 통과율, 보조 정리 비율, 짝비교 통계는 모두 공개 보고서 기준으로 대조 확인함.