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，一种用于验证神经网络控制系统的安全性的高效而精确的正式可达性分析工具。该工具使用泰勒模型算术来跨越神经网络层层传播泰勒模型从而计算神经网络函数的近似值，能够分析任何具有连续激活函数的前馈神经网络。文章中还提出了一种在 ReLU 激活函数上更加高效和精确传播泰勒模型的新方法。在多个数据集上的对比实验表明，POLAR-Express 在可达性分析中取得了最佳的效率和可靠性。