LLM이 TLA+로 실제 세계의 시스템을 모델링할 수 있는가?

편집자 주: AI는 컴퓨팅 시스템을 위한 응용 형식 방법론 (applied formal methods)의 경계를 적극적으로 넓혀왔습니다. 이 글에서 Specula 팀은 병렬 및 분산 시스템을 위한 명세 언어 (specification language)인 TLA+를 사용하여, 에이전트 기반 모델 체킹 (agentic model checking)의 기본 역량인 시스템 코드 모델링에 대한 LLM 평가 경험을 작성했습니다. 이 글은 'The Next Horizon of System Intelligence' 시리즈의 일곱 번째 블로그입니다.

몇 달 전, 우리는 Claude에게 Etcd의 Raft 구현을 위한 TLA+ 명세 (spec)를 작성하도록 요청했습니다. 그것은 구문 검사 (syntax checks)를 통과했고, TLC 모델 체커 (model checker)를 통해 실행되었으며, 언뜻 보기에는 다듬어진 형식 모델 (formal model)처럼 보였습니다. 그러다 우리는 한 가지를 발견했습니다. 이것은 Raft 논문에 나온 명세와 매우 유사하며, Etcd 특유의 세부 사항과는 거의 관련이 없다는 점이었습니다. Claude가 생성한 것은 Etcd를 위한 명세가 아니었습니다. 그것은 Raft 논문의 부록에 있는 명세였습니다. 이후 우리는 다음과 같은 질문을 계속 던지게 되었습니다. AI가 컴퓨팅 시스템을 충실하게 모델링하고 있는지, 아니면 단순히 시스템의 참조 논문을 암기하여 읊고 있는 것인지 어떻게 구별할 수 있을까?

대규모 언어 모델 (LLMs)이 계속 발전함에 따라 이 질문에 답하기는 더욱 어려워지고 있습니다. LLM은 온라인에 있는 거의 모든 TLA+ 예제를 학습했습니다. LLM에게 "Raft 명세를 작성하라"고 요청하는 것은 학습한 내용을 회상하라고 요청하는 것과 거의 같습니다. 반면, Etcd가 원자적 동작 (atomic actions)을 실제로 어떻게 분해하고 상태 (state)를 진화시키는지 반영하는 명세인 "Etcd의 명세를 작성하라"고 요청하는 것은 완전히 다른 문제입니다. 이는 LLM이 복잡한 구현으로부터 로직을 추상화하고, 그 추상화를 올바른 형식 모델로 변환할 수 있는지를 테스트합니다.

SysMoBench는 자동화된 벤치마크를 통해 이 두 가지를 구분하려는 우리의 시도입니다.

SysMoBench란 무엇인가?

SysMoBench는 LLM에게 11개의 시스템을 제공하고, 생성된 TLA+ 명세를 자동으로 평가합니다.

표 1: SysMoBench에서 아티팩트 (artifacts)로 사용된 시스템들

11개의 시스템은 병렬 동기화 (concurrent synchronization) 및 분산 프로토콜 (distributed protocols)을 아우릅니다. 각 작업에 대해 우리는 소스 코드, 트레이스 수집 하네스 (trace-collection harness), 그리고 불변량 템플릿 (invariant template)을 제공합니다.

그림 1: SysMoBench 개요

평가는 네 가지 단계로 진행됩니다:

• 구문 단계 (syntax phase)는 명세 (spec)가 컴파일되는지 확인합니다.
• 런타임 단계 (runtime phase)는 TLC가 오류 없이 이를 실행할 수 있는지 확인합니다.
• 일치 단계 (conformance phase)는 명세와 코드 간의 일관성을 확인하는 일반적인 방법인 트레이스 검증 (trace validation)을 사용합니다. 즉, 코드에서 생성된 실행 트레이스 (execution traces)를 모델과 비교합니다.
• 불변량 단계 (invariant phase)는 명세가 주요 안전성 (safety) 및 활성 (liveness) 속성을 만족하는지 확인합니다.

