PaperlayerView exact revision on arXiv

Source-linked AI summary

Verification of Deep Convolutional Neural Networks Using ImageStars

Hoang-Dung Tran, Stanley Bak, Weiming Xiang, Taylor T. Johnson

arXiv:2004.05511v2cs.LGcs.CV

TL;DR

Small adversarial changes can cause CNNs to make errant predictions, while existing verification methods have limited ability to handle CNNs and real-world networks. This paper uses ImageStar-based exact and over-approximate reachability for robustness verification, and reports less conservative and faster analysis than zonotope and polytope methods. Its analysis applies to real-world CNNs with small perturbed input sets, while input-set size remains an important performance constraint.

  • Problem

    CNNs can be vulnerable to small adversarial input changes, and only a handful of existing verification methods handle CNNs, limiting formal evaluation of robustness in real-world networks.

    Source: §1 · pp. 1–2

  • Method

    The paper represents perturbed images with ImageStars and uses exact and over-approximate reachability algorithms to analyze CNN outputs and robustness.

    Source: §1 · pp. 2–3

  • Results

    The approach is reported as less conservative than zonotope and polytope approaches and faster when dealing with deep networks.

    Source: §1 · p. 2, §7 · p. 20

  • Takeaways & Limitations

    The method can verify robustness of real-world CNNs with small perturbed input sets and can compute and visualize exact output ranges.

    Source: §7 · p. 20

    Large input sets can increase computation time, memory use, and conservativeness, and these challenges also affect existing approaches.

    Source: §6 · pp. 19–20

Abstract

from arXiv · show

Convolutional Neural Networks (CNN) have redefined the state-of-the-art in many real-world applications, such as facial recognition, image classification, human pose estimation, and semantic segmentation. Despite their success, CNNs are vulnerable to adversarial attacks, where slight changes to their inputs may lead to sharp changes in their output in even well-trained networks. Set-based analysis methods can detect or prove the absence of bounded adversarial attacks, which can then be used to evaluate the effectiveness of neural network training methodology. Unfortunately, existing verification approaches have limited scalability in terms of the size of networks that can be analyzed. In this paper, we describe a set-based framework that successfully deals with real-world CNNs, such as VGG16 and VGG19, that have high accuracy on ImageNet. Our approach is based on a new set representation called the ImageStar, which enables efficient exact and over-approximative analysis of CNNs. ImageStars perform efficient set-based analysis by combining operations on concrete images with linear programming (LP). Our approach is implemented in a tool called NNV, and can verify the robustness of VGG networks with respect to a small set of input states, derived from adversarial attacks, such as the DeepFool attack. The experimental results show that our approach is less conservative and faster than existing zonotope methods, such as those used in DeepZ, and the polytope method used in DeepPoly.

1 Introduction

CNNs are vulnerable to small adversarial input changes, motivating formal robustness evaluation, especially for safety-critical applications. The paper introduces ImageStar-based reachability analysis and reports that its implementation is less conservative and faster than zonotope and polytope approaches.

1 Introduction

  • CNNs can produce errant predictions after tiny input changes, raising concerns about their use in safety-critical applications and motivating formal robustness evaluation.The introduction also notes CNN applications including face recognition, image classification, document analysis, and semantic segmentation.Source: §1 · p. 1
  • ImageStar represents sets of images and supports exact and over-approximate reachability algorithms for constructing reachable sets and verifying CNN robustness.Reachable sets contain possible network outputs under bounded input sets; exact reachability can construct concrete adversarial examples when a robustness property is violated.Source: §1 · pp. 2–3
  • Only a handful of existing verification methods address CNNs, and the introduction identifies just one that handles real-world CNNs such as VGGNet [27].That approach [26] uses L0 distance and optimization, whereas this paper analyzes bounded input sets subject to arbitrary linear constraints.Source: §1 · p. 2
  • The NNV implementation is reported as less conservative and faster than the zonotope method in DeepZ and the polytope method in DeepPoly.The comparison concerns robustness verification of CNNs.Source: §1 · p. 2

2 Problem formulation

The paper formulates CNN reachability as constructing a set containing all possible network outputs for a perturbed input set. It defines the reachable set incrementally across the network's layers.

2 Problem formulation

  • CNN reachability analyzes a trained network on a perturbed input set to construct a set containing all possible network outputs.The formulation considers a linear input set.Source: §2 · p. 3
  • The modeled CNN consists of layers that may include convolution, fully connected, max-pooling, average-pooling, and ReLU operations.Source: §2 · p. 3
  • The reachable set is constructed layer by layer, with each layer's reachable set determined by its operation.The output reachable set of one layer becomes the input for the next.Source: §2 · p. 3

3 ImageStar

ImageStar represents a set of images using an anchor image, generator images, and a predicate over their coefficients. Its image-based representation extends generalized star sets and supports reachability analysis across several CNN layer types.

