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.

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