교과서를 넘어: 실제 TLA+ 모델링에 대한 LLM 평가

수년 동안 TLA+는 동시성 및 분산 시스템을 명세하는 표준으로 자리 잡아 왔으며, 엔지니어들이 단 한 줄의 코드를 작성하기 전에 중요한 설계 결함을 포착할 수 있도록 해 주었습니다. 대규모 언어 모델(LLM)의 부상과 함께, 이 엄격한 프로세스를 AI에 위임하려는 유혹이 커지고 있습니다. 그러나 중요한 질문이 남아 있습니다. AI가 실제로 당면한 시스템을 모델링하고 있는 것일까요, 아니면 단순히 학습 데이터에 있는 잘 알려진 교과서적 구현을 읊고 있는 것일까요?

Specula 팀의 최근 연구는 "textbook modeling"과 충실한 시스템 표현 사이의 격차를를 드러내기 위해 설계된 자동화된 벤치마크인 SysMoBench를 소개합니다. 동시성 동기화 프리미티브부터 Etcd 및 ZooKeeper와 같은 복잡한 분산 프로토콜에 이르기까지 11개의 실제 시스템을 LLM으로 평가함으로써, 팀은 현재의 LLM이 형식적 명세를 작성하는 방식에서 나타나는 체계적인 실패를 밝혀냈습니다.

정답의 환상

Etcd의 Raft 구현에 대한 TLA+ 명세를 작성하도록 요청받았을 때, 선도적인 LLM들은 종종 구문 검사를 통과하고 TLC 모델 체커를 오류 없이 실행하는 코드를 생성합니다. 언뜻 보기에는 결과가 매우 세련되어 보입니다. 그러나 자세히 살펴보면, 해당 명세는 Etcd의 실제 구현에서 이루어진 특정 아키텍처 선택을 반영하기보다는 원래 Raft 논문의 부록을 그대로 반영하는 경우가 많습니다.

이것이 LLM 기반 모델링의 핵심 과제입니다. LLM은 온라인상의 거의 모든 TLA+ 예제를 보았기 때문에, "Raft spec"을 요청하면 추상화 메커니즘이 아닌 회상 메커니즘이 작동하게 됩니다. 시스템을 진정으로 모델링하려면, LLM은 복잡한 소스 코드에서 로직을 추상화하고 그 추상화를 올바른 형식적 모델로 변환할 수 있어야 합니다.

SysMoBench의 작동 방식

회상과 모델링을 구분하기 위해, SysMoBench는 4단계 평가 파이프라인을 채택합니다:

Syntax Phase: 명세가 컴파일되는지 확인합니다.
Runtime Phase: TLC 모델 체커가 명세 없이 충돌 없이 실행될 수 있는지 검증합니다.
Conformance Phase: 트레이스 검증을 사용하여 실제 코드의 실행 트레이스와 모델을 비교합니다.
Invariant Phase: 명세가 주요 안전성(safety) 및 활성성(liveness) 속성을 만족하는지 확인합니다.

대부분의 최첨단 LLM들은 구문 단계에서 100%에 가까운 점수를 받지만, 일치성(conformance) 및 불변성(invariant) 테스트 중에는 성능이 급격히 떨어집니다. 복잡한 분산 시스템의 경우, 가장 강력한 모델조차 전체 점수가 10%에서 50% 사이로 떨어지는 경우가 많습니다.

"교과서적 모델링"의 두 가지 패턴

연구에서는 LLM이 구현 세부 사항 대신 일반적인 템플릿에 의존하는 두 가지 반복적인 실패 모드를 식별했습니다:

1. 불가능한 상태의 허용

