PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks

TL;DR

PREMAP introduces a unifying framework for neural network preimage approximation, enabling efficient verification of input sets satisfying output properties, with significant improvements in scalability and robustness analysis.

Contribution

It provides a general, scalable preimage abstraction framework using linear relaxations and iterative refinement, unifying verification approaches for neural networks.

Findings

Achieves rapid approximation improvements with heuristics.

Demonstrates scalability to high-dimensional image classification.

Provides sound algorithms for quantitative verification.

Abstract

Most methods for neural network verification focus on bounding the image, i.e., set of outputs for a given input set. This can be used to, for example, check the robustness of neural network predictions to bounded perturbations of an input. However, verifying properties concerning the preimage, i.e., the set of inputs satisfying an output property, requires abstractions in the input space. We present a general framework for preimage abstraction that produces under- and over-approximations of any polyhedral output set. Our framework employs cheap parameterised linear relaxations of the neural network, together with an anytime refinement procedure that iteratively partitions the input region by splitting on input features and neurons. The effectiveness of our approach relies on carefully designed heuristics and optimization objectives to achieve rapid improvements in the approximation volume. We evaluate our method on a range of tasks, demonstrating significant improvement in efficiency and scalability to high-input-dimensional image classification tasks compared to state-of-the-art techniques. Further, we showcase the application to quantitative verification and robustness analysis, presenting a sound and complete algorithm for the former and providing sound quantitative results for the latter.