Provable Preimage Under-Approximation for Neural Networks (Full Version)
Xiyue Zhang, Benjie Wang, Marta Kwiatkowska
TL;DR
The paper tackles the challenge of verifying global properties of neural networks by computing provable, under-approximated preimages of polyhedral output sets. It introduces an anytime method that builds a disjoint union of polytopes ($\text{DUP}$) as a sound under-approximation of the restricted preimage $f^{-1}_{\mathcal{C}}(O)$ by backwardly propagating LiRPA bounds and progressively refining the input region via input and ReLU splitting, guided by a differentiable volume-optimization objective. The approach supports both under- and over-approximations, provides soundness/completeness guarantees for quantitative verification on piecewise-linear networks, and demonstrates substantial efficiency gains and scalability to high-dimensional tasks (e.g., MNIST) for applications in quantitative verification and robustness analysis. By enabling exact volume computations over the resulting polytope unions, the method supports precise probabilistic guarantees about the proportion of inputs satisfying a property, with practical impact on safety-critical AI systems.
Abstract
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.