기술 요약: TLA-Prover

문제 정의

TLA+는 분산 시스템 및 안전 필수 프로토콜을 검증하기 위해 사용되는 형식 명세 언어이며, 전수 상태 공간 탐색을 위한 TLC 모델 체커와 함께 사용됩니다. 대규모 언어 모델(LLM)은 코드 생성에서 유망한 가능성을 보여주고 있지만, TLA+의 희소한 사전 학습 코퍼스 데이터와 독특한 구문(예: 시간 연산자, 집합 컴프리헨션)으로 인해 TLA+ 작업에서는 상당한 어려움을 겪고 있습니다.

FormaLLM 연구와 같은 기존 베이스라인에 따르면, 튜닝되지 않은 오픈 웨이트 LLM은 25개 모델에 대해 TLC 모델 체커를 통과하는 성공률이 8.6%에 불과했습니다. TLA+ 학습에서 LLM이 직면한 핵심 과제는 **보상 해킹(reward hacking)**입니다. TLA+ 및 TLC의 맥락에서, 모델은 이진(binary) "통과(pass)" 신호를 최적화하기 위해 사소하고 항진적인(tautological) 불변량(예: TypeOK == TRUE)을 생성할 수 있습니다. 이러한 명세는 도달 가능한 모든 상태에 대해 TLC를 통과하지만, 프로토콜에 대한 의미 있는 속성을 전달하지 못하므로 검증으로서의 가치가 없습니다. 단순히 TLC의 통과/실패 여부만을 보상 신호로 사용하는 표준 강화 학습 방식은 이러한 실패 모드에 취약합니다.

방법론

저자들은 TLA+ 명세 합성을 위해 설계된 200억 파라미터 모델(gpt-oss-20b 기반)인 TLA-Prover를 제시합니다. 이 접근 방식은 지도 미세 조정(SFT)과 복구 기반 그룹 상대 정책 최적화(GRPO) 및 4단계 검증 계층 구조를 결려한 새로운 훈련 파이프라인을 결합합니다.

1. 4단계 검증 계층 구조

보상 해킹을 방지하고 의미론적 타당성을 보장하기 위해, 모든 모델 출력은 결정론적인 외부 파이프라인에 의해 네 가지 티어로 분류됩니다:

• 브론즈(Bronze): 출력이 SANY 파서를 통과하지 못함 (구문 오류).
• 실버(Silver): 출력이 파싱은 되지만 TLC에서 로드하거나 실행하는 데 실패함 (예: 타임아웃, 타입 에러).
• 골드(Gold): 출력이 SANY와 TLC를 모두 통과함; 모델 체커가 상태 공간을 모두 탐색하였으며 모든 불변량이 성립함.
• 다이아몬드(Diamond): 출력이 골드 조건을 통과할 뿐만 아니라, 불변량이 **변이 민감성(mutation-sensitive)**을 가짐.
  • 메커니즘: 불변량 서술어(predicate)에 자동화된 AST 수준의 변이(예: 결합 조건 부정, 관계 연산자 반전, 상수 교체)를 적용합니다. 변이된 명세를 다시 TLC로 실행합니다.
  • 기준: 만약 변이가 TLC에서 반례(counterexample)를 찾아낸다면, 원래의 불변량은 비자명(non-trivial)한 것으로 간주됩니다(다이아몬드). 만약 변이 후에도 TLC가 통과한다면(예: 불변량이 TRUE인 경우), 해당 출력은 다이아몬드 검사를 통과하지 못합니다. 이 단계는 항진적 불변량을 명시적으로 차단합니다.

2. 훈련 파이프라인

훈련 과정은 두 가지 주요 단계로 구성되며, 비교를 위한 DPO 절제 실험(ablation)이 포함됩니다:

• 1단계: 지도 미세 조정 (SFT)

  • 코퍼스: 엄격하게 다이아몬드 티어로 필터링된 1,053개의 명세 큐레이션 데이터셋. 데이터는 TLA+ 재단 배포본과 tlaplus/examples 저장소에서 가져왔으며, Ollama 생성기와 LLM 판별기 및 4단계 파이프라인을 통해 보강 및 필터링되었습니다.
  • 아키텍처: 20B 파라미터 베이스 모델의 어텐션 프로젝션에 LoRA 어댑터(rank 8, alpha 16)를 적용했습니다.
  • 목표: 모델에게 TLA+의 구조적 어휘와 구문을 가르치는 것입니다.