LLM은 종종 시스템의 실제 데이터 구조와 일치하지 않는 형식화 템플릿을 사용합니다. 예를 들어, ZooKeeper Fast Leader Election (FLE) 명세에서, Claude Sonnet은 서버의 recvset을 집합 합집합(set union)으로 처리하여 모든 투표를 증거로 축적할 수 있게 했습니다. 실제 ZooKeeper 코드에서는 이것이 송신자에 의해 키가 지정된 맵(map)이며, 이는 새로운 투표가 이전 투표를 덮어쓴다는 것을 의미합니다. 이러한 불일치는 명세가 실제 시스템이 결코 도달할 수 없는 상태에 진입하게 만듭니다.

2. 도달 가능한 상태의 삭제

반대로, LLM은 여러 구현 단계를 하나의 원자적 가드(atomic guard)로 병합하는 경우가 빈번합니다. 동일한 ZooKeeper 예제에서, LLM은 로컬 논리적 시계를 업데이트하고 메시지를 처리하는 행위를 하나의 단계로 융합했습니다. 실제 코드에서는 이 작업들이 순차적으로 일어납니다. 이들을 융합함으로써, LLM은 모든 선거 라운드에서 실제 시스템이 진입하는 상태를 삭제해 버렸습니다. 이로 인해 명세에서는 특정 전이(transition)가 불가능해집니다.

전이 검증: 세밀한 접근 방식

이러한 실패를 정확히 짚어내기 위해, SysMoBench는 Transition Validation을 활용합니다. 모듈 전체에 대해 이진법적인 합격/불합격 판정을 내리는 대신, 시스템은 실제 실행 트레이스를 수집하여 이를 "전이 윈도우"(pre-state, action, post-state)로 나눕니다.

각 윈도우는 TLC에 입력되어 명세의 액션이 실제로 시스템을 pre-state에서 post-state로 이동시킬 수 있는지 확인합니다. 이는 액션별 점수표를 제공하여, 개발자가 대략적인 총점 대신 정확히 어떤 특정 상태 전이가 실패하는지, 그리고 왜 실패하는지를 볼 수 있게 해줍니다.

더 넓은 의미와 해결되지 않은 과제

연구 결과는 LLM이 TLA+ 언어에는 능숙하지만, 특정 구현의 로직에는 어려움을 겪는다는 것을 시사합니다. 이는 형식적 방법론의 미래에 대해 더 넓은 논의를 불러일으켰습니다:

Coupled Verification: 일부는 구현과 검증을 결합하여 모델이 코드와 분리되는 것을 방지하는 Verus와 같은 접근 방식을 주장합니다.
Human Intent: 설계 프로세스를 자동화하는 것이 인간의 의제의도를도를 제거한다는 철학적 우려가 있습니다. 한 댓글 작성자는 LLM이 설계와 코드를 모두 생성한다면, "증명"에는 의미 있는 인간의 보장(assurance)이 부족할 수 있다고 지적했습니다.
Liveness Properties: 사용자들은 LLM이 안전성 속성(safety properties)에 비해 활성성 속성(liveness properties)을 다루는 데 특히 어려움을 겪는다는 점에 주목했습니다.

이러한 장애물에도 불구하고, Specula 팀은 저장소를 자율적으로 읽고 명세 작성 워크플로우를 주도할 수 있는 특화된 에이전트를 개발하고 있습니다. 그들의 특화된 에이전트인 Specula는 이미 현재 SysMoBench 작업에서 완전한 일치성 및 불변성 점수를 달성할할 수 있는 능력을 보여주었으며, 이는 앞으로의 길이 단순한 LLM 프롬프팅이 아닌 에이전트 워크플로우에 있음을 시사합니다.

결론

컴파일되는 TLA+ 모듈을 작성하는 것은 낮은 기준입니다. 해당 모듈을 실제 시스템의 실제 동작과 일치시키는 것이 진정한 과제입니다. 우리가 에이전트 기반 모델 체킹으로 나아가면서, focus는 구문에서 일치성으로 전환되어야 합니다. 목표는 Raft가 처럼 보이는 명세를 만드는 것이 아니라, 시스템 그 자체를 만드는 것입니다.n