Verus-SpecGym: 명세 자동 형식화 (Specification Autoformalization) 평가를 위한 에이전트 기반 환경

AI 코딩 에이전트 (AI coding agents)가 실제 소프트웨어를 작성하는 데 점점 더 많이 사용되고 있지만, 그 출력물이 정확한지 보장하는 것은 여전히 근본적인 과제로 남아 있습니다. 형식 검증 (Formal verification)은 유망한 경로를 제공합니다. 즉, 에이전트가 코드를 생성할 때 기계가 검증 가능한 증명 (proof)을 함께 생성하여, 해당 코드가 형식 명세 (formal specification)를 충족함을 보장하는 방식입니다. 그러나 형식 명세 자체가 사용자의 의도와 일치한다는 보장은 없습니다. 본 연구에서는 명세 자동 형식화 (specification autoformalization), 즉 LLM 에이전트가 비형식적 (informal) 프로그래밍 문제를 충실한 형식 명세로 번역할 수 있는지 여부를 연구합니다. 우리는 Rust용 검증기인 Verus를 대상으로 Codeforces 문제에서 유도된 581개의 명세 작성 작업 벤치마크인 Verus-SpecBench와, 모델이 Verus, bash, 그리고 파일 시스템 (filesystem)과 상호작용하며 이러한 명세를 개발하는 에이전트 기반 환경인 Verus-SpecGym을 소개합니다. 핵심 과제는 평가 (evaluation)입니다. 전문가가 작성한 참조 명세 (reference specs)는 작성 비용이 많이 들며, LLM 판사 (LLM judges)는 미세한 실수를 놓칠 수 있습니다. 우리는 이를 해결하기 위해 (a) 생성된 명세가 Rust 코드로 실행될 수 있도록 Verus의 exec_spec 메커니즘을 확장하고, (b) 이를 공식 Codeforces 테스트 및 Codeforces의 "hacks"에서 추출된 적대적 사례 (adversarial cases)에 대해 테스트합니다. 여기서 "hacks"란 잘못된 솔루션을 깨뜨리기 위해 경쟁자들이 작성한 엣지 케이스 (edge cases)를 의미합니다. Verus-SpecBench에서 가장 강력한 모델인 Gemini 3.1 Pro는 작업의 77.8%를 해결했으며, 다른 프런티어 모델 (frontier models)들은 51.157.8%를 해결한 반면, 오픈 소스 (OSS) 모델들은 21.525.5%에 그쳤습니다. 실패 모드 (failure modes)에 대한 분석 결과, 모델이 생성한 명세는 중요한 입력 가정 (input assumptions)을 누락하거나, 잘못된 출력을 수용하거나, 유효한 출력을 거부할 수 있음을 보여줍니다. 또한 LLM-as-a-judge 평가 방식이 우리의 평가기가 잡아내는 실패의 26%를 놓친다는 점도 발견했습니다. 전반적으로 우리의 결과는 명세 자동 형식화가 프런티어 에이전트들에게 도달 가능한 범위 내에 있지만, 에이전트가 이미 정확한 코드를 생성할 수 있는 문제에서도 여전히 취약함 (brittle)이 남아 있음을 시사합니다. 코드, 데이터 및 로그는 https://github.com/formal-verif-is-cool/verus-spec-gym 에서 확인할 수 있습니다.