Source-linked AI summary
Safety Verification of Deep Neural Networks
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, Min Wu
TL;DR
Neural-network classifiers can be unsafe because small, human-imperceptible input changes may alter decisions in safety-critical applications, while verification methods for such decisions remain limited. The paper develops an SMT-based framework that discretises specified manipulation regions and propagates their analysis through feed-forward networks. It implements the approach in Z3, finds adversarial examples on several state-of-the-art networks, and identifies scalability limits from exponential feature complexity.
Problem
Neural-network image classifiers can change labels under small perturbations that humans would regard as the same image, creating safety concerns for perception and control systems.
Method
The framework verifies pointwise classification invariance by discretising a user-specified safe region and propagating manipulation analysis layer by layer through the network using SMT.
Results
The Z3-based implementation finds adversarial examples on state-of-the-art classifiers, including examples automatically found for CIFAR10 networks.
Takeaways & Limitations
The framework can provide exhaustive adversarial-example searches for a specified region and manipulation family, supporting safety assessment of individual network decisions.
Takeaways & Limitations
Verification has prohibitive complexity for larger images because the process is exponential in the number of features.
Abstract
from arXiv · showhide
Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. We develop a novel automated verification framework for feed-forward multi-layer neural networks based on Satisfiability Modulo Theory (SMT). We focus on safety of image classification decisions with respect to image manipulations, such as scratches or changes to camera angle or lighting conditions that would result in the same class being assigned by a human, and define safety for an individual decision in terms of invariance of the classification within a small neighbourhood of the original image. We enable exhaustive search of the region by employing discretisation, and propagate the analysis layer by layer. Our method works directly with the network code and, in contrast to existing methods, can guarantee that adversarial examples, if they exist, are found for the given region and family of manipulations. If found, adversarial examples can be shown to human testers and/or used to fine-tune the network. We implement the techniques using Z3 and evaluate them on state-of-the-art networks, including regularised and deep learning networks. We also compare against existing techniques to search for adversarial examples and estimate network robustness.
1 Introduction
The paper frames adversarial instability in neural-network image classifiers as a safety problem for perception and control systems, then proposes automated verification of individual classification decisions under specified image manipulations.
- Neural networks can misclassify images after minimal, sometimes imperceptible perturbations, including camera-related changes such as resizing, cropping, or altered lighting.
- Safety assurance and verification methodologies for machine learning remain little studied despite applications in safety-critical systems such as autonomous driving.
- The paper focuses on individual-decision safety by requiring classification invariance within a neighbourhood of a given image, rather than estimating average robustness across data points.
- A decision is defined as safe when user-specified manipulations preserve the same class throughout a region assumed to contain images with the same human-assigned class.
- The framework uses discretisation and layer-by-layer propagation to systematically explore manipulation regions, operating directly on network code and trained weights.
- The implementation uses Z3 in DLV and evaluates networks trained on MNIST, CIFAR10, GTSRB, and ImageNet, while comparing MNIST falsification with existing methods.
2 Background on Neural Networks
The paper models feed-forward neural networks as layered transformations that map high-dimensional inputs through successive activation functions to outputs. These classifiers are trained from finite examples and use regularisation to improve local smoothness and generalisation.
- Feed-forward networks arrange neurons in disjoint layers, with connections between successive layers but not between neurons within the same layer.
- Formally, a network consists of layers, sequential connections, and one activation function for each non-input layer.
- An input is propagated through the network by successive activation functions, producing a corresponding activation vector at each layer.
- A neural-network classifier approximates human image-labeling capability from a finite set of training examples in a high-dimensional, potentially nonlinear space.
- Regularisation techniques such as dropout improve smoothness by encouraging nearby points around training examples to receive the same class.
- The verification method works with the network implementation and its trained weights.
3 Safety Analysis of Classification Decisions
The framework defines pointwise safety as invariant classification within a user-specified neighbourhood and verifies it by exhaustively exploring valid manipulations through discretised, layer-wise ladders. Under complete coverage and minimal manipulations, finding no adversarial example establishes safety for the region.
- Safety definition: Safety requires every activation in the specified region around an input to produce the same output-layer classification as the original.The region represents inputs that a human would judge close enough to share the original class.
- Scope: The framework is point-specific rather than distributional, unlike risk and statistical robustness measures.Its guarantee concerns the selected input, region, and manipulation family rather than an input distribution.
- Manipulations: The user defines manipulation families and distance measures to model perturbations such as camera-angle changes, scratches, or weather conditions.Manipulations operate on layer activations and may be represented as hyper-rectangles; the framework considers L2 and L1 distances.
- Discretised search: Minimal manipulations permit exhaustive discrete exploration because checking the endpoints suffices to detect a classification change within each manipulation hyper-rectangle.This yields an exhaustive but potentially impractical search in unit steps, with finer manipulations used for refinement.
- Ladders and coverage: Ladders form a complete branching exploration tree by repeatedly applying valid manipulations, while bounded variation supports finite coverage of the region.Each branch starts from the original activation and records successive manipulated activations until reaching the region boundary or a leaf.
- Verification guarantee: Safety with respect to manipulations is defined by a complete, covering ladder set whose region has zero variation, and general safety implies this property.Conversely, under minimality, exhaustive ladder search is sufficient to find any adversarial example or certify safety when none is found.
4 The Verification Framework
The framework verifies classification safety by searching for adversarial misclassifications, propagating regions and manipulations through hidden layers, and using SMT-based recursive checking. Feature-based partitioning reduces high-dimensional verification into lower-dimensional independent subproblems.
- Verification Framework: The framework searches for adversarial misclassifications to establish safety or falsification, with discovered examples usable for testing or fine-tuning.The method guarantees finding a misclassification when one exists within the specified region and manipulation family.
- Layer-by-Layer Analysis: Regions are propagated layer by layer using mappings between activations and regions, with each deeper-layer region covering the preceding-layer region.Definition 6 requires region inclusion under the reverse-layer mappings and supports computing later regions from earlier ones.
- Layer-by-Layer Analysis: Layer refinement means every manipulation at one layer is implemented by a sequence of valid manipulations at the next layer.The refinement relation connects safety notions across consecutive layers and supports implication toward input-layer safety.
- Refinement Framework: If manipulations are refined by layer, safety with respect to the deeper-layer region and manipulations implies safety at the preceding layer.Theorem 3 provides the formal implication used by the refinement framework.
- Verification Method: The recursive procedure determines regions and manipulation sets, verifies safety at the current layer, reports safety when successful, and continues toward the output layer.The procedure can start from any selected layer and uses SMT solvers to encode refinement and within-layer verification.
- Feature Decomposition and Discovery: Feature partitioning addresses high-dimensional regions by exploiting feature independence and low dimensionality, while hidden-layer analysis can discover features automatically.Features assign small regions to activations and partition the verification region across disjoint dimension sets.
Determining the manipulation set ∆k according to ηk(αx,k), ηk−1(αx,k−1), and ∆k−1
The manipulation-set construction adapts exact layer refinement when precise spans are computationally impractical, using an ε-approximate notion while retaining the relevant region. Experiments use bounded first-layer manipulations and map hidden-layer adversarial activations back to input images.
- Approximate Refinement: Exact span computations can produce overly small manipulation spans and unacceptable verification costs, motivating a weaker ε-parameterized refinement notion.The approximate relation permits activation targets to lie within a hyper-rectangle rather than requiring exact reachability.
- Approximate Refinement: ε-refinability replaces exact activation reachability with a sequence whose consecutive activations differ by at most ε.The definition requires valid layer manipulations and a bounded distance between successive activations.
- Approximate Refinement: The maximal number of next-layer manipulations is represented by h when constructing approximate refinement values.The framework uses h to express a lower-layer manipulation through a bounded sequence of higher-layer manipulations.
5 Experimental Results
DLV was evaluated on small synthetic and image-classification networks using exhaustive, layer-by-layer verification and adversarial-example search. The experiments found class changes across MNIST, CIFAR-10, GTSRB, and ImageNet settings, while some high-dimensional cases remained safe within the tested manipulation region.
- Experimental setup: DLV was validated on fully connected and convolutional networks, including ReLU, pooling, zero-padding, and dropout layers.The experiments used small surface-classification networks and medium-sized image-classification networks.
- Two-dimensional point classification: The two-dimensional network achieved more than 99% accuracy on 5,000 sampled training points.It used three fully connected hidden layers with ReLU activations.
- Two-dimensional point classification: The input-layer manipulation set contained 9 points, but missed class changes that existed elsewhere inside the surrounding region.The experiment therefore reported the input-layer decision as safe for that manipulation set.
- Two-dimensional point classification: A class change was detected after refining the analysis at the first hidden layer and mapping the manipulation set back to the input layer.The detected class change is represented as a red point in the corresponding visualization.
- MNIST: On MNIST, most examples yielded a class change within 100 dimensional changes in the first hidden layer, with some requiring fewer than 30.The tool checked the entire network for cases with up to 40 dimensional changes, and adversarial-example search took up to several minutes.
- CIFAR-10: On CIFAR-10, human-recognisable image modifications could nevertheless cause incorrect classifications, with searches ranging from seconds to 20 minutes.The experiment used 500 dimensions and produced pairs of correctly classified originals and wrongly classified perturbed images.
- ImageNet: On ImageNet, one street-sign image was unsafe after 6,346 dimensional changes, while another was safe for 20,000 changes.The unsafe case involved 0.2% of the 3,211,264 dimensions in the second layer; the authors suggest the safe case may require more complex manipulations.
6 Comparison
The comparison evaluates DLV against FGSM and JSMA, contrasting deterministic single-path heuristics with DLV’s multi-path search. Across high-success settings, JSMA finds the smallest perturbations, DLV is intermediate, and FGSM is fastest but requires larger changes.
- FGSM: FGSM deterministically increases ϵ from 0.05 to 0.4, with the final image misclassified after a relatively large manipulation.The experiment tests misclassification against the original image at each perturbation level.
- JSMA: JSMA gradually manipulates selected pixels and reaches misclassification while changing no more than 10% of the pixels under the reported setting.The setting uses ϵ = 0.1 and θ = 1.0.
- DLV: DLV uses nondeterministic feature selection through Monte Carlo Tree Search rather than a fixed feature order, allowing multi-path exploration.The search has a theoretical convergence guarantee for infinite sampling.
- Runtime: DLV takes 1–2 minutes per MNIST image, JSMA about 10 minutes per image, while FGSM is fastest per image because it processes a set of images.The comparison uses a randomly selected test set of 500 images.
- Results: 97.2% for FGSM with ϵ = 0.4, 98% for DLV with dimsl = 450, and 99% for JSMA with θ = 0.4 are the reported high-success settings.At these settings, JSMA has the smallest average L1 and L2 distances, followed by DLV and then FGSM.
- Caveat: Smaller perturbations that cause misclassification may reduce transferability, making the adversarial example harder to reproduce on another model.The note applies to transferability across models trained on the same or a small subset of the dataset.
7 Related Work
Related verification and adversarial-example methods differ in scalability, activation-function support, and guarantees. The paper positions its layer-by-layer constraint-based analysis as more scalable than earlier whole-network encodings while retaining systematic region exploration.
- Neural-network verification: Earlier SAT-based verification encoded the entire network but was limited to networks with six neurons and three hidden neurons.A later method improved on this approach but supported only ReLU activation functions.
- Adversarial-example search: FGSM uses a fast deterministic gradient-sign manipulation that tests discrete points along a lasso-type ladder tree without branches.The resulting search does not satisfy the covering property.
- Robustness estimation: Existing optimisation-based robustness methods compute approximations because non-convex search spaces and lack of convergence guarantees prevent exact minimal-perturbation results.This contrasts with the paper’s constraint-based verification framing.
- Robustness estimation: Distribution-averaged robustness is difficult to estimate accurately in high dimensions, motivating comparison with pointwise safety notions.The related work identifies pointwise robustness as corresponding to the paper’s general safety concept.
8 Conclusions
The paper presents an SMT-based framework that systematically explores manipulation regions around images and propagates verification through network layers. It finds adversarial examples quickly in small-dimensional cases, but verification becomes prohibitively complex for larger images.
- Conclusions: The framework systematically explores a region around a data point for specified adversarial manipulations and propagates the analysis into deeper layers.Although focused on classification, the approach is stated to generalise to other network types.
- Conclusions: The approach was implemented using SMT and validated on several state-of-the-art neural-network classifiers for realistic images.The implementation is associated with the DLV tool and configurable network and image inputs.
- Conclusions: Adversarial examples were found in some cases within seconds when only a few dimensions were involved.This result concerns falsification during the verification framework’s systematic search.
- Limitations: Verification has exponential complexity in the number of features and becomes prohibitively complex for larger images.Parallelisation is identified as a potential way to improve performance and scalability.
- Implementation: The tool supports heuristic single-path and Monte Carlo Tree Search modes, with configurable starting layer, dimension limits, precision, and feature dimensions.These parameters define how the analysis explores network layers.
A.2 Network for the MNIST Dataset –
The MNIST network configuration specifies layer and parameter settings, including l = 1, dims_l = 150, sp = 1.0, mp = 1.0, ε = 1.0, and dims_k,f = 5.
- The configuration sets l = 1 and dims_l = 150.
- The configuration sets sp = 1.0 and mp = 1.0.
- The configuration sets ε = 1.0 and dims_k,f = 5.
A.3 Network for the CIFAR-10 Dataset –
The CIFAR-10 network configuration uses specified layer dimensions and search parameters, with Figure 13 showing adversarial examples found by single-path search.
- The reported configuration includes layer dimensions of 500 and 1000, with a second layer dimension of 20,000.
- The search parameters set sp = 1.0, mp = 1.0, ε = 1.0, and dimsk,f = 5.
- Figure 13 presents additional adversarial examples for the CIFAR-10 network obtained by single-path search.
C Additional Adversarial Examples for the German Traffic Sign Recognition Benchmark (GTSRB)
This section presents additional adversarial examples for traffic-sign recognition and other networks, including examples produced by single-path search and specific GTSRB misclassifications.
- Figure 16 presents adversarial examples obtained using single-path search for the GTSRB dataset.
- Other GTSRB examples include speed limit 50 to speed limit 80 and speed limit 70 to speed limit 120.
- Additional examples include no overtaking to go straight and priority road to speed limit 30.
- The reported GTSRB misclassifications include road narrows to construction and give way to priority road.
D Architectures of Neural Networks
The paper presents architectures for a two-dimensional point-classification network and networks trained on MNIST, CIFAR-10, and GTSRB, with the ImageNet network sourced from prior work.
- Figure 17 presents the architecture of the neural network for two-dimensional point classification.
- Figure 18 presents the architecture of the neural network for the MNIST dataset.
- Figure 19 presents the architecture of the neural network for the CIFAR-10 dataset.
- Figure 20 presents the architecture of the neural network for the GTSRB dataset.
- The network for the ImageNet dataset is from [34].