A Neuro-Symbolic Approach to Strategy Synthesis for Strategic Logics

📄 arXiv: 2606.17962v1 📥 PDF

作者: Marco Aruta, Vadim Malvone, Aniello Murano, Domenico Parente, Luca Rizzuti

分类: cs.MA, cs.AI

发布日期: 2026-06-16

💡 一句话要点

提出神经符号方法以解决多智能体系统中的策略合成问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 多智能体系统 策略合成 神经符号方法 模型检查 大型语言模型 博弈论 自动化决策

📋 核心要点

  1. 现有的多智能体系统中，策略合成的计算成本高，限制了战略能力逻辑的应用。
  2. 本文提出的神经符号框架通过将大型语言模型集成到模型检查中，生成候选策略并进行验证。
  3. 实验结果显示，使用Qwen3-32B模型的认证管道在策略合成上达到了92%的准确率，显著提升了效率。

📝 摘要（中文）

在多智能体系统（MAS）中，推理代理通过战略互动可以实现的目标是一个核心挑战。尽管战略能力的逻辑（如ATL）提供了严格的方法，但策略合成的计算成本常常阻碍其应用。本文提出了一种神经符号框架，将大型语言模型（LLM）集成到MAS的模型检查流程中。LLM作为策略生成的oracle，提出候选策略，然后由标准的MAS模型检查器进行正式验证。这种生成与认证的架构利用LLM的指导来导航大型组合策略空间，同时保持形式上的健全性：只有在验证者认证后，生成的策略才会被接受。我们为NatATL中的有界战略推理实例化了该框架，并引入了首个NatATL策略合成数据集，包含4211个实例。实验表明，我们的认证管道在策略合成结果上达到了92%的准确率。

🔬 方法详解

问题定义：本文旨在解决多智能体系统中策略合成的高计算成本问题。现有方法在处理复杂的战略能力逻辑时，往往面临效率低下的挑战。

核心思路：论文提出了一种神经符号框架，利用大型语言模型（LLM）作为策略生成的oracle，生成候选策略并通过标准模型检查器进行验证，从而提高策略合成的效率。

技术框架：整体架构包括两个主要模块：首先，LLM生成候选策略；其次，模型检查器对生成的策略进行形式验证。生成的策略仅在通过验证后被接受，确保了结果的形式健全性。

关键创新：该研究的主要创新在于将神经网络与符号逻辑结合，形成生成与认证的架构，显著降低了策略合成的计算复杂度，与传统方法相比具有本质区别。

关键设计：在实验中，使用了开放权重的Qwen3-32B模型，设置了特定的参数和损失函数，以优化策略生成的质量和验证的准确性。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果显示，使用Qwen3-32B模型的认证管道在策略合成结果上达到了92%的准确率，显著高于传统方法。这一成果表明，神经符号方法在处理复杂策略合成任务中的有效性和潜力。

🎯 应用场景

该研究的潜在应用领域包括多智能体系统中的自动化决策、博弈论分析和智能代理的策略优化。通过提高策略合成的效率，该方法可以在复杂环境中实现更高效的智能体协作，具有重要的实际价值和未来影响。

📄 摘要（原文）

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.