claimcheck: 명세 충실도 측정 및 개선

형식 검증(Formal verification)은 프로그램이 명세를 만족함을 증명하지만, 그 명세가 작성자가 의도한 바를 포착했는지에 대해서는 아무것도 말해주지 않습니다. LLM이 코드와 명세를 모두 작성함에 따라, 작성자의 자연어 요구사항과 명세 사이의 간극이 실질적인 위험 요소가 됩니다. 요청된 것보다 좁은 속성(property)에 대한 기계 검증 증명은 가치가 없지만 모든 검사를 통과합니다. 이 간극을 메우는 것이 바로 명세 형식화 문제(spec formalization problem)를 해결하는 것입니다: 자연어 요구사항이 주어졌을 때, 그 의미와 일치하는 형식적 아티팩트를 생성하는 것입니다. 이 간극을 측정하기 위해, 우리는 Dafny 계약 및 Lean 4, Isabelle 및 Rocq 정리 진술의 네 가지 형식 언어를 포괄하는 종단 간(end-to-end) 명세 형식화 벤치마크를 구축했습니다. 그 3,234개 행 각각은 자연어 요구사항과 형식적 아티팩트, 그리고 실행, 증명 또는 해당 벤치마크에서 가져온 레이블을 쌍으로 연결합니다. 세 분의 행은 원래 아티팩트를 의미를 보존하는 방식으로 재작성한 것으로, 충실도 레이블(faithful label)을 유지하므로 심사관이 어떤 행이 수정되었는지 감지하여 점수를 매길 수 없습니다. 우리는 부정확한 형식화를 탐지하는 도구인 claimcheck를 소개합니다: 이 형식적 아티팩트는 요구사항을 본 적 없는 모델에 의해 일반 영어로 번역되고, 별도의 모델인 심사관(judge)이 비형식화된 내용과 요구사항이 동일한 보장(guarantee)을 표현하는지 여부를 결정합니다. 네 가지 언어 모두에서, 이 도구는 요구사항과 아티팩트를 보여주는 단일 호출 대비 8.2점에서 9.8점의 거시적 재현율(macro recall)을 얻었으며, 동일한 의미 보존 재작성 목록을 전달하는 경우 4.2점에서 6.0점을 얻었습니다. 심사관에게 아티팩트까지 보여주는 것은 1.4점에서 4.5점의 비용이 발생합니다. 또한 아티팩트를 보는 네 명의 심사관에 걸쳐, 심사관이 더 강력해질수록 이 이득은 줄어들어 가장 강력한 단일 호출 대비 한 점 범위 내로 수렴했습니다.