Analytically Determining the Robustness of Binarized Neural Networks

Binarized neural networks (BNNs) are a class of deep neural networks (DNNs) known for their minimal computational requirements during inference, making them ideal for low-performance environments. Despite their efficiency, BNNs are as vulnerable to safety and security issues as other types of DNNs, and hence analyzing their robustness is essential. In contrast to general DNNs, BNNs are relatively small and straightforward, making it feasible to assess their robustness analytically. We propose a method for rigorously analyzing BNN robustness based on 0–1 Integer Linear Programming (0–1 ILP), which utilizes the dual functionality of boolean variables within BNNs as both boolean (with values of ‘true’ and ‘false’) and real-valued variables constrained to binary values (0 and 1). By leveraging this duality, we formalize the robustness problem as a linear programming problem augmented with boolean reasoning. We minimize the distance to a differently classified image using either the L<inf xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</inf>-norm (binarized and non-binarized inputs) or the Lœ-norm (non-binarized inputs). We have implemented our approach using the Z3 solver and evaluated it on the MNIST and FashionMNIST datasets. Our results demonstrate the capability to construct optimal adversarial examples with minimal deviations from the ground truth images. We achieved a one-pixel difference between the original and perturbed images for all binarized images. We also identified minimal perturbations on grayscale images using the L<inf xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">1</inf> and Lœ-norms. For the latter, we simplified the analysis to determine the existence of epsilon-close adversarial examples across a range of epsilon values.