A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems

TL;DR

This paper introduces a numpy-compatible toolbox for fast interval arithmetic, enabling efficient formal verification of neural network controlled systems through systematic construction and composition of interval bounds.

Contribution

The authors develop a numpy-based interval analysis toolbox with C-accelerated computations, facilitating formal verification of neural network-controlled dynamical systems.

Findings

Efficient interval bounds computation using compiled C code.

Successful application to formal verification of neural network controllers.

Enhanced numpy interface for interval analysis tasks.

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 interface in numpy with its canonical features, such as n-dimensional arrays, matrix/vector operations, and vectorization. We then use this toolbox in formal verification of dynamical systems with neural network controllers, through the composition of their inclusion functions.