기술 요약: KBSpec

문제 정의

자동화된 정형 명세(formal specification) 생성은 프로그램 이해 및 정형 검증을 위한 핵심적인 단계이다. 대규모 언어 모델(LLM)이 코드 생성 분야에서 유망한 성능을 보여주었으나, 정형 명세(예: JML, Java Modeling Language) 생성에 적용할 때는 중대한 장애물에 직면한다. 바로 학습 데이터 내의 정형 명세 코퍼스(corpus)가 매우 부족하다는 점이다. 이러한 "저자원(low-resource)" 상태는 빈번한 구문 오류와 의미론적 실패(예: 경계값 체크 누락, 잘못된 불변량)를 초사한다.

외부 지식(예: 공식 문서)을 LLM에 증강하려는 기존의 시도들은 정형 명세 리소스가 불완전하거나, 다양한 검증 패턴을 포괄하지 못하거나, 검증기가 완전히 지원하지 않는 실험적 기능을 포함하고 있는 경우가 많기 때문에 충분하지 않다. 또한, 정의된 정적 외부 지식에만 의존하는 것은 성공적인 검증을 위해 필요한 미묘하고 검증기 특화된 제약 조건을 포착하는 데 한계가 있다.

방법론: KBSpec

저자들은 KBSpec(Knowledge Base-Augmented Specification Generation)을 제안한다. 이는 LLM을 이중 소스, 자기 진화형 지식 베이스로 증강하는 프레임워크이다. 이 시스템은 LLM 파라미터를 수정하거나 레이블이 지정된 정답(ground-truth) 데이터를 요구하지 않고, 대신 정형 검증기(formal verifier)로부터의 피드백에 의존하여 작동한다.

KBSpec 파이프라인은 세 가지 주요 단계로 구성된다:

1. 지식 베이스 초기화

시스템은 외부 지식(예: OpenJML 튜토리얼, 예제, 연습 문제 등 공식 문서에서 추출)과 인간이 작성한 수정 가이드라인을 사용하여 정형 명세 지식 베이스($M$)를 초기화한다. 각 지식 항목은 검색을 용이하게 하기 위해 LLM에 의해 생성된 원본 내용($c_i$), 요약($s_i$), 키워드($k_i$)의 트리플렛(triplet) 구조로 구성된다.

2. 지식 베이스 진화 (학습 단계)

이것이 핵심적인 혁신이다. 지식 베이스는 Java 프로그램 "학습" 코퍼스를 대상으로 실행되는 생성 및 수정 파이프라인을 통해 동적으로 업데이트된다.

• 생성(Generation): 주어진 프로그램에 대해 LLM은 베이스라인 명세를 생성한다. 그 후, 관련 지식 항목을 검색하고 검색된 지식의 다양한 조합을 바탕으로 새로운 명세를 생성한다.
• 검증 및 점수 산정(Verification & Scoring): 생성된 명세는 정형 검증기(OpenJML)를 통해 검증된다. 검색된 각 지식 항목에 대해, 해당 항목이 이전에 실패했던 검증을 통과하는 데 도움을 주었는지, 혹은 통과했던 검증을 실패하게 만들었는지에 따라 **도움 정도 점수(helpfulness score)**를 부여한다.
• 반복 수정(Iterative Repair): 명세가 실패할 경우, 시스템은 최대 3회까지 수정 단계를 수행한다. LLM은 원본 명세, 검증기의 에러 메시지, 그리고 검색된 지식을 사용하여 수정된 버전을 생성한다. 검색된 항목의 도움 정도는 에러 감소 또는 검증 성공 여부에 따라 업데이트된다.
• 업데이트 및 필터링(Update & Filtering): 각 에포크(epoch)가 끝난 후 지식 베이스가 업데이트된다. 도움 정도 점수가 낮은 항목은 필터링되어 제거되며, 새로운 성공적인 궤적(생성 또는 수정 과정)이 추가된다. 중복성은 유사도 검사를 통해 관리된다.