3 ImageStar

  • An ImageStar is a tuple of an anchor image, generator images, and a predicate, with the generators arranged as a basis array.The anchor and generators have height, width, and channel dimensions; the represented set is constrained by the predicate.Source: §3 · p. 3
  • ImageStar predicates are conjunctions of linear constraints, and the represented set is empty exactly when the predicate is empty.The predicate has the form Cα ≤ d.Source: §3 · p. 4
  • A bounded disturbance on one pixel of a 4 × 4 grayscale image is given as an ImageStar example.The disturbance b lies in [-2, 2] and is applied at position (1, 2, 1).Source: §3 · p. 4
  • Unlike generalized star sets, whose anchors and generators are vectors, ImageStar uses images with multiple channels.The paper says this representation is efficient for reachability analysis of convolutional, fully connected, and average-pooling layers.Source: §3 · p. 4
  • An affine mapping transforms the ImageStar anchor and generators while preserving its predicate.The anchor becomes γ × c + β, and the generators become γ × V; γ may be a scalar or channel-wise scale factors.Source: §3 · p. 4

4 Reachability of CNN using ImageStars

ImageStar reachability propagates sets layer by layer through a CNN. Convolution, pooling, fully connected, and batch-normalization layers have exact reachable sets, while max-pooling and ReLU also support over-approximation to control set growth.

4.1 Reachability of a convolutional layer

  • Convolution maps the ImageStar anchor with the layer’s bias and each generator image with its weights, producing another ImageStar.This preserves the input predicate while transforming the anchor and generators separately.Source: §4.1 · p. 5

4.2 Reachability of an average pooling layer

  • Average pooling applies the pooling operation to the ImageStar anchor and generator images, producing another ImageStar with the same predicate.Source: §4.2 · p. 6

4.3 Reachability of a fully connected layer

  • A fully connected layer maps the reshaped anchor affinely and each reshaped generator linearly, yielding another ImageStar.The flattened input dimension must match the weight matrix’s input dimension.Source: §4.3 · p. 6

4.4 Reachability of a batch normalization layer

  • Batch normalization transforms an ImageStar into another ImageStar using two affine mappings.The layer is parameterized by the training-set mean and variance, a stabilizing ε, and learned scale and offset.Source: §4.4 · pp. 6–7

4.5 Reachability of a max pooling layer

  • Exact max-pooling reachability enumerates local maximum candidates and splits the input ImageStar when candidates depend on predicate values.The number of resulting ImageStars can grow quickly; estimated pixel ranges reduce candidate searches before exact range checks.Source: Exact reachability of a max pooling… · pp. 7–9
  • Over-approximate max pooling replaces multiple local maximum candidates with a new predicate variable, yielding one over-approximate reachable set.The new variable is constrained to be at least each candidate and no greater than an upper bound for the region.Source: Exact reachability of a max pooling… · p. 9

4.6 Reachability of a ReLU layer

4.7 Reachabilty algorithm and parallelization

  • CNN reachability propagates each layer’s output set as the next layer’s input; exact analysis can process multiple ImageStars in parallel as sets grow.Convolution, average pooling, and fully connected layers have exact reachable sets; max pooling and ReLU have exact and over-approximate options.Source: §4.7 · p. 12

5 Evaluation

The evaluation compares ImageStar with zonotope and polytope methods on MNIST CNNs, then tests VGG16 and VGG19 with adversarially derived input sets. Results show differences in provable robustness, verification time, and the limits imposed by input-set size.

5.1 Robustness Verification of MNIST Classification Networks

  • The MNIST evaluation attacked 100 correctly classified images with independently varied pixels and tested whether the correct class remained the maximum over each reachable output set.The networks had 98%, 99.7%, and 99.9% accuracy; d controls which pixels are attacked and δ sets their allowed value range.Source: §5.1 · pp. 13–14
  • For a digit-0 attack with d = 250 and δ = 0.05, ImageStar and polytope proved robustness, while zonotope ranges could not; ImageStar produced tighter ranges than polytope.The zonotope computation took 93 seconds, compared with 0.3 seconds for polytope and 0.74 seconds for approximate ImageStar.Source: §5.1 · p. 14, Figure 8 · p. 15
  • For large MNIST networks, ImageStar was 16.65 times faster on average than polytope and proved robustness in more cases; polytope was faster on the small network.For d = 240 and δ = 0.015, ImageStar proved 88 medium-network cases versus 38 for polytope, and 71 small-network cases versus 65.Source: §5.1 · p. 14, Table 2 · p. 16, Table 3 · p. 16

