IC3 및 Large Language Models (LLMs)를 통한 분산 프로토콜용 귀납적 불변량 합성

분산 프로토콜 (Distributed protocols)은 정확하게 검증하기가 매우 어려운 것으로 악명이 높습니다. 안전성 (safety)을 증명하려면 원하는 속성을 함의하면서 동시에 모든 프로토콜 전이 (protocol transition)에 의해 보존되는 귀납적 불변량 (inductive invariants)이 일반적으로 필요합니다. 하지만 이러한 불변량을 추론하는 것은 여전히 주요한 병목 구간으로 남아 있습니다. 기존의 접근 방식들은 프로토콜 모델을 1차 논리 (first-order logic)의 결정 가능한 파편 (decidable fragment)으로 제한하거나, 전문가가 직접 제작한 템플릿 (templates)을 요구합니다.

본 논문에서는 Large Language Models (LLMs)의 도움을 받아 TLA+ 상태에 대해 IC3 스타일의 프로세스를 실행함으로써 귀납적 불변량을 합성하는 신경-기호 프레임워크 (neuro-symbolic framework)인 IC3Syn을 제시합니다. 거시적으로 IC3Syn은 불변량 합성을 집중적인 차단 작업 (blocking tasks)으로 분해하는 기호적 IC3 컨트롤러 (symbolic IC3 controller)와, TLA+ 명세 (specifications)에 대해 IC3 단독으로는 부족한 프로토콜 수준의 추론을 제공하는 LLM을 결합합니다. 이러한 통합은 논리적 제한을 가하거나 수동 템플릿을 요구하지 않으면서도, 규율 있으면서도 유연한 불변량 탐색을 가능하게 합니다.

우리는 합의 (consensus), 재구성 (reconfiguration), 클라이언트-서버 시스템을 아우르는 29개의 분산 프로토콜에 대해 IC3Syn을 평가하고, 이를 Endive, IC3PO, SWISS 및 DistAI와 비교합니다. IC3Syn은 비교 대상인 어떤 도구도 해결책을 보고하지 못한 산업 규모의 Raft 기반 재구성 프로토콜인 MongoLoglessDynamicRaft (MLDR)와 하나의 복잡한 Paxos 변형을 포함하여, 29개 프로토콜 모두에 대해 후보 불변량을 발견합니다. 각 사례에서 유한한 인스턴스 (finite instances) 상에서 합성된 불변량은 TLAPS를 통해 전체 무한 프로토콜 (unbounded protocol)에 대해 귀납적임이 입증되었으며, 이를 통해 안전성을 확립했습니다.