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 solving a series of
Mixed Integer Linear Programs (MILPs) offline for each pair of agents. Our
pair-wise approach is parallelizable and thus scales well with increasing
number of agents, and 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）的碰撞避免属性，并展示该方法在 10 个智能体系统上的计算可扩展性。