에이전트 기반 분리 논리 명세 합성 (Agentic Separation Logic Specification Synthesis)

명세 합성 (Specification synthesis)은 프로그램 구현과 자연어로부터 형식적 명세 (formal specifications)를 자동으로 추론하는 작업으로, 리팩토링 (refactoring), 트랜스파일링 (transpilation), 최적화 (optimization) 및 검증 (verification)에 있어 중요하지만, 대규모 C++ 저장소 (repositories)에 대해서는 여전히 해결되지 않은 과제로 남아 있습니다. 기존의 LLM 기반 접근 방식들은 이러한 저장소 규모로 동시에 확장하거나, 동적 메모리 (dynamic memory) 및 힙 할당 데이터 구조 (heap-allocated data structures)와 같은 시스템 코드의 특징을 포착할 수 있을 만큼 표현력이 풍부한 명세를 생성하거나, 잘못된 후보를 배제하기 위해 해당 명세들을 체계적으로 검증하는 데 실패하고 있습니다. 본 논문에서는 대규모 C++ 코드베이스 전반에 걸쳐 표현력이 풍부하고 잘 검증된 명세를 합성하기 위한 에이전트 기반 시스템인 Spec-Agent를 제안합니다. Spec-Agent는 명세 언어의 단계인 명제 논리 (propositional logic), 1차 논리 (first-order logic), 명제 분리 논리 (propositional separation logic), 그리고 1차 분리 논리 (first-order separation logic)를 목표로 합니다. 각 함수에 대해 Spec-Agent는 정적 분석 (static analysis)과 런타임 힙 트레이싱 (runtime heap tracing)을 사용하여 적절한 대상 명세 언어를 선택하고, 기존의 기능 테스트를 퍼즈 하네스 (fuzz harnesses)로 일반화하며, 반례 유도 피드백 (counterexample-guided feedback)을 통해 LLM이 생성한 후보를 반복적으로 정제합니다. 우리는 수백만 줄의 코드로 구성된 오픈 소스 C++ 코드베이스에서 Spec-Agent를 평가합니다. Spec-Agent는 대상 함수의 85%에 대해 유효한 명세를 합성하며, 퍼징 (fuzzing) 및 전문가 검증 하에서 오탐 (false positives)이 관찰되지 않았으며, Claude Code Opus 4.6보다 10배 낮은 토큰 비용으로 더 우수한 성능을 보였습니다.