AutoReSpec: A Framework for Generating Specification using Large Language Models

1. 문제 정의 (Problem)

소프트웨어 공학에서 공식 명세 (Formal Specification) 는 프로그램의 정확성을 검증하고, 테스트 생성 및 프로그램 합성을 가능하게 하는 핵심 요소입니다. 그러나 실제 코드베이스에서는 수동으로 작성하는 데 전문성과 시간이 많이 소요되어 공식 명세가 거의 존재하지 않습니다.

최근 대규모 언어 모델 (LLM) 을 활용하여 코드에서 자동으로 명세를 생성하려는 시도가 늘고 있지만, 기존 접근법 (SpecGen, FormalBench 등) 은 다음과 같은 한계를 겪고 있습니다:

• 검증 실패: 생성된 명세가 구문 오류, 논리적 부정확성, 또는 불완전한 추론으로 인해 검증 도구 (Verifier) 를 통과하지 못함.
• 복잡한 제어 흐름 대응 부족: 루프나 분기 로직이 포함된 프로그램에서 특히 성능이 떨어짐.
• 고정된 전략: 정적 프롬프트 (Static Prompts) 에만 의존하며, 실패 시 복구 메커니즘이 없거나 프로그램 구조에 맞춰 동적으로 적응하지 못함.
• 단일 모델 의존성: 모든 프로그램 유형에 대해 동일한 모델을 사용하여 비효율적이거나 정확도가 낮음.

2. 방법론 (Methodology)

저자들은 이러한 문제를 해결하기 위해 AutoReSpec이라는 협업형 프레임워크를 제안합니다. 이는 오픈 소스 및 상용 (Closed-source) LLM 을 결합하여 검증 가능한 명세를 생성하는 2 단계 협업 프로세스를 기반으로 합니다.

핵심 구성 요소 및 워크플로우

1. 동적 LLM 추천 (Dynamic LLM Recommender):

   • 입력된 Java 프로그램의 구문 분석 트리 (AST) 를 분석하여 프로그램 유형 (순차, 분기, 단일 경로 루프, 다중 경로 루프, 중첩 루프 등) 을 분류합니다.
   • 각 프로그램 유형에 대해 검증 성공률, 효율성 (호출 횟수, 시간) 등을 기반으로 최적의 주요 (Primary) LLM 과 대응 (Fallback/Collaborative) LLM 쌍을 동적으로 선택합니다.
   • 예: 간단한 프로그램에는 경량 모델을, 복잡한 루프가 포함된 프로그램에는 강력한 모델을 선택하여 비용과 성능을 균형 있게 조절합니다.

2. 반복적 정제 (Iterative Refinement):

   • 1 단계 (주요 LLM): 선택된 주요 LLM 이 Few-shot 프롬프트를 기반으로 초기 명세를 생성합니다. 생성된 명세는 OpenJML 및 Z3 솔버를 통해 검증됩니다.
   • 피드백 루프: 검증이 실패할 경우, 검증기 (Validator) 가 반환한 오류 메시지를 분석하여 프롬프트를 정제하고 LLM 에게 재요청합니다. 이 과정은 최대 반복 횟수 (Budget) 까지 계속됩니다.

3. 협업 복구 (Collaborative Recovery):

   • 주요 LLM 이 예산 내에서 유효한 명세를 생성하지 못하면, 협업 LLM이 호출됩니다.
   • 협업 LLM 은 이전 대화 기록 전체가 아닌, 최종 실패한 명세와 검증 오류 정보만을 컨텍스트로 받아 집중적으로 수정을 시도합니다. 이는 문맥 드리프트 (Context Drift) 를 방지하고 효율성을 높입니다.

4. 프롬프트 관리:

   • 긴 컨텍스트로 인한 비용 증가와 할루시네이션을 방지하기 위해 자동 프롬프트 잘라내기 (Truncation) 와 메모리 관리 전략을 적용합니다.

3. 주요 기여 (Key Contributions)

• AutoReSpec 프레임워크 제안: 프로그램 구조에 기반한 동적 모델 선택과 검증기 안내 대화형 정제를 통해 검증 가능한 명세를 생성하는 새로운 협업 아키텍처를 제시했습니다.
• 협업 프롬프트 엔지니어링: Few-shot 예시, 검증기 피드백, 자동 프롬프트 절단을 결합하여 긴 컨텍스트 상호작용과 표적 오류 해결을 지원합니다.
• AutoReSpecBench 벤치마크 구축: SpecGenBench, SV-COMP, 그리고 실제 GitHub 이슈 (OpenJML) 에서 수집한 72 개의 Java 프로그램을 포함한 새로운 벤치마크와 공개 리더보드를 구축했습니다.
• 오픈 소스 도구 공개: 전체 프레임워크, 데이터셋, VS Code 확장 프로그램을 오픈 소스로 공개하여 재현 가능한 연구를 지원합니다.

4. 실험 결과 (Results)

저자들은 72 개의 Java 프로그램 (실제 및 합성) 으로 AutoReSpec 을 평가하여 기존 도구 (SpecGen, FormalBench) 와 비교했습니다.

• 성공률 및 완전성:
  • 성공 확률 (Success Probability): AutoReSpec 은 **58.2%**를 기록하여 SpecGen(51.4%) 과 FormalBench(24.3%) 를 능가했습니다.
  • 완전성 (Completeness): **69.2%**의 점수를 기록하여 기존 방법들보다 높은 결함 탐지율을 보였습니다.
  • 통과 횟수 (Passes): 72 개 프로그램 중 67 개에서 검증에 성공했습니다 (SpecGen 은 58 개, FormalBench 는 13 개).
• 효율성:
  • 평균 평가 시간을 기존 방법 대비 26.89% 단축했습니다.
  • API 비용 측면에서도 상용 모델을 필요할 때만 호출하는 전략으로 인해 프로그램당 평균 비용 ($0.13) 이 SpecGen($0.16) 보다 낮았습니다.
• 오류 해결 능력:
  • 특히 '사후 조건 (Postcondition)' 및 '루프 불변식 (Loop Invariant)' 관련 오류 해결에서 기존 도구 대비 훨씬 낮은 '고민 비율 (Struggle Ratio)'을 보였습니다 (예: Postcondition 오류 27.06% → 6.55% 감소).

5. 의의 및 결론 (Significance)

AutoReSpec 은 LLM 기반 공식 명세 생성 분야에서 다음과 같은 중요한 진전을 이뤘습니다:

1. 적응형 아키텍처: 모든 프로그램에 동일한 모델을 적용하는 기존 방식의 한계를 극복하고, 프로그램의 복잡도에 따라 최적의 모델 조합을 동적으로 선택함으로써 **확장성 (Scalability)**과 신뢰성을 동시에 확보했습니다.
2. 강건한 복구 메커니즘: 단일 모델의 실패를 협업 모델을 통해 복구하는 2 단계 설계는 검증 실패를 효과적으로 줄여주며, 실제 복잡한 제어 흐름을 가진 프로그램에서도 높은 정확도를 보장합니다.
3. 실용성: 검증 시간 단축과 비용 절감을 실현하여, 실제 소프트웨어 공학 환경에서 자동 명세 생성 도구의 실용적인 도입 가능성을 높였습니다.

결론적으로, AutoReSpec 은 LLM 의 추론 능력을 검증 도구와 긴밀하게 통합함으로써, 수동 개입 없이도 고품질의 검증 가능한 소프트웨어 명세를 생성할 수 있는 효율적이고 신뢰할 수 있는 솔루션을 제시합니다.