A toolbox for fast interval arithmetic in numpy with an application to formal verification of neural network controlled systems
A. Harapanahalli, S. Jafarpour, S. Coogan
ICML workshop on Formal Verification of Machine Learning (WFVML 2023), 2023
Abstract
In this paper, we present a toolbox for interval analysis in numpy, with an application to formal verification of neural network controlled systems. Using the notion of natural inclusion functions, we systematically construct interval bounds for a general class of mappings. The toolbox offers efficient computation of natural inclusion functions using compiled C code, as well as a familiar inter- face in numpy with its canonical features, such as n-dimensional arrays, matrix/vector operations, and vectorization. We then use this toolbox in for- mal verification of dynamical systems with neural network controllers, through the composition of their inclusion functions.