用大模型生成策略，再用形式化方法验证，提升多智能体系统策略合成效率。
A Neuro-Symbolic Approach to Strategy Synthesis for Strategic Logics
- 结合大模型与形式化验证，构建生成-认证的策略合成框架。
- 在4211个实例上达到92%准确率，显著提升合成效率。
- 适合对多智能体系统形式化推理感兴趣的开发者与研究者。
多智能体系统中，推理智能体通过战略互动能达成什么目标是核心挑战。诸如ATL等战略能力逻辑提供了严谨方法，但策略合成的计算成本常阻碍其应用。本文提出一种神经符号框架，将大语言模型（LLMs）融入多智能体系统模型检验流程。LLM作为策略生成预言机，提出候选策略，再由标准的多智能体系统模型检查器进行形式化验证。该生成-认证架构利用LLM引导探索大规模组合策略空间，同时保持形式化正确性：仅当被验证器认证后，生成策略才被接受。我们针对有界战略推理中的NatATL进行了实例化，并构建了首个NatATL策略合成数据集，包含4211个实例。实验使用开源权重的Qwen3-32B模型，表明该认证管道在策略合成结果上达到92%的准确率。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。