Neural network verification mainly focuses on local robustness properties, which can be checked by bounding the image (set of outputs) of a given input set. However, often it is important to know whether a given property holds globally for the input domain, and if not then for what proportion of the input the property is true. To analyze such properties requires computing preimage abstractions of neural networks. In this work, we propose an efficient anytime algorithm for generating symbolic under-approximations of the preimage of any polyhedron output set for neural networks. Our algorithm combines a novel technique for cheaply computing polytope preimage under-approximations using linear relaxation, with a carefully-designed refinement procedure that iteratively partitions the input region into subregions using input and ReLU splitting in order to improve the approximation. Empirically, we validate the efficacy of our method across a range of domains, including a high-dimensional MNIST classification task beyond the reach of existing preimage computation methods. Finally, as use cases, we showcase the application to quantitative verification and robustness analysis. We present a sound and complete algorithm for the former, which exploits our disjoint union of polytopes representation to provide formal guarantees. For the latter, we find that our method can provide useful quantitative information even when standard verifiers cannot verify a robustness property.

翻译：神经网络验证主要关注局部鲁棒性属性，这可以通过界定给定输入集的像（输出集）来检验。然而，通常需要了解给定的属性在输入域上是否全局成立，若否则该属性在多大比例的输入上成立。分析此类属性需要对神经网络的原像进行抽象。本文提出了一种高效的任意时刻算法，用于生成神经网络任意多面体输出集原像的符号化下近似。该算法结合了一种利用线性松弛廉价计算多胞体原像下近似的新技术，以及精心设计的细化过程——通过输入分裂和ReLU分裂迭代划分输入区域为子区域以改进近似。我们在多个领域验证了该方法的有效性，包括现有原像计算方法无法处理的高维MNIST分类任务。最后，作为应用案例，我们展示了该方法在定量验证和鲁棒性分析中的应用。前者我们提出了一个完备且可靠的算法，通过利用多胞体不交并表示提供形式化保证；后者发现即使标准验证器无法验证鲁棒性属性时，我们的方法仍能提供有用的定量信息。