5.3 Exact Analysis vs. Approximate Analysis

  • For small input sets and small δ, polytope and ImageStar could prove VGG16 and VGG19 robustness in reasonable time, with similar times except in two cases where ImageStar was faster.Robustness required the bell-pepper output, index 946, to remain maximal.Source: §5.2 · p. 16, Table 4 · p. 17
  • For VGG19, exact analysis found non-robustness at attack levels of at least 98% and produced a strawberry-classified counterexample, while over-approximation could not prove non-robustness.At l = 0.95% and δmax = 2 × 10^-7, the bell-pepper output remained maximal in the illustrated case.Source: §5.3 · p. 17, Table 5 · p. 17, Figure 10 · p. 18
  • In VGG19 reachability, max-pooling and ReLU layers dominated computation because they require many linear-programming problems; convolutional and fully connected layers were quick.The reported profile used a 50% attack and 10^-7 perturbation; the bottleneck involved five max-pooling and 18 ReLU layers.Source: §5.3 · p. 18, Figure 11 · p. 19
  • Large input sets can increase computation time, memory use, and conservativeness across methods; exact analysis may create many ImageStars, while over-approximation can still require substantial memory.The number of ImageStars in exact analysis increases with input size; 100 splits in VGG19's first ReLU layer would require about 2.4 GB for the resulting ImageStar.Source: §6 · pp. 19–20, Figure 12 · p. 20

7 Conclusion

The paper concludes that ImageStar-based reachability can verify deep CNN robustness and compares favorably with zonotope and polytope approaches. Its current scope is small perturbed input sets, while larger inputs and computational costs remain targets for future work.

7 Conclusion

  • ImageStar reachability is less conservative than recent zonotope and polytope approaches and faster when dealing with deep networks.The method can verify real-world CNN robustness for small perturbed input sets.Source: §7 · p. 20
  • Exact and over-approximate ImageStar reachability algorithms construct reachable sets and support CNN robustness verification.Source: §7 · p. 20
  • ImageStar analysis can compute exact reachable sets, visualize deep CNN output ranges, and speed analysis significantly with parallel computing.Source: §7 · p. 20
  • Input-set size is an important factor affecting reachability-algorithm performance.Source: §7 · p. 20
  • Future work targets larger input sets and lower memory and time complexity.Source: §7 · p. 20

A.1 Exact reachability algorithm for a max-pooling layer

The exact max-pooling procedure maps an ImageStar input to output ImageStars by identifying local maximum candidates and splitting where the maximum is ambiguous.

A.1 Exact reachability algorithm for a max-pooling layer

  • The algorithm zero-pads the ImageStar input and computes the max-map size and start indexes for local regions.Source: §A.1 · p. 24
  • For each max-map point, it finds maximum candidates and updates the output basis directly when there is only one candidate.Source: §A.1 · p. 24
  • When a point has multiple maximum candidates, the algorithm records it as a splitting point and splits the ImageStar set.Source: §A.1 · p. 24
  • The procedure returns the final output set as an array of ImageStars.Source: §A.1 · p. 24

A.2 Approximate reachability algorithm for a max-pooling layer

The approximate max-pooling procedure handles ambiguous local maxima by introducing predicate variables and constraints to construct an over-approximate ImageStar output set.

A.2 Approximate reachability algorithm for a max-pooling layer

  • The procedure zero-pads the ImageStar input and computes the max-map dimensions and local-region start indexes.Source: §A.2 · p. 24
  • When a local region has multiple maximum candidates, it introduces a predicate variable to represent that region's max point and updates the max-map basis.Source: §A.2 · p. 24
  • It adds constraints on the new predicate variables and constructs the over-approximate ImageStar output set.Source: §A.2 · p. 24

A.4 Comparison with ERAN-DeepZ [28]

On the tested CIFAR-10 ConvMaxPool network, ImageStar verifies slightly more images than ERAN-DeepZ, but its runtime grows quickly as the robustness bound increases. ERAN-DeepZ is faster for larger input sets, while the comparison uses a low-accuracy network and brightening attacks.

A.4 Comparison with ERAN-DeepZ [28]

  • The comparison uses a CIFAR-10 subset with 60000 32 × 32 color images in 10 classes and a network with four convolutional and two max-pooling layers.The network also has seven ReLU and three fully connected layers; tested pixels are scaled into [0, 1], and the attack brightens selected pixels independently.Source: §A.4 · pp. 24, 27
  • The exact max-pooling procedure splits ImageStars at output points with multiple maximum candidates and constrains each split to make one candidate the maximum.Source: §A.4 · p. 25
  • The approximate max-pooling procedure represents a region with multiple maximum candidates using a new predicate variable and added constraints.Source: §A.4 · p. 26
  • ImageStar gives a slightly better result than ERAN-DeepZ in the number of verifiable images on the CIFAR-10 ConvMaxPool network.Table 6 presents the verification results.Source: §A.4 · p. 27, Table 6 · p. 28
  • ImageStar verification time grows quickly as robustness bound δ increases, whereas ERAN-DeepZ is faster for large input sets because reachable-set construction uses no LP optimization.The paper describes the runtime increase as the cost of improving the conservativeness of over-approximate methods.Source: §A.4 · p. 27
Loading 2004.05511v2…