이 네 가지 단계는 교과서적인 내용만 나열하는 명세와 실제로 시스템을 모델링하는 명세 사이의 격차를 드러냅니다. 각 단계는 단일 통합 점수 대신 동작 (action) 또는 불변량 (invariant) 단위의 진단을 생성하므로, 명세가 구현과 어떤 동작이나 불변량에서 어긋나는지 정확히 파악할 수 있습니다.

LLM 모델링 패턴

오늘날의 선도적인 LLM들 — Claude, GPT, Gemini, DeepSeek, Kimi, Qwen 등 — 을 SysMoBench에서 실행했을 때, 반복적인 패턴이 나타납니다. 이들의 명세는 처음 두 단계(구문 및 런타임)에서는 상당히 좋은 성능을 보입니다. 대부분 깔끔하게 컴파일되며, 많은 경우 TLC를 통해 오류 없이 실행됩니다. 하지만 평가가 일치 단계에 도달하면, 두 가지 체계적인 형태의 "교과서적 모델링 (textbook modeling)"이 명확해집니다: (1) 명세가 실제 시스템이 결코 도달할 수 없는 상태에 진입하거나, (2) 명세가 실제 시스템이 항상 도달하는 상태에 도달하지 못하는 경우입니다. 이 두 가지 실패 모드 (failure modes)는 일치 및 불변량 점수에 직접적으로 나타납니다. 최신 선도 LLM들조차 구문 단계에서의 완벽에 가까운 점수와 비교했을 때, 일치 단계에서는 평균 약 46%, 불변량 단계에서는 약 41%의 점수를 기록합니다.

명세가 실제 세계의 시스템이 결코 도달하지 않는 상태에 진입하는 경우, LLM은 시스템의 실제 데이터 구조와 일치하지 않는 일반적인 정식화 템플릿 (formalization template)을 따라 명세를 작성하며, 그 결과 실제 시스템은 결코 생성하지 않을 상태를 만드는 전이 (transitions)를 명세가 허용하게 됩니다. 구체적인 예로 Claude Sonnet이 작성한 ZooKeeper Fast Leader Election (FLE) 명세가 있습니다.

그림 2: LLM이 생성한 ZooKeeper FLE 명세의 두 가지 실패 모드

ZooKeeper 코드에서 각 서버의 recvset은 송신자를 키로 하는 맵(map)입니다. 동일한 피어(peer)가 새로운 라운드에서 새로운 투표를 보내면, 해당 피어의 이전 투표를 덮어씁니다. Sonnet은 이를 집합 합집합(set union)인 recvVotes' = recvVotes ∪ {newVote}로 작성하여, 이전 투표와 새로운 투표를 모두 유지했습니다. "모든 투표를 증거로서 축적한다"는 패턴은 많은 형식 기법 (formal-methods) 교과서에 등장하지만, 이는 ZooKeeper의 의미론 (semantics)과 일치하지 않습니다. 결과적으로, 라운드에 따라 피어의 투표가 변경될 때마다 (이는 ZooKeeper의 선거 과정에서 일상적으로 발생합니다), 명세 (spec)의 사후 상태 (post-state)에는 이전 투표와 새로운 투표가 모두 포함되는 반면, 실제 시스템은 새로운 투표만을 유지합니다. 일단 하위 쿼럼 체크 (quorum check)가 투표 수에 의존하게 되면, 명세는 실제 코드가 절대 진입하지 않는 상태에 직면하게 됩니다.

