신호 Vero: AI 에이전트가 형식검증된 소프트웨어 저장소를 만들 수 있는가?

요약

AI 에이전트가 프로그래밍에 점점 더 많이 활용되고 있지만, 이렇게 생성된 코드가 실제로 정확한지에 대해서는 아무런 보장이 없다. 검증된 코드 생성, 즉 에이전트가 구현체와 함께 그 명세에 대한 기계검증 가능한 증명을 함께 만들어내는 방식은 검증되지 않은 생성보다 신뢰할 수 있는 AI 소프트웨어로 가는 더 견고한 경로로 제시된다. 이 논문은 기존 관련 벤치마크들이 개별 함수 단위에 초점을 맞추거나 코드베이스의 좁은 일부만 평가할 뿐, 전체 규모의 형식검증된 소프트웨어 저장소는 다루지 않는다고 지적한다. 이런 공백을 메우기 위해 Vero가 도입되며, AI 에이전트가 전체 형식검증 저장소를 실제로 구축하고 유지할 수 있는지를 시험하는 데 목적이 있다. 결과적으로 Vero는 검증된 코드 생성의 범위를 개별 함수 단위에서 저장소 규모의 실제 소프트웨어 공학으로 확장한다.