For many multiagent control problems, neural networks (NNs) have enabled promising new capabilities. However, many of these systems lack formal guarantees (e.g., collision avoidance, robustness), which prevents leveraging these advances in safety-critical settings. While there is recent work on formal verification of NN-controlled systems, most existing techniques cannot handle scenarios with more than one agent. To address this research gap, this paper presents a backward reachability-based approach for verifying the collision avoidance properties of Multi-Agent Neural Feedback Loops (MA-NFLs). Given the dynamics models and trained control policies of each agent, the proposed algorithm computes relative backprojection sets by (simultaneously) solving a series of Mixed Integer Linear Programs (MILPs) offline for each pair of agents. We account for state measurement uncertainties, making it well aligned with real-world scenarios. Using those results, the agents can quickly check for collision avoidance online by solving low-dimensional Linear Programs (LPs). We demonstrate the proposed algorithm can verify collision-free properties of a MA-NFL with agents trained to imitate a collision avoidance algorithm (Reciprocal Velocity Obstacles). We further demonstrate the computational scalability of the approach on systems with up to 10 agents.

翻译：对于许多多智能体控制问题，神经网络已赋予其令人期待的新能力。然而，这些系统大多缺乏形式化保证（如避碰、鲁棒性），这阻碍了在安全关键场景中运用这些技术突破。尽管近期出现了针对神经网络控制系统的形式化验证研究，但现有方法大多无法处理涉及多个智能体的场景。为填补这一研究空白，本文提出一种基于后向可达性的方法，用于验证多智能体神经反馈回路（MA-NFL）的避碰性能。在已知每个智能体的动力学模型及训练好的控制策略前提下，所提算法通过离线（同步）求解每对智能体间的一系列混合整数线性规划（MILP），计算相对后向投影集。我们考虑了状态测量不确定性，使该方法更贴合实际场景。基于计算结果，智能体可通过在线求解低维线性规划（LP）快速完成避碰检查。我们验证了所提算法能对经训练以模仿避碰算法（互惠速度障碍物）运行的多智能体神经反馈回路完成无碰撞属性验证，并进一步展示了该方法在包含最多10个智能体的系统中的计算可扩展性。