A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems
A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems
复制标题
DOI：
10.48550/arxiv.2306.15340
复制
发表时间：
2023-06
期刊：
影响因子：
--
通讯作者：
Akash Harapanahalli;Saber Jafarpour;S. Coogan
中科院分区：
文献类型：
--
作者：
Akash Harapanahalli;Saber Jafarpour;S. Coogan
在本文中，我们提出了一个 numpy 区间分析工具箱，并应用于神经网络控制系统的形式验证。使用自然包含函数的概念，我们系统地构建一般类映射的区间界限。该工具箱使用编译的 C 代码以及 numpy 中熟悉的接口及其规范功能（例如 n 维数组、矩阵/向量运算和向量化）提供自然包含函数的高效计算。然后，我们通过包含函数的组合，使用该工具箱对具有神经网络控制器的动力系统进行形式验证。
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.