• 2단계: 복구 기반 그룹 상대 정책 최적화 (GRPO)

  • 동기: 표준 GRPO는 그룹 내 모든 샘플이 검증기에서 실패할 때(희소 보상), 어드밴티지가 0이 되어 그래디언트 흐름이 끊기는 문제가 발생합니다.
  • 메커니즘: 모델에게 "고장 난" 명세(이전의 실패 시도에서 추출됨)를 제시하고 이를 복구하도록 합니다.
  • 보상 신호: 티어 전환에 기반한 연속적인 개선 점수(Bronze→Silver: 0.1, Silver→Gold: 0.3, Gold→Diamond: 0.6)를 제공합니다. 이는 최종 출력이 완벽하지 않더라도 티어가 개선되는 한 조밀한 그래디언트를 제공합니다.
  • 프로세스: 모델은 TLC 에러 메시지를 피드백으로 사용하여 자신의 출력을 반복적으로 수정합니다.

• 절제 실험 (DPO): 동일한 SFT 체크포인트로부터 정적 선호 쌍(Diamond > Gold > Silver > Bronze)을 사용하여 훈련된 직접 선호 최적화(DPO) 변형 모델을 비교 대상으로 사용했습니다.

주요 결과

모델은 홀드아웃(held-out) 30문제 벤치마크에서 싱글 샷 그리디 디코딩(single-shot greedy decoding)으로 평가되었습니다.

• 성능: TLA-Prover(최종 복구-GRPO 체크포인트)는 골드 및 다이아몬드 티어 모두에서 30%의 통과율(9/30)을 달 기록했습니다.
• 베이스라인 비교: 이는 8.6%였던 튜닝되지 않은 FormaLLM 베이스라인 대비 3.5배의 향상을 나타냅니다.
• 절제 실험 비교 (DPO): DPO 변형 모델은 20%의 다이아몬드 통과율을 기록했으며, 이는 복구-GRPO 방식(30%)에 의해 상회되었습니다.
• 안티-보상 해킹 검증: 결정적으로, 생산 파이프라인의 모든 체크포인트에서 골드와 다이아몬드 통과율이 일치했습니다(차이 0). 이는 모델이 TLC는 통과하지만 변이 테스트는 통과하지 못하는 항진적 불변량을 생성하는 법을 배우지 않았음을 나타냅니다. DPO 절제 실험에서 발생한 단 하나의 예외는 다이아몬드 티어가 성공적으로 잡아냈습니다.
• 추론 전략:
  • Best-of-8 샘플링은 다이아몬드 통과율을 37%(11/30)로 높였습니다.
  • Greedy ∪ Best-of-8 합집합은 43%(13/30)의 천장을 시사하며, 이는 모델이 여러 번의 시도가 주어진다면 더 많은 문제를 해결할 능력이 있음을 나타냅니다.
  • 자기 수정(Self-correction) (3-shot TLC 피드백)은 개선을 보이지 않았으며, 이는 실패의 원인이 무작위 샘플링 오류가 아닌 지식의 부재에 있음을 시사합니다.

의의 및 기여

본 논문은 세 가지 주요 기여를 주장합니다:

1. 4단계 계층 구조를 갖춘 TLA-Prover: 상위 티어(다이아몬드)가 변이 테스트를 사용하여 항진적 불변량을 배제하는 검증 계층 구조를 도입했습니다. 이는 TLC를 보상 신호로 사용할 때 발생하는 특유의 보상 해킹 위험을 해결하여, "통과"가 의미 있는 명세를 의미하도록 보장합니다.
2. 복구 기반 GRPO 파이프라인: 다이아몬드 티어 코퍼스로 SFT를 수행하고 복구 기반 GRPO를 결합한 2단계 훈련 파이프라인입니다. 이 방식은 검증기로부터의 온라인 피드백을 활용하여 조밀한 보상 신호를 제공함으로써, 정적인 DPO 절제 모델보다 우수한 성능을 보입니다.
3. 경험적 안티-보상 해킹 분석: 골드와 다이아몬드 통과율이 모든 체크포인트에서 일치한다는 관찰 결과는, 본 파이프라인이 "항상 참인 불변량"이라는 실패 모드를 성공적으로 방지했음을 입증하는 경험적 근거를 제공합니다.

저자들은 본 연구가 FormaLLM 베이스라인을 실질적으로 초과하는 최초의 TLA+ 타겟 훈련 연구라고 위치시킵니다. 이 모델은 명세 합성을 크게 개선했지만, 현재는 케이스 분석이나 양화사 조작이 필요한 복잡한 프로토콜보다는 불변량 스타일의 명세와 작은 상태 공간을 가진 문제에 특화되어 있습니다. 이 연구는 다이아몬드 티어와 같은 안티-보상 해킹 검증 없이 검증기 가이드 훈련을 수행하는 것은 의미 있는 형식 명세를 생성하는 데 불충분하다는 점을 강조합니다.