We propose POLAR, a \textbf{pol}ynomial \textbf{ar}ithmetic framework that leverages polynomial overapproximations with interval remainders for bounded-time reachability analysis of neural network-controlled systems (NNCSs). Compared with existing arithmetic approaches that use standard Taylor models, our framework uses a novel approach to iteratively overapproximate the neuron output ranges layer-by-layer with a combination of Bernstein polynomial interpolation for continuous activation functions and Taylor model arithmetic for the other operations. This approach can overcome the main drawback in the standard Taylor model arithmetic, i.e. its inability to handle functions that cannot be well approximated by Taylor polynomials, and significantly improve the accuracy and efficiency of reachable states computation for NNCSs. To further tighten the overapproximation, our method keeps the Taylor model remainders symbolic under the linear mappings when estimating the output range of a neural network. We show that POLAR can be seamlessly integrated with existing Taylor model flowpipe construction techniques, and demonstrate that POLAR significantly outperforms the current state-of-the-art techniques on a suite of benchmarks.

翻译：我们建议采用POLAR, 这是一种利用多盘超位和间隔剩余时间对神经网络控制系统进行封闭时间可达性分析的POLAR框架。 与使用标准的泰勒模型的现有算术方法相比,我们的框架采用一种新颖的方法,迭代地超近神经输出范围层,结合伯恩斯坦的连续激活功能的多元间插和其他操作的泰勒模型算术。 这种方法可以克服标准泰勒模型算术中的主要缺陷, 即它无法处理泰勒多盘多盘无法完全接近的功能, 并且大大提高了NNCNS计算可达状态的准确性和效率。 为了进一步强化过度使用, 我们的方法在估计神经网络的产出范围时, 将泰勒模型的剩余部分保留在线性绘图之下。 我们表明, POLAR可以与现有的泰勒模型模型流动计算技术紧密结合, 并展示当前AR 系统基准的状态技术大大超出。