VeriFast를 위한 LLM 생성 명세(Specifications)에 관한 실증적 연구

정적 검증(Static verification) 도구는 산업 규모의 소프트웨어를 보장할 수 있지만, 명세(specifications)를 작성하는 데 상당한 인적 노동이 필요합니다. 이는 분리 논리(Separation Logic, SL) 기반의 정적 검증기(SL verifiers)의 경우 특히 그러한데, 이들은 힙(heap)을 조작하는 프로그램을 검증하는 데 탁월하지만 힙 구조를 추론하기 위해 많은 복잡한 보조 명세(auxiliary specifications)를 필요로 합니다. 최근 연구들은 대규모 언어 모델(LLMs)을 코드, 테스트, 증명(proofs) 생성에 적용하고 있으며 여기에는 검증기를 위한 명세 생성도 포함되지만, 대부분 비-SL 검증기(non-SL verifiers)를 대상으로 하고 있습니다. 이러한 격차를 해소하기 위해, 본 논문은 SL 검증기인 VeriFast를 사용하여 303개의 C 함수를 검증하기 위한 명세를 생성하도록 LLM에 프롬프트를 제공했을 때의 성능을 철저히 평가합니다. 우리는 두 단계에 걸쳐 8가지 프롬프팅 접근 방식, 10개의 LLM, 그리고 3가지 입력 유형을 탐색했습니다. 정량적 및 정성적 분석을 사용하여 LLM이 생성한 코드와 명세의 기능적 동작(functional behavior), 검증 가능성(verifiability) 및 오류를 평가했습니다. 결과에 따르면 LLM은 소스 코드와 명세 모두에서 기능적 동작을 보존하지만(둘 다 91% 이상), 검증 성공률은 완만한 수준(31.4%)을 기록했습니다. Gemini 2.5 Pro를 사용하고 공식 계약(formal contracts)을 제공하는 것이 우리의 설정에서 더 높은 성공률을 이끌어냈습니다. 또한, 대부분의 오류(94%)는 VeriFast와 같은 SL 검증기의 도메인 특화 지식(domain-specific knowledge)에 대한 LLM의 실수에서 비롯되었습니다. 이러한 발견은 SL 검증기를 위한 LLM 생성 명세를 최적화하는 데 지침을 제공합니다.