Source-linked AI summary
Verifying Properties of Binarized Deep Neural Networks
Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, Toby Walsh
TL;DR
Deep neural networks raise important questions about properties such as robustness, but exact verification remains challenging. This paper encodes BNNs as exact Boolean formulas and combines SAT solving with counterexample-guided search; experiments demonstrate verification of medium-sized image-classification networks.
Problem
Exact methods for verifying important deep-neural-network properties, especially adversarial robustness, are needed as these networks face crafted perturbations and security risks.
Method
The paper constructs an exact Boolean encoding of BNNs and uses SAT solvers with a counterexample-guided search procedure to verify their properties.
Results
The approach verifies medium-sized BNNs, with SAT and CEG outperforming ILP; a five-layer BNN was certified or attacked on up to 95% of considered images.
Takeaways & Limitations
Exact Boolean encoding enables certifiable robustness and equivalence checking for BNNs on MNIST and variant datasets.
Takeaways & Limitations
During inference, the additional hard tanh layer used in training is omitted from the BNN construction.
Abstract
from arXiv · showhide
Understanding properties of deep neural networks is an important challenge in deep learning. In this paper, we take a step in this direction by proposing a rigorous way of verifying properties of a popular class of neural networks, Binarized Neural Networks, using the well-developed means of Boolean satisfiability. Our main contribution is a construction that creates a representation of a binarized neural network as a Boolean formula. Our encoding is the first exact Boolean representation of a deep neural network. Using this encoding, we leverage the power of modern SAT solvers along with a proposed counterexample-guided search procedure to verify various properties of these networks. A particular focus will be on the critical property of robustness to adversarial perturbations. For this property, our experimental results demonstrate that our approach scales to medium-size deep neural networks used in image classification tasks. To the best of our knowledge, this is the first work on verifying properties of deep neural networks using an exact Boolean encoding of the network.
1 Introduction
The paper addresses the need to verify deep-network properties by developing an exact SAT encoding for Binarized Neural Networks, focusing on robustness and equivalence. Experiments show the approach can verify medium-sized image-classification BNNs.
- Motivation: BNNs are attractive for resource-constrained devices because binary parameters reduce memory use and binary activations enable fast matrix multiplication.They have achieved performance comparable to floating-point networks on several standard datasets.
- Contribution: The paper constructs an exact Boolean formula representing a BNN without approximating its network structure.This encoding supports rigorous investigation of BNN properties using SAT solvers.
- Target properties: The study focuses on verifying network robustness to adversarial perturbations and equivalence between networks.These properties arise in security-sensitive deployment and after network alterations or input preprocessing.
- Verification: SAT encoding can certify whether a BNN is robust to adversarial perturbation on a particular image.The same encoding can check network equivalence or produce inputs where two networks differ.
- Results: For a five-fully-connected-layer BNN, the method proves robustness or finds an adversarial perturbation for up to 95% of considered images.The experiments use MNIST and its variants.
2 Preliminaries
The preliminaries formalize neural-network inputs, outputs, robustness, and equivalence, while motivating verification through adversarial vulnerability and network transformations. Robustness is defined by the absence of bounded perturbations causing misclassification across a set of inputs.
- Classification setting: The image-classification task learns a classifier from labeled images sampled from an unknown distribution and label function.Images are represented as vectors in Z^n and labels belong to [s].
- Network notation: For a feedforward network F, F(x) denotes its output and ℓx denotes the ground-truth label of input x.These quantities support the formal definitions of network properties.
- Robustness: Universal adversarial robustness requires that no perturbation with ||τ||p ≤ ϵ causes misclassification on at least a ρ-fraction of inputs in S.The p = ∞ case bounds the maximum perturbation applied to each input entry.
- Equivalence: Network equivalence means two networks produce identical outputs for every input in their domain.The property is relevant to network alteration, model reduction, and preprocessing changes.
- Transformation order: Augmentation reordering asks whether applying transformations f and g in different orders changes a network’s behavior.The setup considers networks that apply compositions such as f ◦ g before inference.
3 Binarized Neural Networks
A BNN is organized as sequential blocks that transform predominantly binary representations, while allowing real-valued intermediate computations. Its standard internal block combines linear transformation, batch normalization, and binarization.
- BNN definition: A BNN is a feedforward network whose weights and activations are predominantly binary.The network is structured as sequential blocks rather than only individual layers.
- Block structure: Each internal block maps a binary input vector to a binary output vector, although its internal layers may produce real-valued intermediates.Blocks are assembled sequentially to form the network.
- Internal block: A common internal block applies a linear transformation, batch normalization, and binarization in sequence.The linear transformation may use a fully connected or convolutional layer.
- Training versus inference: During training, each internal block includes an additional hard tanh layer after batch normalization, but this layer is omitted during inference.The schematic of Figure 1 highlights this additional training-time layer.
- Input representation: The network input is assumed to be an integer vector, such as an RGB image, whose values can be encoded with binary values {−1, 1}.The formal BNN maps binary inputs to output labels.
4 Encodings of Binarized Networks
The paper encodes BNN blocks exactly by translating their linear, normalization, binarization, and output-selection operations into progressively smaller MILP, ILP, and SAT representations.
- Network encoding: BNNs are encoded compositionally as a conjunction of Boolean functions for internal blocks and the output block.The full network encoding links consecutive block inputs and outputs.
- Internal blocks: Each internal block applies a linear transformation, batch normalization, and sign-based binarization to binary inputs.The linear layer computes affine outputs, which batch normalization transforms before binarization produces binary activations.
- Output block: The output block computes affine scores, encodes pairwise score orderings with Boolean variables, and selects the maximal label.The ordering variables indicate whether one output score is at least another, and implication constraints determine the predicted output.
- ILP encoding: The ILP encoding removes real-valued intermediate variables by substituting integer-valued binary expressions and safely rounding thresholds.The resulting threshold constraints depend on the sign of the batch-normalization scale parameter.
- SAT encoding: Directly translating ILP into CNF is inefficient, so the SAT encoding exploits BNN structure and sequential counters for compact cardinality constraints.Sequential counters represent cumulative Boolean sums in unary.
5 Encoding of Properties
The exact SAT encoding expresses robustness and equivalence properties as satisfiability questions over valid inputs, perturbations, network outputs, and labels.
- Property encodings: The exact BNN encoding enables property verification directly in the SAT domain.The section focuses primarily on robustness and equivalence.
- Adversarial robustness: For L∞ robustness, each integer perturbation lies within [−ϵ, ϵ], and the perturbed image must remain within valid image bounds.These linear integer constraints are converted into Boolean variables and clauses.
- Adversarial robustness: The adversarial condition requires the predicted output to differ from the original image’s true label.Robustness checking therefore searches for a satisfying assignment representing a valid misclassified perturbation.
- Universal robustness: Universal robustness duplicates the adversarial encoding across inputs and checks whether at least a specified fraction are misclassified.The construction supports verifying a ρ-fraction condition over a set of images.
- Network equivalence: Network equivalence is checked by searching for a valid input on which two networks produce different outputs.An unsatisfiable formula certifies equivalence; a satisfying assignment supplies a distinguishing witness.
6 Counterexample-Guided Search Procedure
The counterexample-guided procedure exploits the BNN’s modular encoding by separating generation from verification and refining shared activation assignments with Craig interpolants.
- Motivation: Direct SAT solving can become difficult on large encodings, motivating a search procedure that exploits the network’s modular structure.The procedure is based on counterexample-guided search from formal verification.
- Generator–verifier decomposition: The network is partitioned into a generator for an initial block and a verifier for the remaining blocks and output condition.For robustness, the generator includes perturbation and valid-image constraints, while the verifier checks later blocks and misclassification.
- Shared interface: The generator and verifier communicate only through shared intermediate activation variables, which are usually few relative to the full formula.This small interface makes interpolant-based search practical.
- Counterexample-guided refinement: The procedure proposes generator assignments, tests whether the verifier can extend them, and extracts interpolants from unsatisfiable combinations to guide subsequent search.Interpolants use only variables shared by the two formulas and exclude regions that cannot yield a counterexample.
- Generalization: The partitioning approach extends beyond the illustrated two-block network by applying after each block or layer.The paper notes that the generalization is straightforward.
7 Related Work
Prior verification methods use approximations, solver branching, or limited scalability, whereas this work combines exact BNN encodings with block-level reasoning and interpolant-guided search.
- Existing verification methods: Earlier sigmoid-network verification approximated nonlinear activations and was reported to scale only to small networks.The cited approach used Boolean formulas over linear constraints and examples with about 20 hidden neurons.
- Existing verification methods: ReLU verification can handle constraints directly, but it is tailored to ReLU and introduces branching choices that raise scalability concerns.The cited work used an SMT solver to manage branching and studied networks with limited size.
- Paper’s distinction: The paper avoids abstraction refinement by reasoning over blocks of layers and uses interpolants rather than inverse functions to guide search.These choices distinguish the proposed procedure from the compared prior approach.
- Adversarial search: The authors identify MILP as the only previously proposed complete adversarial-perturbation search procedure, while many alternatives are incomplete.Their experiments use the more efficient ILP encoding as the baseline for BNNs.
8 Experimental Evaluation
Experiments evaluate adversarial-robustness verification on MNIST and two variants using ILP, SAT, and counterexample-guided SAT search. SAT-based methods outperform ILP, while CEG is generally faster than SAT and the datasets differ in perturbation difficulty.
- Experimental Setup: The experiments train BNNs on MNIST, MNIST-rot, and MNIST-back-image, evaluating 200 correctly classified test images per dataset.The networks use four internal blocks, with 200 neurons in the first linear layer and 100 in the others.
- Compared Methods: The study compares SCIP-based ILP, Glucose-based SAT, and counterexample-guided CEG searches for adversarial perturbations.Generated SAT formulas average about 1.4 million variables and 5 million clauses, with the largest reaching about 3 million variables and 12 million clauses.
- Results: SAT and CEG solve up to 30% more instances than ILP across all datasets, demonstrating the effectiveness of the SAT encoding over ILP.Solved instances include either finding a misclassifying perturbation or certifying that none exists within the timeout.
- Results: CEG solves more instances than SAT on MNIST-rot and MNIST-back-image, while SAT solves more on MNIST; CEG is faster across all datasets.Cactus plots show CEG solving most instances faster than SAT.
- Results: MNIST-rot images are easiest to perturb, whereas MNIST-back-image images are hardest to perturb.Figure 3 examples include perturbations whose differences can be indistinguishable to human observers.
- Certified Robustness: The complete search procedure certifies ε-robustness by establishing that no adversarial perturbation fools the network on a given image.As ε increases, fewer images are certified robust and fewer instances are solved within the 300-second timeout.
9 Conclusion
The paper presents an exact Boolean encoding for verifying BNN properties, including robustness and equivalence, and adds counterexample-guided search to accelerate verification. Experiments show feasibility on MNIST variants, while future work targets larger and more general networks.
- The proposed exact Boolean encoding verifies BNN properties including robustness and equivalence.
- Counterexample-guided search exploits the network’s modular structure to speed up property verification.
- Experiments demonstrate feasibility on MNIST and its variant datasets, while future work targets scalability to larger neural networks.
- Extending the approach to networks with fixed-bit weights is promising but presents an even more challenging scalability problem.