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.

翻译：本文提出了一种在numpy中实现区间分析的工具箱，并将其应用于神经网络控制系统的形式化验证。利用自然包含函数的概念，我们系统性地构建了一类通用映射的区间边界。该工具箱通过编译的C代码高效计算自然包含函数，同时提供与numpy一致且具有其典型特性（如n维数组、矩阵/向量运算及向量化）的熟悉接口。我们进一步通过组合包含函数，将本工具箱应用于含神经网络控制器的动力系统形式化验证。