Efficient Preimage Approximation for Neural Network Certification

TL;DR

This paper introduces PREMAP2, an improved algorithm for neural network preimage approximation that enhances scalability and enables certification of complex, real-world models against adversarial inputs.

Contribution

The authors extend PREMAP with new heuristics and sampling techniques, allowing application to high-dimensional, real-world neural networks for robustness and fairness certification.

Findings

PREMAP2 successfully certifies robustness against patch attacks on CNNs.

The method supports non-uniform priors and provides confidence intervals.

Open-source implementation is available for practical use.

Abstract

The growing reliance on artificial intelligence in safety- and security-critical applications is raising concerns about the robustness of neural networks to erroneous or adversarial input. Certification is a methodology for ensuring model trustworthiness by providing formal guarantees on model behaviour. While most verification methods focus on worst-case analysis by bounding the network output, an alternative approach based on approximating the preimage can complement such analysis by estimating the proportion of inputs that satisfy a given specification. However, existing preimage-based methods, such as the state-of-the-art PREMAP, are limited to fully connected neural networks of moderate dimensionality. In this paper, we introduce PREMAP2, a collection of algorithmic extensions to PREMAP that enhance its scalability and efficiency through improved branching heuristics, adaptive Monte Carlo sampling, and reverse bound propagation. We further endow PREMAP2 with additional functionality such as support for non-uniform priors and confidence intervals. These advances enable the application of PREMAP2 to previously intractable settings, including real-world patch attacks against convolutional neural networks, where adversarial stickers or lighting conditions obscure parts of images. We showcase the effectiveness of our approach across several use cases, including certifying reliability, robustness, interpretability, and fairness, on domains ranging from computer vision to control tasks. Our implementation is available as open-source software.