战略逻辑策略综合的神经符号方法

推理智能体通过战略交互可以实现什么是多智能体系统（MAS）的核心挑战。战略能力逻辑（例如 ATL）提供了严格的方法，但它们的采用常常受到策略综合的计算成本的阻碍。我们引入了一个神经符号框架，它将 大语言模型 (LLM) 集成到 MAS 的模型检查管道中。 LLM 充当策略生成预言机，提出候选策略，然后由标准 MAS 模型检查器进行正式验证。这种生成和认证架构使用 LLM 指导来导航大型组合策略空间，同时保持形式健全性：仅在经过验证者认证时才接受生成的策略。我们在 NatATL 中实例化了有界策略推理框架，并引入了第一个 NatATL 策略综合数据集，其中包含 4211 个实例。开放权重 Qwen3-32B 模型的实验表明，我们经过认证的流程在策略综合结果方面实现了 92% 的准确率。