전략적 논리를 위한 전략 합성의 신경-기호적 접근 방식

에이전트가 전략적 상호작용을 통해 무엇을 달성할 수 있는지에 대해 추론하는 것은 다중 에이전트 시스템 (Multi-Agent Systems, MAS)의 핵심 과제입니다. ATL과 같은 전략적 능력에 대한 논리(Logics for strategic ability)는 엄격한 방법론을 제공하지만, 전략 합성 (strategy synthesis)의 계산 비용으로 인해 도입이 저해되는 경우가 많습니다. 우리는 MAS를 위한 모델 검사 (model-checking) 파이프라인에 대규모 언어 모델 (Large Language Models, LLMs)을 통합하는 신경-기호적 (neuro-symbolic) 프레임워크를 소개합니다. LLM은 전략 생성 오라클 (strategy-generation oracle) 역할을 수행하여 후보 전략을 제안하며, 제안된 전략은 표준 MAS 모델 검사기에 의해 공식적으로 검증됩니다. 이러한 생성 및 인증 (generate-and-certify) 아키텍처는 LLM의 가이드를 사용하여 방대한 조합론적 전략 공간을 탐색하는 동시에 형식적 건전성 (formal soundness)을 유지합니다. 즉, 생성된 전략은 검증기에 의해 인증될 때만 수락됩니다. 우리는 NatATL에서의 유계 전략 추론 (bounded strategic reasoning)을 위해 이 프레임워크를 구현하였으며, 4,211개의 인스턴스로 구성된 최초의 NatATL 전략 합성 데이터셋을 도입합니다. 오픈 웨이트 (open-weight) 모델인 Qwen3-32B를 사용한 실험 결과, 우리의 인증 파이프라인이 전략 합성 결과에서 92%의 정확도를 달성함을 보여줍니다.