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.

翻译：在多智能体系统中，推理智能体通过策略交互能够实现的目标是一项核心挑战。用于策略能力的逻辑（例如ATL）提供了严谨的方法，但其应用常常受到策略综合计算成本的制约。我们引入了一种神经符号框架，将大型语言模型集成到多智能体系统的模型检测流程中。该大型语言模型充当策略生成预言机，提出候选策略，然后由标准的多智能体系统模型检测器对这些策略进行形式化验证。这种“生成-验证”架构利用大型语言模型引导来导航庞大的组合策略空间，同时保持形式上的正确性：生成的策略仅在通过验证器认证后才被接受。我们在NatATL中实例化了该框架，用于有界策略推理，并引入了首个NatATL策略综合数据集，包含4211个实例。使用开源权重的Qwen3-32B模型进行的实验表明，我们的认证流程在策略综合结果上达到了92%的准确率。