기술 요약: SYSMOBENCH

문제 정의

형식 모델(Formal models)은 대규모의 복잡한 컴퓨터 시스템, 특히 분산 및 병행 컴퓨팅 도메인에서 시스템의 정확성을 명세하고 검증하는 데 매우 중요합니다. 그러나 이러한 모델을 생성하는 작업은 저수준 시스템 코드를 엄격한 수학적 명세로 추상화하기 위해 상당한 전문가의 노력을 필요로 하므로, 비용이 매우 많이 드는 것으로 악명이 높습니다. 최근 생성형 AI(LLM 및 에이전트 기술)의 발전이 함수 수준의 명세(예: 전제 조건 및 사후 조건)를 생성하는 데 유망함을 보여주었으나, AI가 완전한 실제 시스템을 효과적으로 모델링할 수 있는지 여부는 여전히 불분clear합니다. 기존의 벤치마크들은 주로 작은 코드 조각이나 논리 퍼즐을 대상으로 하며, 시스템 설계를 추상화하고, 결함 상황에서의 안전성(safety) 및 활성(liveness)을 추론하며, 프로덕션급 아티팩트의 규모를 다루는 복잡성을 해결하는 데는 한계가 있습니다.

방법론

저자들은 생성형 AI가 복잡한 실제 시스템을 형식적으로 모델링하는 능력을 평가하기 위해 설계된 벤치마크인 SYSMOBENCH를 제시합니다. 이 프레임워크는 운영 체제나 클라우드 서비스와 같은 핵심 인프라의 근간이 되는 병행 및 분산 시스템에 초점을 맞춥니다.

핵심 구성 요소

1. 태스크 정식화(Task Formulation): 이 벤치마크는 AI 에이전트에게 실제 시스템 아티팩트로부터 (특히 시스템 명세 언어의 표준인 **TLA+**를 사용하여) 형식적인 시스템 모델을 생성하도록 과제를 부여합니다. 입력값에는 소스 코드, 문서, 런타임 트레이스가 포함됩니다. 출력값은 불필요한 구현 세부 사항은 제외하면서 필수적인 동작 특성과 상태 전이를 포착해야 합니다.
2. 시스템 아티팩트(System Artifacts): 현재 이 벤치마크는 단순한 동기화 프리미티브(Asterinas OS의 Spinlock, Mutex, Ringbuffer)부터 복잡한 분산 프로토콜(Etcd Raft, Redis Raft, ZooKeeper FLE, Xline CURP) 및 컴파일러 생성 시스템(PGo)에 이르기까지 11개의 다양한 아티팩트를 포함합니다.
3. 자동화된 평가 지표: 본 연구의 주요 기여는 취약한 인간 비교나 "LLM-as-a-judge" 방식에 의존하지 않고 모델의 품질을 평가하기 위한 자동화된 정량적 지표를 개발한 것입니다. 지표는 다음과 같습니다:
   • 구문 정확성(Syntax Correctness): SANY 구문 분석기를 사용하여 검증합니다. 부분적인 정확성을 처리하기 위해 가중치 점수 체계(전체 모델 vs. 액션별)를 채택합니다.
   • 런타임 정확성(Runtime Correctness): 모델의 액션 중 오류 없이 실행 가능한 비율을 측정하며, 이는 논리적 자기 일관성(logical self-consistency)의 대리 지표 역할을 합니다.
   • 적합성(Conformance): 트레이스 검증을 통해 평가됩니다. 여기서 실행 트레이스는 계측된 시스템 코드로부터 추출되며, 생성된 모델의 상태 공간(state space)과 대조됩니다. 이 과정에서는 명칭 불일치를 처리하기 위해 LLM을 사용하여 모델 요소와 코드 요소를 매핑합니다.
   • 불변량 정확성(Invariant Correctness): 모델이 시스템 특유의 안전성(safety) 및 활성(liveness) 속성을 만족하는지 평가합니다. 불변량 템플릿은 LLM을 통해 모델별 TLA+ 공식으로 구체화된 후 모델 체킹을 통해 검증됩니다.

평가 에이전트

본 연구는 네 가지 최첨단 LLM(Claude-Sonnet-4, GPT-5, Gemini-2.5-Pro, DeepSeek-R1)을 기반으로 하는 세 가지 별도의 에이전트 설계를 평가합니다:

• 기본 모델링 에이전트(Basic Modeling Agent): 소스 코드와 태스크 요구사항을 LLM에 직접 프롬프트로 제공합니다.
• 코드 번역 에이전트(Code Translation Agent): 시스템 코드를 문장 단위로 TLA+로 번역한 후 제어 흐름을 구성합니다.
• 트레이스 학습 에이전트(Trace Learning Agent): 코드 입력 없이 오직 런타임 트레이스로부터 시스템 모델을 추론합니다.

