Papers·2개월 전
CMU, LLM 에이전트의 형식 명세 자동 생성 벤치마크 — Gemini 3.1 Pro 77.8% 해결
CMU 연구팀이 LLM 코딩 에이전트가 비공식 문제 설명을 Verus 검증기용 형식 명세로 변환하는 능력을 측정하는 벤치마크 Verus-SpecBench(581개 태스크)를 공개했습니다. 핵심은 Codeforces 해킹 케이스를 활용해 명세의 충실성을 평가하는 방식으로, Gemini 3.1 Pro가 77.8%를 해결했으며 다른 최신 모델은 51.1~57.8%, 오픈소스 모델은 21.5~25.5%에 그쳤습니다. 다만 LLM-as-a-judge 평가는 26%의 실패를 놓칠 정도로 취약해, 명세 자동 생성이 아직 깨지기 쉽다는 한계가 드러났습니다.
LLM 코딩 에이전트가 생성한 코드의 정확성을 기계 검증으로 보장하려면, 먼저 사용자 의도를 반영한 형식 명세가 필요합니다. CMU 연구팀은 이 명세 자동 생성 능력을 평가하는 벤치마크를 제시했습니다.
핵심 결론
- 벤치마크 — Verus-SpecBench는 Codeforces 문제 581개를 Verus(Rust 검증기) 명세 작성 태스크로 변환했습니다.
- 최고 성능 — Gemini 3.1 Pro가 77.8% 해결, Claude 4 Sonnet 57.8%, GPT-4.1 51.1%, 오픈소스는 21.5~25.5%.
- 평가 방식 — 공식 테스트와 Codeforces 해킹 케이스(경쟁자가 작성한 엣지 케이스)를 활용해 명세의 충실성을 검증합니다.
방법
- Verus 확장 — exec_spec 메커니즘을 확장해 생성된 명세를 Rust 코드로 실행 가능하게 했습니다.
- 에이전트 환경 — Verus-SpecGym은 모델이 Verus, bash, 파일시스템과 상호작용하며 명세를 개발하는 환경입니다.
- 평가 시 해킹 케이스를 포함해 명세가 잘못된 입력을 허용하거나 올바른 입력을 거부하는 경우를 잡아냅니다.
한계·조건
- 실패 분석 — 모델 생성 명세는 중요한 입력 가정을 생략하거나, 잘못된 출력을 허용하거나, 유효한 출력을 거부하는 경우가 많았습니다.
- LLM 평가 취약 — LLM-as-a-judge 평가는 연구팀의 평가 방식이 잡아낸 실패의 26%를 놓쳤습니다.
- 코드 공개 — GitHub(https://github.com/formal-verif-is-cool/verus-spec-gym)에서 코드, 데이터, 로그를 공개했습니다.
편집자 한 줄
명세 자동 생성이 코드 생성보다 훨씬 까다롭다는 점을 보여주는 흥미로운 결과네요. 해킹 케이스를 평가에 활용한 아이디어가 특히 돋보입니다.
- #formal-verification
- #llm-agents
- #code-generation
- #cmu
Carnegie Mellon University