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.

翻译：神经网络验证主要关注局部鲁棒性。然而，通常需要了解某个性质是否在全局输入域上成立，若不成立则该性质对多少比例的输入成立。虽然精确前像生成可构建神经网络等价表示以辅助此类（定量）全局鲁棒性验证，但该方法在大规模场景下难以处理。本文提出一种基于线性松弛的高效实用任意时间算法，用于生成神经网络前像的符号化欠逼近。该算法通过将输入区域划分为子区域并收紧神经网络松弛界，迭代最小化体积逼近误差。进一步采用采样和可微体积近似方法，优先拆分关键区域并优化松弛参数，从而加速收敛并生成更紧凑的欠逼近。评估结果表明，本方法生成前像逼近的速度显著快于精确方法，且可扩展至无法进行精确前像生成的神经网络控制器。我们还展示了该方法在定量全局验证中的应用。