본 논문은 소프트웨어 정확성을 보장하기 위한 공식 명세 작성의 어려움을 해결하기 위해, 대규모 언어 모델(LLM) 대신 소규모 미세 조정 언어 모델을 사용하는 방법을 제시합니다. 70억 매개변수의 소규모 코드 모델을 사용하여 실제 Java 버그(Defects4J)를 기반으로 사후 조건 생성을 수행하고, GPT-4o 등 대규모 모델과 비교 평가했습니다. 실험 결과, 소규모 모델이 구문 및 의미 정확성, 버그 식별 능력 면에서 대규모 모델과 동등하거나 우수한 성능을 보임을 확인하여, 소규모 모델의 효율적인 미세 조정을 통한 자동 명세 생성의 실현 가능성을 제시합니다. 본 연구는 실제 저장소 의존성을 처리하고 사전 상태 정보를 유지하여 표현력 있고 정확한 명세를 생성하는 데 중점을 둡니다.
