LLM은 TLA+로 실제 시스템을 모델링할 수 있는가?

Specula 팀이 SysMoBench를 공개하고, Claude·GPT·Gemini·DeepSeek·Kimi·Qwen 등 여러 LLM을 **TLA+**로 실제 시스템을 모델링하는 과제에 걸었다.

벤치마크는 11개 시스템을 대상으로 syntax, runtime, conformance, invariant의 4단계로 평가한다. 구문과 실행 가능성은 대체로 높았지만, 실제 코드 동작과의 일치성과 안전·라이브니스 불변식에서는 성능 격차가 크게 벌어졌다.

핵심 실패 패턴은 두 가지다.

• 교과서식 템플릿을 따라 도달 불가능한 상태를 만드는 경우
• 여러 단계로 나뉜 코드를 하나의 원자적 동작으로 합쳐, 실제로는 가능한 상태를 놓치는 경우

예로 ZooKeeper FLE에서는 recvset을 map이 아니라 set union으로 모델링하거나, 더 높은 electionEpoch를 처리하는 과정을 하나의 guard로 묶는 실수가 나왔다. 이를 잡기 위해 Transition Validation은 실제 실행 trace를 (pre_state, action, post_state) 윈도우로 쪼개 액션 단위로 검증한다.

결과는 구문 단계는 거의 **100%**에 가깝지만, conformance와 invariant에서 급격히 떨어졌다. 특히 Etcd, RedisRaft, CURP, PGo raftkvs 같은 복잡한 분산 시스템에서 약했고, 일부 모델은 전체 점수가 25% 수준에 그쳤다.

남은 과제도 분명하다.

• trace 커버리지를 더 넓혀야 함
• 상태 추상화로 생기는 정보 손실을 줄여야 함
• 새로운 시스템을 위한 하네스·불변식 템플릿·검증 모듈 자동화가 필요함