KBSpec: 진화하는 도메인 지식 베이스를 활용한 LLM 기반 형식 명세 생성

자동화된 형식 명세 (Formal Specification) 생성은 프로그램 이해 및 형식 검증 (Formal Verification)을 향한 핵심 단계입니다. 최근 코드 생성 분야에서 거대 언어 모델 (LLMs)의 성공에 힘입어, 연구자들은 형식 명세를 생성하기 위해 LLM을 채택하려는 초기 시도들을 해왔습니다. 그러나 실제 환경에서 형식 명세 언어 코퍼스 (Corpora)의 부족으로 인해, LLM이 구문론적으로 정확하고 의미론적으로 검증 가능한 명세를 생성하는 데 실패하는 경우가 빈번합니다. 이러한 격차를 완화하기 위해, 우리는 형식 명세 언어의 이중 소스 지식(dual-source knowledge)으로 LLM을 증강하는 KBSpec을 제안합니다. 이 지식은 공식 문서로부터 얻은 외부 지식과, LLM이 생성한 명세에 대한 검증기 (Verifier) 피드백으로부터 추출된 내부 지식으로 구성됩니다. KBSpec은 LLM의 파라미터 튜닝이나 라벨링된 학습 데이터 없이도, 성공적인 생성 및 수정 궤적 (Trajectories)으로부터 지속적으로 업데이트되는 자기 진화형 지식 베이스 (Self-evolving knowledge base)를 유지합니다. 우리는 세 가지 LLM 백엔드를 사용하여 Java Modeling Language (JML) 명세 생성에 대해 KBSpec을 평가하였으며, 결과에 따르면 KBSpec은 최신 LLM 기반 방식들보다 검증 통과율 (Verification pass rates)을 10-25% 향상시키는 동시에, 가장 많은 수의 높은 완전성 (High-completeness)을 가진 명세를 생성함을 보여주었습니다.