验证带记忆的多智能体神经系统，首次实现无界LTL性质检查。
LTL Verification of Memoryful Neural Agents
- 基于约束求解与归纳推理，将复杂逻辑验证转为可计算问题。
- 在Gymnasium和PettingZoo环境中首次完成无界LTL验证，提速超十倍。
- 适合从事多智能体系统形式化验证的研究者与工程师。
我们提出一个框架，用于对带记忆的神经多智能体系统（MN-MAS）进行全范围线性时序逻辑（LTL）性质验证。在MN-MAS中，智能体与非确定性、部分可观测环境交互，典型例子包括前馈、循环神经网络或多状态空间模型。不同于以往方法，本工作支持有界与无界LTL规格的验证。我们利用成熟的有界模型检验技术，如环路搜索与不变式合成，将验证问题转化为约束求解任务。为求解这些约束，我们开发了基于边界传播、混合整数线性规划和自适应分割的高效方法。我们在Gymnasium和PettingZoo库中的单智能体与多智能体环境中评估了算法有效性，首次实现了无界规格的验证，并相较现有最优方法将有界规格的验证时间缩短了一个数量级。
原文摘要 · Abstract (English)
We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable environment. Examples of MN-MAS include multi-agent systems based on feed-forward and recurrent neural networks or state-space models. Different from previous approaches, we support the verification of both bounded and unbounded LTL specifications. We leverage well-established bounded model checking techniques, including lasso search and invariant synthesis, to reduce the verification problem to that of constraint solving. To solve these constraints, we develop efficient methods based on bound propagation, mixed-integer linear programming, and adaptive splitting. We evaluate the effectiveness of our algorithms in single and multi-agent environments from the Gymnasium and PettingZoo libraries, verifying unbounded specifications for the first time and improving the verification time for bounded specifications by an order of magnitude compared to the SoA.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。