명세가 실제 시스템이 도달하는 상태에 도달하지 못하는 경우, LLM은 코드에서 여러 단계에 걸쳐 수행되는 연산들을 하나의 원자적 가드 (atomic guard)로 병합하여, 명세 내에서 전이 (transition)를 불가능하게 만듭니다. Sonnet의 동일한 ZooKeeper 명세에서, HandleNotification 액션은 들어오는 메시지의 에포크 (epoch)가 로컬 logicalClock보다 높은지 확인하는 가드 m.electionEpoch <= logicalClock[s]를 포함하고 있습니다. 만약 그렇다면, 해당 액션은 비활성화됩니다. 하지만 ZooKeeper의 코드는 이런 방식으로 작동하지 않습니다. 서버가 더 높은 electionEpoch를 가진 메시지를 받으면, 먼저 자신의 logicalClock을 이에 맞춰 증가시킨 다음 메시지를 처리합니다. 이 두 단계는 코드에서 해당 순서대로 발생합니다. 그러나 LLM은 이들을 하나의 가드로 융합하였고, 그 과정에서 모든 선거 라운드마다 코드가 진입하는 상태 (로컬 에포크=1, 들어오는 에포크=2)를 지워버렸습니다.

위의 두 가지 패턴은 공통된 원인을 공유합니다. LLM은 구조적으로 완전하고 타입이 올바른 (type-correct) TLA+ 모듈을 생성하지만, 이는 실제 구현을 반영하기보다는 교과서적인 정형화 템플릿 (textbook formalization templates)에 따라 작성됩니다. LLM은 Raft와 ZAB가 프로토콜로서 어떤 모습인지 알고 있지만, Etcd나 ZooKeeper가 특정 동작을 어떻게 여러 단계로 나누는지(splits a particular action across multiple steps)는 알지 못합니다. 이것이 바로 구문 (syntax) 및 런타임 평가 (runtime evaluation) 기준만으로는 충분하지 않은 정확한 이유입니다. LLM이 생성한 명세 (specs)는 모두 구조적으로 완전하고 구문적으로 깨끗하기 때문에 SANY TLA+ 파서 (parser)를 통과합니다. “Etcd를 모델링하는 것”과 “Raft 논문을 암송하는 것”을 구분하기 위해서는, 평가가 적합성 (conformance) 및 불변량 (invariant) 단계에 도달하여, 각 동작 (action)의 전이 (transition)가 시스템이 런타임에 실제로 생성하는 상태 변화와 일치하는지 물어야 합니다.

전이 검증 (Transition Validation): 동작 단위의 명세 읽기

SysMoBench의 모든 단계는 단일 집계 점수를 넘어 동작별 (per-action) 또는 불변량별 (per-invariant) 진단 결과를 생성합니다. 구문 (syntax) 단계에서는 모듈 전체를 컴파일하는 대신, 어떤 동작이 잘못되었는지 국소화하기 위해 동작별 분해 (per-action decomposition)를 수행합니다. 런타임 (runtime) 단계에서는 TLC가 명세를 실행할 수 있는지 여부뿐만 아니라, 상태 공간 (state space)에 대한 동작별 커버리지 (per-action coverage)를 분석합니다. 불변량 (invariant) 단계에서는 각 불변량을 개별적으로 검증하며, 이때 LLM은 고정된 템플릿을 각 생성된 명세에 맞는 실행 가능한 불변량으로 번역합니다. 적합성 (conformance) 단계에서는 우리가 *전이 검증 (Transition Validation)*이라 부르는 방식을 사용하며, 이는 “교과서적인 프로토콜을 암송하는 것”과 “시스템을 모델링하는 것” 사이의 간극을 가장 직접적으로 드러냅니다.

아이디어는 간단합니다. 시스템의 실제 실행에서 실행 트레이스 (execution traces)를 수집한 다음, 각 트레이스를 일련의 “전이 윈도우 (transition windows)”로 자릅니다. 하나의 윈도우는 (pre_state, action, post_state)라는 세 쌍(triple)으로 구성됩니다. 각 윈도우는 TLC에 독립적으로 입력되며, TLC는 명세의 동작이 pre_state에서 post_state로 이동할 수 있는지 확인합니다. 출력값은 단일 점수가 아니라 동작별 상세 내역 (per-action breakdown)이며, 각 동작당 하나의 통과율 (pass rate)이 제공됩니다.

