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.
翻译:神经网络 (NNs) 在解决复杂控制问题时的表现是惊人的,它们被广泛应用于控制领域。但将神经网络控制器应用于实际系统的发展,也引起了人们对神经网络控制系统 (NNCSs) 安全性的担忧,尤其是在安全关键应用中的使用。本文提出了 POLAR-Express 工具,它是一种高效而精确的形式可达性分析工具,用于验证 NNCSs 的安全性。 POLAR-Express 利用 Taylor 模型算术来逐层通过神经网络传播 Taylor 模型 (TMs),从而计算出神经网络函数的上估计。它适用于分析任何使用连续激活函数的前馈神经网络。我们还提出了一种新的方法,用于在 ReLU 激活函数中更高效和准确地传播 TMs。此外,POLAR-Express 提供了对层与层之间 TMs 传播的并行计算支持,有效提高了效率和可扩展性,超过了其早期原型工具 POLAR。在六个不同基准测试集的比较中,POLAR-Express 实现了最佳的可达性分析效率和TMs精度。