LLM이 TLA+로 실제 시스템을 제대로 모델링할 수 있을까? — SysMoBench 벤치마크
Can LLMs model real-world systems in TLA+?
TL;DR Highlight
LLM이 TLA+ 명세를 작성할 때 문법은 잘 통과하지만 실제 시스템과의 동작 일치도(conformance)는 46% 수준에 그친다는 걸 체계적으로 검증한 벤치마크 연구로, AI 기반 형식 검증의 현실적 한계를 보여준다.
Who Should Read
분산 시스템이나 동시성 코드를 설계/검증하는 개발자, 또는 LLM을 활용해 TLA+ 같은 형식 명세(formal specification) 작성을 자동화하려는 엔지니어.
Core Mechanics
- 이 연구를 시작한 계기는 Claude에게 Etcd의 Raft 구현에 대한 TLA+ 명세를 작성해달라고 했더니, Raft 논문 부록에 있는 명세를 그대로 가져다 냈기 때문이다. 문법도 맞고 모델 체커도 통과했지만, Etcd 실제 구현과는 무관한 명세였다.
- 이를 구별하기 위해 SysMoBench라는 자동 벤치마크를 만들었다. 동시성 동기화 및 분산 프로토콜을 포함한 11개 실제 시스템(ZooKeeper, etcd 등)을 대상으로, LLM이 생성한 TLA+ 명세를 4단계로 자동 평가한다.
- 4단계 평가는 순서대로 syntax(컴파일 가능 여부) → runtime(TLC 모델 체커 실행 오류 없는지) → conformance(실제 코드 실행 트레이스와 명세가 일치하는지) → invariant(안전성·활성 속성 만족 여부)로 구성된다.
- Claude, GPT, Gemini, DeepSeek, Kimi, Qwen 등 주요 LLM을 평가한 결과, syntax 단계는 거의 완벽에 가깝게 통과하지만, conformance 평균은 46%, invariant 평균은 41%에 불과했다. 명세가 예쁘게 생겼다고 올바른 건 아니라는 걸 수치로 보여준다.
- LLM 명세의 실패 패턴은 두 가지로 반복된다. 하나는 실제 시스템이 절대 도달할 수 없는 상태를 명세가 허용하는 것, 다른 하나는 실제 시스템이 반드시 도달하는 상태에 명세가 도달하지 못하는 것이다.
- 구체적 예시로, ZooKeeper Fast Leader Election(FLE) 명세에서 Claude Sonnet은 각 서버의 recvset(투표 수신 맵)을 map이 아닌 set union으로 구현했다. 실제 ZooKeeper는 같은 피어가 새 라운드에서 투표하면 이전 투표를 덮어쓰는데, LLM은 형식검증 교과서의 '모든 투표를 증거로 누적' 패턴을 따라서 두 투표를 모두 유지했다.
- 이런 오류가 발생하는 근본 원인은 LLM이 실제 구현 코드의 세부 동작을 추상화하는 게 아니라, 인터넷에 공개된 참고 논문이나 교과서 공식화 패턴을 재현하기 때문이다. LLM은 훈련 데이터에서 본 TLA+ 예제를 '기억'할 뿐이다.
- SysMoBench는 단일 점수가 아닌 action별, invariant별로 세분화된 진단 결과를 제공한다. 어느 액션에서 실제 구현과 어긋나는지 정확히 찾아낼 수 있어서 단순 합격/불합격보다 훨씬 유용하다.
Evidence
- 실제 TLA+ 작성 경험자는 'LLM이 safety 속성은 어느 정도 도움이 되지만, liveness(활성) 속성을 올바르게 잡아내는 건 훨씬 어렵다'고 지적했다. 또한 LLM이 만든 모델에서 상태 공간 폭발(state space explosion)이 자주 발생하는데, 간단한 모델은 유도해주면 수정 가능하다는 경험도 공유됐다.
- 람포트(Lamport)의 '쓰지 않고 생각하는 건 생각하는 척일 뿐'이라는 말을 인용하며, 첫 초안은 반드시 직접 손으로 작성하고 전체 구조가 잡힌 후에 LLM을 추가 탐색 도구로 활용한다는 워크플로우를 소개한 댓글이 공감을 받았다.
- TLA+와 별개로 Verus(구현 코드와 검증을 동시에 작성하는 Rust 기반 도구)를 옹호하는 의견이 있었다. 구현과 모델이 분리된 TLA+ 방식은 양쪽이 엇갈릴 위험이 있는데, Verus처럼 구현-검증을 결합하면 이 문제를 원천 차단한다는 주장이었다.
- 'LLM이 설계(TLA+)도 만들고 그 설계를 만족하는 코드도 쓴다면, 인간의 의도(intent)는 어디에 있는가? 인간이 원하는 걸 명시하지 않은 채 LLM이 검증까지 하면 무엇을 증명한 것인가?'라는 근본적 질문이 제기됐다.
- '이름(Raft, Etcd 등)을 난독화한 소스코드만 주고 TLA+ 명세를 만들어달라면 어떤 결과가 나오나?'라는 질문이 댓글에 등장했는데, 이는 LLM이 이름 기반으로 학습 데이터를 재활용하는지 여부를 확인하는 흥미로운 실험 방향으로 주목받았다.
- TLAiBench(https://github.com/tlaplus/TLAiBench)라는 별도 벤치마크도 소개됐다. 논리 퍼즐과 실세계 시나리오를 포함한 TLA+ 평가 데이터셋으로, SysMoBench와 유사한 방향의 커뮤니티 프로젝트다.
- 벤치마크 테스트 케이스 자체가 이미 LLM 훈련 데이터에 포함되어 있을 가능성을 지적한 댓글도 있었다. 완전히 새로운 복잡한 시스템 명세 설계에서 LLM이 어떤 성능을 보이는지가 진짜 핵심이라는 의견이었다.
How to Apply
- LLM으로 TLA+ 명세를 생성한 후 '잘 컴파일되고 TLC가 통과하니 됐다'고 안심하고 싶을 때, SysMoBench의 conformance 단계처럼 실제 코드 실행 트레이스를 수집해 명세와 대조하는 검증 단계를 반드시 추가해야 한다. 문법 통과가 정확성을 보장하지 않는다.
- LLM에게 Raft, Paxos 같은 유명 프로토콜의 구현체(예: etcd, ZooKeeper)에 대한 TLA+ 명세를 요청할 때는 시스템 이름을 난독화하거나 소스코드를 직접 붙여넣는 방식으로 제공해서, LLM이 논문 암기가 아닌 실제 코드 추상화를 하도록 유도하는 게 좋다.
- 구현과 검증 코드가 분리되면 양쪽이 엇갈릴 위험이 걱정된다면, Verus(https://github.com/verus-lang/verus) 같이 Rust 코드 안에서 직접 증명을 작성하는 도구를 검토할 수 있다. 이 방식은 모델-구현 불일치 문제를 구조적으로 차단한다.
- TLA+ 명세 작성 워크플로우에서 LLM을 활용하려면, 첫 초안(특히 상태 변수 정의, 액션 분해 방식)은 직접 손으로 작성해서 시스템의 실제 데이터 구조를 반영하고, 그 이후 TLC 디버깅이나 invariant 탐색 단계에서 LLM을 보조 도구로 사용하는 방식이 더 안전하다.
Terminology
관련 논문
Natural Language Autoencoders: Claude의 내부 활성화를 자연어 텍스트로 변환하는 기법
Anthropic이 LLM 내부의 숫자 벡터(활성화값)를 직접 읽을 수 있는 자연어로 변환하는 NLA 기법을 공개했다. AI가 실제로 무슨 생각을 하는지 해석하는 interpretability 연구의 새로운 진전이다.
ProgramBench: LLM이 프로그램을 처음부터 다시 만들 수 있을까?
LLM이 FFmpeg, SQLite, PHP 인터프리터 같은 실제 소프트웨어를 문서만 보고 처음부터 재구현할 수 있는지 측정하는 새 벤치마크로, 최고 모델도 전체 태스크의 3%만 95% 이상 통과하는 수준에 그쳤다.
MOSAIC-Bench:코딩 에이전트의 Compositional Vulnerability 유도 측정
티켓 3장으로 쪼개면 Claude/GPT도 보안 취약점 코드를 53~86% 확률로 그냥 짜준다.
LLM의 거절(Refusal) 동작은 단 하나의 방향(Direction)으로 제어된다
13개의 오픈소스 채팅 모델을 분석했더니, 모델이 유해한 요청을 거절하는 동작이 내부 활성화 공간에서 단 하나의 1차원 벡터 방향으로 인코딩되어 있었다. 이 방향을 제거하면 안전 파인튜닝이 사실상 무력화되므로, 현재 안전 학습 방식이 얼마나 취약한지 보여준다.
LLM의 구조화된 출력(Structured Output)을 테스트하는 새 벤치마크 SOB 공개
스키마 준수 여부만 보던 기존 벤치마크의 한계를 넘어, 실제 값의 정확도까지 7가지 지표로 평가하는 Structured Output Benchmark(SOB)가 공개됐다. 인보이스 파싱, 의료 기록 추출처럼 JSON 출력의 정확성이 중요한 프로덕션 시스템에서 어떤 모델을 써야 할지 판단하는 데 직접적으로 참고할 수 있다.
Claude.ai 전면 장애 및 API 오류 급증 인시던트 리포트 (2026년 4월 28일)
Anthropic의 Claude.ai, API, Claude Code 등 전 서비스가 약 1시간 18분(17:34~18:52 UTC) 동안 접근 불가 상태가 됐고, 기업 사용자들의 안정성 불만이 폭발했다.