用LLM帮MAS做策略合成，再加形式验证保证正确性，Qwen3-32B跑出92%准确率，挺实在的方法。
研究人员提出一个神经符号框架，将大语言模型(LLM)集成到多智能体系统(MAS)模型检查流程中。LLM作为策略生成预言机，产生的候选策略由标准MAS模型检查器进行形式验证。该生成-认证架构利用LLM引导搜索大型组合策略空间，同时保持形式正确性。框架在NatATL逻辑中实例化，创建了首个包含4211个实例的NatATL策略合成数据集。使用开源Qwen3-32B模型时，认证管道的策略合成准确率达92%。
A Neuro-Symbolic Approach to Strategy Synthesis for Strategic Logics
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.