주요 결과

평가 결과, 복잡한 시스템 모델링에 대한 현재 AI 역량의 상당한 한계가 드러났습니다:

• 확장성 격차(Scalability Gap): AI 에이전트는 작고 단순한 아티팩트(예: Asterinas Spinlock)에서는 구문, 런타임, 적합성 점수에서 높은 점수를 얻으며 우수한 성능을 보입니다. 그러나 Etcd Raft와 같이 크고 복잡한 시스템에서는 성능이 급격히 저하됩니다. 예를 들어, Etcd Raft의 경우 가장 성능이 좋은 에이전트(코드 번역을 사용하는 Claude-Sonnet-4)조차 적합성 15.38%, 불변량 정확성 92.31%만을 달성했으며, 다른 에이전트들은 구문이나 런타임 체크를 통과하는 데 완전히 실패했습니다.
• 추상화의 어려움(Abstraction Challenges): 복잡한 시스템에서의 주요 실패 모드는 코드의 장황함(verbosity) 처리, 복잡한 프로토콜 로직(예: Raft 순서 지정) 이해, 그리고 중첩된 데이터 구조(예: 분산 로그)를 올바르게 추상화하는 능력의 부족입니다.
• 에이전트 성능: 코드 번역 에이전트가 복잡한 시스템에서 기본 모델링 에이전트보다 일반적으로 더 나은 성능을 보였으며, 이는 LLM의 코드 번역 능력을 활용하는 것이 로직의 환각(hallucination)을 방지하는 데 도움이 됨을 시사합니다. 트레이스 학습 에이전트는 전반적으로 저조한 성적을 거두었으며, 종종 컴파일 및 런타임 체크에 실패했습니다. 이는 트레이스로부터 시스템 모델을 추론하는 것이 소스 코드를 처리하는 것보다 현재 LLM에게 더 어렵다는 것을 나타냅니다.
• 오류 분석: 구문 오류는 특히 수학적 기호와 연산자 오용에서 빈번하게 발생합니다. 런타임 오류는 주로 일관되지 않은 설정이나 TLA+ 데이터 구조에 대한 오해에서 비롯됩니다. 주목할 점은, LLM이 **활성 속성(liveness properties)**에 대해 크게 고전한다는 것입니다. 불변량 위반 중 41.9%가 활성 관련이었던 반면 안전성 관련은 8.3%에 불과했는데, 이는 시간적 추론(temporal reasoning)의 약점을 강조합니다.
• 질적 유용성(Qualitative Utility): 정량적 한계에도 불구하고, AI가 생성한 모델은 다섯 가지 서로 다른 시스템에서 알려진 버그를 재현하는 데 성공하여 부분적 정확성 검증에 대한 실질적인 유용성을 입증했습니다.

의의 및 주장

저자들은 SYSMOBENCH를 "코드 지능(code intelligence)"에서 "시스템 지능(system intelligence)"으로 진화시키기 위한 기초적인 단계로 규정합니다.

• 현실적인 벤치마킹: 본 논문은 AI가 코딩 작업에는 유망함을 보이지만, 현재로서는 형식 검증에 필요한 대규모의 복잡한 시스템을 이해하고, 추상화하고, 명세하는 능력은 부족하다고 주장합니다.
• 자동화된 평가: 구문, 런타임, 적합성 및 불변량에 대한 자동화된 지표를 구축함으로써, SYSMOBENCH는 작은 프로그램이나 논리 퍼즐에 집중하는 기존 벤치마크의 한계를 넘어 이 분야의 발전을 측정할 수 있는 확장 가능하고 객관적인 방법을 제공합니다.
• 미래 방향: 저자들은 SYSMOBENCH를 혁신적인 AI 접근 방식을 촉발하는 매개체로 보고 있습니다. 이 벤치마크는 확장 가능하며(Alloy 및 PAT 지원), 아티팩트 컬렉션을 적극적으로 확장하고 있습니다. 저자들은 목표가 단순히 코드를 생성하는 것이 아니라, 소프트웨어 엔지니어링에서의 SWE-bench와 유사하게 AI가 안전 필수적인 실제 시스템의 형식 검증을 도울 수 있도록 하는 것이라고 강조합니다.

결론적으로, 현재의 LLM은 복잡한 시스템을 모델링하는 데 한계가 있지만, 이 프레임워크는 개선 사항을 추적하고 더욱 유능한 형식 시스템 모델링 AI 에이전트 개발을 가이드할 수 있는 필요한 도구를 제공합니다.