A Neuro-Symbolic Approach to Strategy Synthesis for Strategic Logics
For multi-agent systems researchers, this work reduces the computational cost of strategy synthesis by combining LLM guidance with formal verification, though it is incremental as it applies existing LLM capabilities to a known bottleneck.
The paper introduces a neuro-symbolic framework that uses LLMs as strategy-generation oracles in a generate-and-certify pipeline for ATL-based strategy synthesis, achieving 92% accuracy on a new NatATL dataset of 4211 instances.
Reasoning about what agents can achieve through strategic interaction is a core challenge in Multi-Agent Systems (MAS). Logics for strategic ability, such as ATL, provide rigorous methods, but their adoption is often hindered by the computational cost of strategy synthesis. We introduce a neuro-symbolic framework that integrates large language models (LLMs) into the model-checking pipeline for MAS. The LLM acts as a strategy-generation oracle, proposing candidate strategies that are then formally validated by a standard MAS model checker. This generate-and-certify architecture uses LLM guidance to navigate large combinatorial strategy spaces while preserving formal soundness: generated strategies are accepted only when certified by the verifier. We instantiate the framework for bounded strategic reasoning in NatATL and introduce the first NatATL strategy-synthesis dataset, consisting of 4211 instances. Experiments with an open-weight Qwen3-32B model show that our certified pipeline achieves 92\% accuracy on strategy-synthesis outcomes.