구체적인 예시로, Asterinas RwMutex에 대해 전이 검증 (Transition Validation)을 실행하면 출력값은 동작별 상세 내역 (per-action scorecard)이며, 각 동작당 하나의 통과율 (pass rate)이 제공됩니다. 거친 입도 (Coarse-grained) 평가로는 이러한 종류의 진단 (diagnostics)을 제공할 수 없습니다. 단일 점수는 명세 (spec)가 통과했는지 실패했는지만 알려주는 반면, 전이 검증 (Transition Validation)은 어떤 동작이 어긋났는지뿐만 아니라, 트레이스 (trace) 내의 특정 윈도우 (window)에 고정된 어떤 구체적인 상태 전이 (state transition)가 실패했는지까지 알려줍니다.

결과: 점수가 갈리는 지점

11개의 시스템에 걸쳐 주요 LLM들을 실행해 본 결과, LLM은 올바른 TLA+ 구문 (syntax)을 생성하는 데는 뛰어나지만, 준수성 (conformance)과 적절한 불변량 (invariants)을 보장하는 데는 어려움을 겪는 것으로 나타났습니다.

그림 3: SysMoBench에서 11개 LLM의 단계별 점수 (전체 점수순 정렬); 서로 다른 LLM의 순위는 SysMoBench 리더보드에서 확인할 수 있습니다.

대부분의 LLM은 구문 (syntax) 단계에서 100% 근처에 밀집해 있습니다. 거의 모든 프런티어 (frontier) LLM은 구문적으로 유효한 TLA+ 명세 (spec)를 작성할 수 있습니다. 런타임 (runtime) 단계에서는 이미 30%에서 92%까지 차이를 보이며 분산되기 시작합니다. 진짜 격차는 준수성 (conformance)과 불변량 (invariance)에서 벌어집니다. 불변량 (invariant) 단계에서 가장 성능이 낮은 LLM은 16%에 머무는 반면, Gemini 3.1은 81%에 도달합니다.

이러한 낮은 준수성 (conformance) 및 불변량 (invariant) 점수 패턴은 시스템별 수준에서도 일관되게 나타납니다. 그림 4는 Claude Sonnet-4.6을 대표 모델로 사용하여 이를 설명합니다. 더 단순한 시스템 (Asterinas Spin, Mutex, RwMutex)에서는 거의 모든 LLM이 1단계 (구문, syntax)부터 4단계 (불변량, invariant)까지 높은 점수로 완료합니다. 복잡한 분산 시스템 (Etcd, RedisRaft, CURP, PGo raftkvs)의 경우, LLM들은 1단계 (구문, syntax)에서 안정적으로 100% 또는 100%에 가까운 점수를 기록하지만, 2단계 (런타임, runtime)부터 무너지기 시작합니다. 일부는 TLC를 아예 실행하지 못하기도 하며, 실행에 성공하더라도 준수성 (conformance) 및 불변량 (invariant) 점수는 10%에서 50% 사이에 머뭅니다. 가장 강력한 LLM 중 하나인 Claude Sonnet 4.6조차 RedisRaft와 CURP에서는 전체 점수가 25%에 불과합니다.

그림 4: 난이도 수준별(쉬움에서 어려움 순) 다양한 시스템에 대한 Claude Sonnet-4.6의 전체 점수.

우리는 여러 LLM에서 유사한 동작을 관찰했습니다. 컴파일 가능한 TLA+ 모듈을 작성하는 것은 가능하지만, 해당 모듈을 특정 시스템의 실제 동작과 일치시키는 것은 어렵습니다. 높은 구문 (syntax) 점수는 주로 학습 데이터에 풍부하게 존재하는 TLA+ 예시들을 반영합니다. 평가가 실제 코드와 같은 방식으로 동작 (actions)을 분해하고 상태 (state)를 데이터 구조와 매칭하는 것을 요구하게 되면, 이전의 예시들은 더 이상 유용하지 않게 됩니다. 적합성 (conformance)과 불변량 세밀도 (invariant granularity)를 분리하여 평가하는 것이 바로 "TLA+ 작성"과 "특정 시스템 모델링"을 구분할 수 있게 해주는 핵심입니다.

