논문 요약: 언어 모델을 활용한 TLA+ 증명 자동화 (Towards Language Model Guided TLA+ Proof Automation)

이 논문은 분산 시스템 및 복잡한 알고리즘의 명세와 검증을 위해 널리 사용되는 형식 명세 언어인 **TLA+**의 증명 자동화를 위해 대규모 언어 모델 (LLM) 을 활용한 새로운 접근법인 **LMGPA(Language Model Guided Proof Automation)**를 제안합니다.

1. 문제 정의 (Problem Statement)

• TLA+ 증명의 어려움: TLA+ 는 엄격한 수학적 논리에 기반하여 시스템을 검증할 수 있게 하지만, 증명을 구성하는 과정은 상당한 전문 지식과 노력이 필요합니다. 이는 형식 검증의 확산을 저해하는 병목 현상입니다.
• 기존 LLM 기반 자동화의 한계: Lean 이나 Rocq(구 Coq) 와 같은 '전술 (tactic) 기반' 증명기에서는 LLM 이 증명 전술 시퀀스를 생성하여 성공적으로 작동해 왔습니다. 그러나 TLA+ 는 전술을 순차적으로 적용하는 방식이 아니라, 계층적 (hierarchical) 증명 구조를 따릅니다. 즉, 복잡한 명제를 증명하기 위해 중간 단계의 보조 명제 (sub-claims) 를 발견하고 계층적으로 분해해야 합니다.
• 직접 생성의 실패: LLM 에게 TLA+ 증명을 직접 생성하도록 요청하면, 문법 오류 (syntax errors) 가 빈번하게 발생하고, 전체 증명을 한 번에 생성하는 과정에서 초기 오류가 누적되어 검증 실패로 이어집니다. 또한 TLA+ 를 위한 대규모 학습 데이터셋이 부족합니다.

2. 방법론 (Methodology)

저자들은 LLM 의 추론 능력과 기호적 증명기 (symbolic provers) 의 엄격한 검증을 결합한 LMGPA 시스템을 제안합니다. 핵심 아이디어는 LLM 이 '완전한 증명'을 생성하는 대신, **'정규화된 (normalized) 주장 분해'**만 수행하도록 제한하는 것입니다.

핵심 구성 요소 및 알고리즘

1. 계층적 재귀 증명 생성 (Recursive Proof Generation):

   • 주어진 증명 의무 (proof obligation) 에 대해 먼저 기호적 방법 (TLAPS 의 OBVIOUS 또는 BY DEF 등) 으로 자동 증명을 시도합니다.
   • 자동 증명이 실패하면, LLM 을 활용하여 복잡한 목표를 더 단순한 **하위 주장 (sub-claims)**으로 분해합니다.
   • 분해된 하위 주장들이 부모 주장을 논리적으로 뒷받침하는지 TLAPS 를 통해 검증합니다.
   • 하위 주장들이 모두 증명 가능할 때까지 이 과정을 재귀적으로 반복합니다.

2. 정규화된 주장 분해 (Normalized Claim Decomposition):

   • LLM 이 생성하는 하위 주장의 형식을 엄격하게 제한합니다 (예: ASSUME ... PROVE ... 구조, ASCII 문자만 사용, 논리 기호의 표준화 등).
   • 이를 통해 LLM 이 생성하는 TLA+ 코드의 문법 오류를 극도로 줄이고, 시스템이 생성된 텍스트를 파싱하여 유효한 TLA+ 모듈로 변환할 수 있게 합니다.

3. 피드백 루프 (Adaptive Feedback Loop):

   • TLAPS 검증 실패 시, 오류 메시지를 LLM 에게 피드백하여 분해 전략을 수정하도록 유도합니다.

4. 기호적 자동 증명 (Symbolic Auto Proof):

   • 단순한 주장의 경우 LLM 호출 없이, 정의 (definition) 를 펼치는지 분석하여 OBVIOUS 또는 BY DEF 지시어를 자동으로 생성합니다.

3. 주요 기여 (Key Contributions)

