Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performances on challenging control problems. However, the potential adoption of NN controllers in real-life applications also gives rise to a growing concern over the safety of these neural-network controlled systems (NNCSs), especially when used in safety-critical applications. In this work, we present POLAR-Express, an efficient and precise formal reachability analysis tool for verifying the safety of NNCSs. POLAR-Express uses Taylor model arithmetic to propagate Taylor models (TMs) across a neural network layer-by-layer to compute an overapproximation of the neural-network function. It can be applied to analyze any feed-forward neural network with continuous activation functions. We also present a novel approach to propagate TMs more efficiently and precisely across ReLU activation functions. In addition, POLAR-Express provides parallel computation support for the layer-by-layer propagation of TMs, thus significantly improving the efficiency and scalability over its earlier prototype POLAR. Across the comparison with six other state-of-the-art tools on a diverse set of benchmarks, POLAR-Express achieves the best verification efficiency and tightness in the reachable set analysis.

翻译：神经网络（NN）作为控制器已在具有挑战性的控制问题上展现出令人瞩目的实证表现。然而，神经网络控制器在实际应用中的潜在推广也引发了对这些神经网络控制系统（NNCSs）安全性的日益关注，特别是在安全关键型应用场景中。本研究提出POLAR-Express，一种用于验证NNCSs安全性的高效精确形式可达性分析工具。POLAR-Express采用泰勒模型算法，逐层传播泰勒模型（TMs）通过神经网络，从而计算神经网络函数的超近似。该方法可应用于分析任何具有连续激活函数的前馈神经网络。我们还提出了一种新颖方法，可在ReLU激活函数上更高效、更精确地传播TMs。此外，POLAR-Express为TMs的逐层传播提供并行计算支持，从而显著提升其早期原型POLAR的效率和可扩展性。在与六种其他最新工具在多样化基准测试上的对比中，POLAR-Express在可达集分析中实现了最优的验证效率和紧致性。