POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems

Understand

We present POLAR, a polynomial arithmetic-based framework for efficient bounded-time reachability analysis of neural-network controlled systems (NNCSs).

• Existing approaches that leverage the standard Taylor Model (TM) arithmetic for approximating the neural-network controller cannot deal with non-differentiable activation functions and suffer from rapid explosion of the remainder when propagating the TMs.
• POLAR overcomes these shortcomings by integrating TM arithmetic with \textbf{Bernstein B{\'e}zier Form} and \textbf{symbolic remainder}.
• The former enables TM propagation across non-differentiable activation functions and local refinement of TMs, and the latter reduces error accumulation in the TM remainder for linear mappings in the network.