3. 지식 증강 추론 (Knowledge-Augmented Inference)

평가 단계에서 KBSpec은 진화된 지식 베이스를 사용하여 명세 생성을 보조한다. 무작위로 지식 그룹을 샘플링하는 학습 단계와 달리, 추론 단계에서는 **LLM 기반 선택기(selector)**를 사용한다. LLM은 검색된 집합에서 가장 관련성이 높은 지식 항목(최대 3개)을 자율적으로 선택하여 명세 생성 및 후속 수정을 가이드한다.

주요 기여

1. KBSpec 프레임워크: 검증기 피드백에 의해 구동되는 자기 진화형 지식 베이스를 통합한, 파라미터 변경이 필요 없는 새로운 정형 명세 생성 접근 방식이다.
2. 이중 소스 지식: 외부 문서(초기 언어 이해용)와 내부 지식(생성/수정 궤적에 대한 검증기 피드백에서 추출됨)을 결합하는 것이 LLM의 한계를 극복하는 데 필수적임을 확인하고 입증하였다.
3. 실증적 검증: FormalBench 벤치마크(JML 명세 생성)에 대한 종합적인 평가를 통해, KBSpec이 SpecGen 및 다양한 프롬프팅 전략(Few-shot, Least-to-Most, Self-repair)을 포함한 최신 SOTA(state-of-the-art) 베이스라인들을 유의미하게 능가함을 입증하였다.

결과

실험은 GPT-5.2, GPT-5-mini, DeepSeek-v3.2의 세 가지 LLM 백엔드를 사용하여 수행되었다.

• 통과율 개선: KBSpec은 최신 LLM 기반 방식(예: SpecGen)보다 검증 통과율을 10~25% 향상시켰다. GPT-5.2의 경우, 통과율이 43.35%(SpecGen)에서 **58.94%**로 증가했다.
• 실패 감소: 본 프레임워크는 실패율을 실질적으로 감소시켰다(예: GPT-5.2의 실패율을 20.6%로 감소시킴).
• 완전성(Completeness): 평균 완전성 점수는 다소 변동이 있었으나, KBSpec은 가장 많은 수의 고완전성 명세(완전성 $\ge$ 0.5)를 생성했다. 상호 검증된 프로그램들에 대한 분석 결과, KBSpec은 SpecGen과 비교하여 완전성을 유지하거나 개선했음을 보여주었으며, 이는 통과율의 이득이 단순히 지나치게 약한 계약(contract)을 생성함으로써 얻어진 것이 아님을 나타낸다.
• 절제 연구(Ablation Study): 연구 결과, 지식 베이스 진화 메커니즘(내부 지식)이 가장 결정적인 요소였으며, 초기 외부 문서보다 성능에 더 크게 기여했음을 확인했다. 반복 수정 또한 성공의 주요 동인으로 식별되었다.

의의 및 주장

본 논문은 KBSpec이 검증기 피드백을 통해 스스로의 성공과 실패로부터 배우는 자기 개선 루프를 생성함으로써 정형 명세 언어의 "저자원" 특성을 해결한다고 주장한다.

• 모델 불가지론(Model Agnostic): 이 접근 방식은 경량이며 파인튜닝 없이 모든 LLM에 적용 가능하다.
• 일반화 가능성: JML에 대해 평가되었으나, 저자들은 이 설계가 언어 불가지론적이며 자동화된 검증기가 존재하는 모든 명세 언어에 적응될 수 있다고 주장한다.
• 실용적 공학: 학습된 지식에 대한 분석은 시스템이 단순히 검증을 통과하기 위해 명세를 약화시키는 것이 아니라, 실용적인 수정 전략(예: 산술 오버플로 처리, 지원되지 않는 구문 제거)을 효과적으로 학습함을 보여준다.

저자들은 문서 기반 지식과 검증기에 근거한 메모리 진화를 통합하는 것이 LLM이 구문적으로 정확하고 의미론적으로 검증 가능한 정형 명세를 생성하는 능력을 실질적으로 향상시킨다고 결론짓는다.