Verus-SpecGym: 명세 자동 형식화를 평가하기 위한 에이전틱 환경
Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
TL;DR AI
2분핵심 요약
연구진은 Codeforces 스타일 문제를 Verus 명세로 옮길 수 있는지 평가하기 위해 Verus-SpecGym과 Verus-SpecBench를 공개했다.
이들은 581개 태스크 벤치마크와 인터랙티브 명세 작성 환경을 만들고, 실행 가능한 명세와 적대적 엣지 케이스로 여러 모델을 평가했다.
Gemini 3.1 Pro가 가장 좋은 성능을 보였지만, 가정 누락과 허용/거부 사례를 잘못 판단하는 등 반복적인 실패가 나타났다.
또한 LLM-as-a-judge는 많은 명세 오류를 놓쳐 자동 평가는 여전히 사각지대가 있음을 보여줬다.
결론적으로 LLM은 명세 자동형식화에 유망하지만, 신뢰할 수 있는 형식 검증에는 아직 더 강한 안전장치가 필요하다.
