[논문] LLM이 올바른 TLA+ 사양을 작성할 수 있을까? 자연어‑TLA+ 생성 평가
개요
TLA+는 Amazon과 Microsoft와 같은 기업에서 산업용 검증을 지원해 왔지만, 자연어에서 올바른 TLA+ 사양을 작성하려면 여전히 시간과 전문 지식이 필요합니다. 이는 채택을 제한하는 요인입니다. 대형 언어 모델(LLM)은 가능성을 보여주고 있지만, 기존 연구에서는 자연어로부터 의미적으로 올바른 TLA+ 사양을 생성하는지를 측정한 바가 없습니다. 본 논문은 자연어 기반 LLM을 이용한 TLA+ 사양 합성을 최초로 체계적으로 평가합니다. 우리는 205개의 TLA+ 사양으로 구성된 정제된 데이터셋을 사용해 8개 패밀리의 30개 LLM을 평가했습니다: 4가지 프롬프트 전략을 적용한 25개의 오픈‑웨이트 모델(2,600회 실행)과 몇 샷 프롬프트를 적용한 5개의 독점 모델(130회 실행) 모두 SANY 파서와 TLC 모델 체커로 검증했습니다. LLM은 최대 26.6%의 구문 정확성을 달성했지만 의미 정확도는 8.6%에 불과했으며, 성공 사례는 전적으로 진행형 프롬프트에 국한되었습니다. 결과는 모델 크기가 품질을 예측하지 않음을 보여줍니다. 예를 들어 DeepSeek r1:8b가 70B 버전을 모든 전략에서 앞섰으며, 이는 형식 언어에 대한 추론 정렬의 중요성을 시사합니다. 코드 특화 모델은 주류 언어 학습에서 발생하는 부정적 전이 때문에 일관되게 성능이 낮았습니다. 우리는 다섯 가지 반복적인 환각(halucination) 유형을 식별했으며, 모두 특정 학습 데이터 편향과 연관됩니다. 이러한 결과는 현재 LLM이 전문가의 감독 없이 신뢰할 수 있는 TLA+ 사양을 생성하지 못한다는 점을 시사합니다. 우리는 재현성과 향후 연구를 지원하기 위해 평가 프레임워크, 코드, 데이터셋을 공개합니다.
주요 기여
본 논문은 다음 분야의 연구를 제시합니다.
- cs.AI
- cs.LG
- cs.LO
- cs.SE
방법론
자세한 방법론은 전체 논문을 참고하십시오.
실용적 함의
본 연구는 cs.AI 분야의 발전에 기여합니다.
저자
- Arslan Bisharat
- Brian Ortiz
- Eric Spencer
- Khushboo Bhadauria
- TaiNing Wang
- George K. Thiruvathukal
- Konstantin Laufer
- Mohammed Abuhamad
논문 정보
- arXiv ID: 2606.05792v1
- 분류: cs.AI, cs.LG, cs.LO, cs.SE
- 발행일: 2026년 6월 4일
- PDF: PDF 다운로드