[논문] TLA‑Prover: 선호 최적화 저랭크 적응을 통한 검증 가능한 TLA+ 명세 합성
개요
TLA+는 분산 시스템과 안전이 중요한 프로토콜을 검증하기 위한 형식 사양 언어입니다. 대형 언어 모델(LLM)은 종종 의미적 이유로 TLC 모델 체커를 통과하지 못하는 TLA+ 사양을 생성합니다. 25개의 LLM을 대상으로 한 실험에서 가장 좋은 공개 베이스라인은 구문 파싱 26.6%, 의미 모델 체크 8.6%였습니다. 우리는 TLA+ 사양 생성을 위해 200억 파라미터 규모의 모델인 TLA-Prover를 제시합니다. 학습은 검증된 예시를 이용한 지도 미세조정(SFT)과 복구 기반 그룹 상대 정책 최적화(GRPO)를 결합합니다. GRPO 단계에서는 모델이 스스로 거부된 사양을 수정하도록 학습합니다. 또한 동일한 SFT 체크포인트에서 직접 선호 최적화(DPO) 변형을 훈련시켜 비교 실험(ablation)으로 사용합니다. 보상 신호는 학습된 보상 모델 없이 TLC가 직접 제공합니다. 출력은 네 단계로 평가됩니다: 브론즈(구문 파싱 성공), 실버(경고 없음), 골드(TLC 통과), 다이아몬드. 다이아몬드 등급에 도달하려면 모델의 정합성 속성이 작은 방식으로 자동 수정되어야 하며, 이때 TLC가 위반을 감지해야 합니다. 만약 TLC가 여전히 통과한다면 해당 속성은 언제나 참이었으며 의미가 없으므로 다이아몬드 등급을 받지 못합니다. TLA-Prover는 보류된 30문제 벤치마크에서 골드와 다이아몬드 모두 9/30(즉, pass@1 = 30%)을 달성했습니다. 이는 약 3.5배 높은 8.6% 미조정 베이스라인 대비 향상된 수치입니다. DPO 변형은 다이아몬드 등급에서 20%를 기록했습니다. 골드와 다이아몬드 등급은 모든 체크포인트에서 일치하며, 이는 사소한 속성 실패 모드를 방지합니다.
주요 기여
이 논문은 다음 분야의 연구를 다룹니다:
- cs.SE
- cs.AI
- cs.LG
- cs.LO
방법론
자세한 방법론은 전체 논문을 참고하십시오.
실용적 함의
본 연구는 cs.SE 분야의 발전에 기여합니다.
저자
- Eric Spencer
- Arslan Bisharat
- Brian Ortiz
- Khushboo Bhadauria
- TaiNing Wang
- George K. Thiruvathukal
- Konstantin Laufer
- Mohammed Abuhamad
논문 정보
- arXiv ID: 2606.06133v1
- 분류: cs.SE, cs.AI, cs.LG, cs.LO
- 발표일: 2026년 6월 4일
- PDF: PDF 다운로드