TLA-Prover: 선호도 최적화 저차원 적응 (LoRA)을 통한 검증 가능한 TLA+ 명세 합성

TLA+는 분산 시스템 (Distributed Systems) 및 안전 필수 프로토콜 (Safety-critical Protocols)을 검증하기 위한 형식 명세 언어 (Formal Specification Language)입니다. 대규모 언어 모델 (LLMs)은 의미론적 (Semantic) 이유로 TLC 모델 체커 (Model Checker)를 통과하지 못하는 TLA+ 명세를 빈번하게 생성합니다. 25개의 LLM을 대상으로 조사한 결과, 가장 우수한 공개 베이스라인은 구문 분석 (Syntactic Parse) 26.6%, 의미론적 모델 체킹 (Semantic Model-check) 8.6%였습니다. 본 논문에서는 TLA+ 명세 합성을 위한 200억 파라미터 규모의 모델인 TLA-Prover를 제시합니다. 학습은 검증된 예시를 통한 지도 미세 조정 (Supervised Fine-tuning, SFT)과 수정 기반 그룹 상대 정책 최적화 (Group-Relative Policy Optimization, GRPO)를 결합하여 진행됩니다. GRPO 단계에서 모델은 거부된 자신의 명세를 스스로 수정하는 법을 배웁니다. 또한, 절제 연구 (Ablation)로서 동일한 SFT 체크포인트로부터 직접 선호도 최적화 (Direct Preference Optimization, DPO) 변형 모델을 학습시켰습니다. 별도의 학습된 보상 모델 (Reward Model) 없이 TLC가 직접 보상 신호 (Reward Signal)를 제공합니다. 각 출력물은 네 단계로 등급이 매겨집니다: Bronze (구문 분석 성공), Silver (경고 없음), Gold (TLC 통과), 그리고 Diamond입니다. Diamond 등급에 도달하기 위해, 모델의 정당성 속성 (Correctness Property)이 미세하게 자동으로 변경되며, 이때 TLC는 반드시 위반 사항을 감지해야 합니다. 만약 TLC가 여전히 통과한다면, 해당 속성은 항상 참 (Always-true)이었으며 아무런 기여를 하지 못한 것이므로, 해당 출력은 Diamond 등급에서 탈락합니다. TLA-Prover는 별도의 30개 문제 벤치마크에서 Gold와 Diamond 모두 9/30 (즉, pass@1 = 30%)을 달성했습니다. 이는 튜닝되지 않은 베이스라인인 8.6%보다 약 3.5배 높은 수치입니다. DPO 변형 모델은 Diamond에서 20%에 도달했습니다. 모든 체크포인트에서 Gold와 Diamond가 일치하며, 이는 자명한 속성 (Trivial-property)으로 인한 실패 모드를 방지합니다.