Neural network verification mainly focuses on local robustness properties. However, often it is important to know whether a given property holds globally for the whole input domain, and if not then for what proportion of the input the property is true. While exact preimage generation can construct an equivalent representation of neural networks that can aid such (quantitative) global robustness verification, it is intractable at scale. In this work, we propose an efficient and practical anytime algorithm for generating symbolic under-approximations of the preimage of neural networks based on linear relaxation. Our algorithm iteratively minimizes the volume approximation error by partitioning the input region into subregions, where the neural network relaxation bounds become tighter. We further employ sampling and differentiable approximations to the volume in order to prioritize regions to split and optimize the parameters of the relaxation, leading to faster improvement and more compact under-approximations. Evaluation results demonstrate that our approach is able to generate preimage approximations significantly faster than exact methods and scales to neural network controllers for which exact preimage generation is intractable. We also demonstrate an application of our approach to quantitative global verification.

翻译：神经网络验证主要关注局部鲁棒性质，然而在许多场景下，需要判断某个性质是否对整个输入域全局成立，若不成立则需确定该性质在多大比例的输入上成立。尽管精确预像生成可以构建神经网络的等价表示以辅助此类（定量）全局鲁棒性验证，但该方法在大规模网络中难以实现。本研究提出一种基于线性松弛的高效实用任意时间算法，用于生成神经网络预像的符号化下近似。该算法通过将输入区域分割为子区域以收紧神经网络松弛边界，迭代最小化体积近似误差。我们进一步采用采样技术与体积可微近似，对分割区域优先级进行优化并调节松弛参数，从而加速收敛并生成更紧凑的下近似。评估结果表明，与精确方法相比，本方法能显著更快地生成预像近似，并可扩展至精确预像生成不可行的神经网络控制器。此外，我们展示了该方法在定量全局验证中的应用。