• TLA+ 특화 증명 자동화 프레임워크: 전술 기반 증명기와는 근본적으로 다른 TLA+ 의 계층적 증명 구조에 맞춰 설계된 최초의 LLM 기반 자동화 시스템입니다.
• 정규화된 분해 전략: LLM 이 전체 증명을 생성하는 대신, 문법 오류를 최소화하는 정규화된 하위 주장만 생성하도록 제한함으로써 TLA+ 증명 자동화의 핵심 장벽인 문법 오류 문제를 해결했습니다.
• 새로운 벤치마크 구축: 수학 정리 (miniF2F, ProofNet 에서 변환) 와 분산 프로토콜의 귀납적 불변성 증명 (inductive invariants) 으로 구성된 119 개의 TLA+ 정리 벤치마크를 공개했습니다.
• 오픈 소스 및 아티팩트: 시스템 소스 코드와 생성된 증명 예시, 벤치마크를 GitHub 및 Zenodo 를 통해 공개했습니다.

4. 실험 결과 (Results)

저자들은 119 개의 정리 (93 개의 수학 정리 + 26 개의 분산 프로토콜 증명) 로 구성된 벤치마크에서 LMGPA 를 평가했습니다.

• 성공률 향상:
  • 수학 벤치마크: LMGPA 는 모든 테스트된 LLM(Claude, DeepSeek, Gemini, GPT-5 등) 에서 기존 베이스라인 (직접 LLM 생성, 순수 기호적 방법) 보다 일관되게 높은 증명 성공률을 보였습니다. 예를 들어, DeepSeek-V3.2-Exp 모델의 경우 LMGPA 를 적용했을 때 성공률이 59.1% 로, 직접 생성 (29.0%) 보다 크게 향상되었습니다.
  • 분산 프로토콜 벤치마크: LMGPA 는 42.3% ~ 50.0% 의 성공률을 기록하여 베이스라인 (0.0% ~ 38.5%) 을 압도했습니다.
• 문법 오류 감소:
  • 직접 생성 (DLPG) 방식은 생성된 증명의 문법 유효성이 매우 낮았음 (평균 20% 미만) 에 반해, LMGPA 의 분해 단계는 문법 유효성이 60%~86% 로 크게 개선되었습니다. 이는 정규화된 형식 제한이 문법 오류를 효과적으로 차단했음을 시사합니다.
• 효율성: LLM 호출 횟수를 줄이고, 검증 실패 시 전체 증명을 폐기하지 않고 국소적으로 수정할 수 있어 전체적인 처리 시간을 단축하거나 효율적으로 관리할 수 있었습니다.

5. 의의 및 결론 (Significance)

• 형식 검증의 접근성 확대: TLA+ 증명에 필요한 높은 진입 장벽을 낮추어, 산업계 (Amazon, Microsoft 등) 와 학계에서 TLA+ 를 활용한 형식 검증을 더 널리 사용할 수 있는 기반을 마련했습니다.
• LLM 과 기호적 도구의 시너지: LLM 의 창의적인 추론 (중간 단계 발견) 과 기호적 증명기의 엄격한 검증 능력을 결합한 하이브리드 접근법의 유효성을 입증했습니다.
• 향후 연구 방향:
  • TLA+ 증명 코퍼스로 LLM 을 미세 조정 (fine-tuning) 하여 성능을 더욱 향상시킬 수 있습니다.
  • LLM 이 생성한 분해가 수학적으로 타당할 뿐만 아니라, 자동 증명기가 검증하기 쉬운 (provability-aware) 형태인지 개선할 필요가 있습니다.
  • 데이터 누출 (data leakage) 문제를 해결하기 위한 새로운 벤치마크 구축이 필요합니다.

결론적으로, 이 논문은 TLA+ 와 같은 계층적 증명 구조를 가진 형식 시스템에서 LLM 을 효과적으로 활용하기 위한 새로운 패러다임을 제시하며, 형식 방법의 자동화 발전에 중요한 기여를 했습니다.