LLM이 정확한 TLA+ 명세(Specification)를 작성할 수 있는가? 자연어-to-TLA+ 생성 평가

TLA+는 Amazon 및 Microsoft와 같은 기업에서 산업적 검증 (Industrial Verification)을 지원해 왔으나, 자연어로부터 정확한 TLA+ 명세 (Specification)를 작성하는 것은 여전히 시간과 전문 지식을 필요로 하며, 이는 도입을 제한하는 요소가 됩니다. LLM (Large Language Models)은 가능성을 보여주고 있지만, 자연어로부터 의미론적으로 정확한 (Semantically Correct) TLA+ 명세를 생성하는지 측정하는 선행 연구는 없었습니다. 본 논문은 자연어로부터 LLM 기반의 TLA+ 명세 합성 (Specification Synthesis)에 대한 최초의 체계적인 평가를 제시합니다. 우리의 연구는 205개의 TLA+ 명세로 구성된 큐레이션된 데이터셋을 통해 8개 계열의 30개 LLM을 평가합니다. 구체적으로 4가지 프롬프팅 전략을 사용한 25개의 오픈 웨이트 (Open-weight) 모델 (2,600회 실행)과 퓨샷 프롬프팅 (Few-shot Prompting) 하의 5개 독점 모델 (Proprietary Models, 130회 실행)을 대상으로 하였으며, 모든 결과는 SANY 파서 (Parser)와 TLC 모델 체커 (Model Checker)를 통해 검증되었습니다. LLM은 최대 26.6%의 구문론적 정확도 (Syntactic Correctness)를 달성했으나, 의미론적 정확도 (Semantic Correctness)는 8.6%에 불과했으며, 성공 사례는 점진적 프롬프팅 (Progressive Prompting)에만 국한되었습니다. 결과에 따르면 모델 크기가 품질을 예측하지 못함을 보여줍니다. 예를 들어, DeepSeek r1:8b는 모든 전략에서 70B 변체보다 우수한 성능을 보였으며, 이는 형식 언어 (Formal Languages)에 대한 추론 정렬 (Reasoning Alignment)의 중요성을 시사합니다. 코드 특화 모델 (Code-specialized Models)은 주류 언어 학습으로부터의 부정적 전이 (Negative Transfer)로 인해 지속적으로 낮은 성능을 보였습니다. 우리는 특정 학습 데이터 편향 (Training Data Biases)에서 기인하는 5가지 반복적인 환각 (Hallucination) 범주를 식별했습니다. 이러한 결과는 현재의 LLM이 전문가의 감독 없이는 신뢰할 수 있는 TLA+ 명세를 생성하지 못함을 시사합니다. 우리는 재현성과 향후 연구를 지원하기 위해 평가 프레임워크, 코드 및 데이터셋을 공개합니다.