본 논문은 대규모 언어 모델(LLM)이 생성한 코드의 정확성을 보장하는 것이 어렵다는 점을 지적하며, 코드, 명세, 그리고 코드-명세 정합성 증명을 함께 생성하는 검증 가능한 코드 생성이 이 문제를 해결할 수 있는 유망한 방법이라고 제시합니다. 현존하는 벤치마크들이 종단간 검증 가능한 코드 생성을 제대로 지원하지 못하는 한계를 극복하고자, Lean 언어를 사용하는 189개의 수동으로 엄선된 코딩 과제로 구성된 고품질 벤치마크 Verina를 소개합니다. Verina는 상세한 문제 설명, 참조 구현, 공식 명세, 그리고 광범위한 테스트 세트를 포함합니다. 최첨단 LLM을 이용한 광범위한 평가를 통해, 특히 증명 생성에서 검증 가능한 코드 생성에 상당한 어려움이 있음을 밝히고, 검증 영역에서 LLM 기반 정리 증명기를 개선할 필요성을 강조합니다. 최고 성능 모델인 OpenAI o4-mini조차도 코드 정확도 61.4%, 정확하고 완전한 명세 51.0%, 성공적인 증명 3.6%의 결과를 보였습니다 (과제당 한 번 시도). Verina는 엄격하고 종합적인 벤치마크를 제공하여 검증 가능한 코드 생성 분야의 발전을 촉진할 것으로 기대하며, 데이터셋과 평가 코드를 공개합니다.