해결되지 않은 과제 (Open Challenges)

몇 가지 미해결 문제가 남아 있습니다.

첫째, 윈도우 수준 (window-level) 평가는 트레이스 샘플링 (trace sampling)에 크게 의존합니다. 전이 검증 (Transition Validation)은 트레이스가 커버하지 않는 코드 경로를 평가할 수 없습니다. 구체적인 예로, 우리의 실행 중 하나에서 Asterinas RwMutex의 AcquireUpReadLock 동작은 0개의 윈도우로 나타났습니다. 이는 명세 (spec)가 실패했기 때문이 아니라, 해당 트레이스에서 upread() 코드 경로가 단순히 실행되지 않았기 때문입니다. 전이 검증은 이를 명확하게 보고하지만, 스스로 그 간극을 메울 수는 없습니다. 체계적으로 트레이스 커버리지를 확장하는 것은 여전히 해결해야 할 과제로 남아 있습니다.

둘째, 상태 추상화 (state abstraction)는 필연적으로 정보를 손실합니다. 변수 log를 (logLen, logLastTerm) 쌍으로 표현하는 것은, 특정 중간 항목의 term을 확인하는 HandleAppendEntries와 같이 로그 내용을 심층적으로 조사하는 동작들에 대해 정보 손실을 초래합니다. 우리는 현재 체계적인 정책 없이 전이 검증 모듈 내부에서 수동으로 이러한 부분을 완화하고 있습니다.

셋째, 작업 간의 일반화 (generalizability)가 과제입니다. 새로운 시스템을 추가하려면 여전히 수동으로 작성된 하네스 (harness), 불변량 템플릿 (invariant template), 그리고 전이 검증 모듈이 필요합니다. 우리는 이 파이프라인을 위한 자동화 스캐폴딩 (scaffolding)을 구축하고 있지만, 완전한 자동화를 위해서는 더 많은 엔지니어링 노력이 필요할 것입니다.

이것들은 우리가 해결한 문제가 아니라, (이상적으로는 커뮤니티와 함께) 해결해 나가기를 희망하는 미해결 과제들입니다. 이 중 관심 있는 내용이 있다면, 저희와 협업하고 싶습니다!

다음 단계 (What’s Next)

저희는 단순한 LLM (Large Language Models)을 넘어 더욱 강력한 에이전트 도구 (agentic tools)를 구축하는 동시에, SysMoBench를 지속적으로 개선해 나가고 있습니다.

실제로 저희는 Claude Code나 Codex와 같은 최첨단 코드 에이전트 (frontier code agents)들이 이미 실제 세계의 시스템을 TLA+로 모델링하는 데 강력한 능력을 갖추고 있음을 발견했습니다. 이들은 대상 저장소 (repository)를 자율적으로 읽고, 무엇을 모델링할지 결정하며, 전체 명세 (specification) 워크플로우를 주도할 수 있습니다. 저희는 TLA+ 형식 모델링 (formal modeling)에 특화된 에이전트인 Specula를 개발하고 있습니다. Specula는 현재 SysMoBench 작업에서 완전 일치 (full conformance) 및 불변량 (invariant) 점수를 달성했습니다 (저희의 리더보드 참조).

sysmobench.com의 리더보드는 새로운 LLM과 시스템을 지속적으로 수집하고 있습니다. 새로운 시스템, 새로운 LLM, 그리고 새로운 결과에 대한 기여를 환영합니다!

논문 (Paper): https://arxiv.org/abs/2509.23130 [1]
코드 (Code): https://github.com/specula-org/SysMoBench
리더보드 (Leaderboard): https://sysmobench.com

[1] LLM의 급격한 발전으로 인해, 이 글에서 보고된 평가 수치는 원본 논문의 수치와 다를 수 있습니다. 사실, 이 글은 새로운 모델 세트로 SysMoBench를 다시 실행해 달라는 최근의 요청에 의해 작성되었습니다. 저희 리더보드는 새로운 모델들을 계속 추적하고 있습니다.