Boosting Few-Pixel Robustness Verification via Covering Verification Designs
Abstract
Proving local robustness is crucial to increase the reliability of neural networks. While many verifiers prove robustness in -balls, very little work deals with robustness verification in -balls, capturing robustness to few pixel attacks. This verification introduces a combinatorial challenge, because the space of pixels to perturb is discrete and of exponential size. A previous work relies on covering designs to identify sets for defining neighborhoods, which if proven robust imply that the -ball is robust. However, the number of neighborhoods to verify remains very high, leading to a high analysis time. We propose covering verification designs, a combinatorial design that tailors effective but analysis-incompatible coverings to robustness verification. The challenge is that computing a covering verification design introduces a high time and memory overhead, which is intensified in our setting, where multiple candidate coverings are required to identify how to reduce the overall analysis time. We introduce CoVerD, an robustness verifier that selects between different candidate coverings without constructing them, but by predicting their block size distribution. This prediction relies on a theorem providing closed-form expressions for the mean and variance of this distribution. CoVerD constructs the chosen covering verification design on-the-fly, while kee** the memory consumption minimal and enabling to parallelize the analysis. The experimental results show that CoVerD reduces the verification time on average by up to 5.1x compared to prior work and that it scales to larger -balls.
1 Introduction
Neural networks are very successful in various applications, most notably in image recognition tasks [14]. However, neural networks are also vulnerable to adversarial example attacks [32, 17]. In an adversarial example attack, an attacker slightly perturbs the input to mislead the network. Many attack models and different kinds of perturbations have been considered for neural networks implementing image classifiers [32, 15, 26]. The most commonly studied perturbations are perturbations, where is [9, 39], [10], [32, 4] or [15, 4]. For perturbations, the attacker is given a small budget and the goal is to find a perturbed input in the -ball that causes misclassification.
In response to adversarial attacks, many verifiers have been proposed to reason about the robustness of neural networks in a given neighborhood of inputs. Most deterministic robustness verifiers analyze robustness in -balls [33, 25, 31, 13, 21, 2], while some deterministic verifiers analyze -balls [22, 19] or -balls [37, 40]. Probabilistic verifiers, often leveraging randomized smoothing [6], have been proposed for analyzing -balls for [23, 28, 38, 11]. Other verifiers analyze neighborhoods defined by semantic or geometric features (e.g., brightness or rotation) [20, 24, 3]. An existing gap is deterministically verifying robustness in -balls, for a small , also known as robustness to few pixel attacks. In -balls, is the number of pixels that can be perturbed. Since is an integer (as opposed to a real number), we denote it as . -balls consist of discrete perturbations, unlike many other attack models whose perturbations are continuous. Thus, their analysis is a challenging combinatorial problem. Theoretically, robustness verification of an -ball can be reduced into a set of robustness verification tasks over neighborhoods, each allows a specific set of pixels to be perturbed. However, this approach is infeasible in practice for , since the number of the neighborhoods that need to be proven robust is , where is the number of pixels. To illustrate, for MNIST images, where , the number of neighborhoods is for , for , and for . That is, every minimal increase of (by one) increases the neighborhood size by two orders of magnitude.
A recent work proposes a deterministic robustness verifier for few pixel attacks, called Calzone [30]. Calzone builds on two main observations. First, if a network is robust to perturbations of a specific set of pixels, then it is also robust to perturbations of any subsumed set of these pixels. Second, often robustness verifiers can analyze robustness to arbitrary perturbations of specific pixels, for values of that are significantly larger than . They thus reduce the problem of verifying robustness in an -ball to proving robustness in a set of neighborhoods defined by a set of -sized pixel sets, subsuming all possible sets of pixels. To compute the -sized pixel sets, they rely on covering designs [16, 34]. Given parameters , a covering is a set of -sized sets that cover all subsets of size of a set (e.g., the pixel set). Covering designs is a field in combinatorics providing construction techniques to compute coverings. The challenge is to compute a covering of minimal size. While many covering constructions have been proposed, computing an optimal covering is an open combinatorial problem for most values of , and . Further, most best-known coverings for are far from the best general lower bound, known as the Schönheim bound [29]. This severely impacts the analysis time of Calzone. In practice, Calzone often does not complete within the five hour timeout when analyzing -balls. To scale, it is crucial to lower the number of analyzed sets. While there are effective covering constructions renowned for the small coverings they compute, they are limited to specific values of and , which are incompatible for the analysis of robustness. Since Calzone treats covering constructions as black-box, it is limited to rely on analysis-compatible coverings and cannot benefit from these effective constructions.
To boost the robustness verification of few pixel attacks, we propose a new covering type, called a covering verification design (CVD), tailoring covering designs for robustness verification. CVD relies on a highly effective construction to obtain an analysis-incompatible covering and partially induces it to an analysis-compatible covering, where sets can have different sizes. Although the exact sets and their sizes depend on a random choice, we prove that the mean and variance of the set sizes are independent of this choice and have closed-form expressions. Partially inducing this effective construction has been proposed before [27], however it has been proposed for another combinatorial design, requiring a bound on the maximal set size in the covering, unlike CVD. We demonstrate that the sizes of CVDs are lower by 8% for and by 15% for than the respective Schönheim lower bound. This improvement, enabled by considering a new type of coverings, is remarkable for scaling robustness analysis. To date, for analysis-compatible values of and and for , it is impossible to obtain an optimal covering design, and even if we obtained it, its size is at least the Schönheim bound. In particular, Calzone’s considered coverings are larger by 4x than the Schönheim lower bound for and by 8.4x for . While promising, CVDs raise a practical challenge: their construction as well as their final size introduce a high memory overhead. Further, to minimize the analysis time, the verifier chooses between multiple coverings. However, the total memory overhead makes it infeasible to store these coverings in a covering database without limiting their size (like Calzone does).
We introduce CoVerD, an robustness verifier, boosting Calzone’s performance by leveraging CVDs. CoVerD has two main components, planning and analysis. The planning component predicts the CVD that will allow it to minimize the overall analysis time. To reduce the memory overhead, it predicts the best CVD out of many candidates, without constructing the candidates. This prediction relies on estimating the set size distribution of a candidate covering, using our expressions for the mean and variance. The analysis component constructs the chosen CVD. The challenge is that the original covering that is being induced may be too large to fit the memory. To cope, CoVerD induces the covering while constructing the original covering. Further, it constructs on-the-fly a partitioning of the CVD so that the analysis can be parallelized over multiple GPUs. Another advantage of the on-the-fly construction is that CoVerD does not need to prepare coverings for every image dimension in advance. This both saves memory consumption and makes CoVerD suitable for any image classifier, without requiring to precompute coverings for new image dimensions, as Calzone requires.
We evaluate CoVerD on convolutional and fully-connected networks, trained for MNIST, Fashion-MNIST, and CIFAR-10. CoVerD is faster than Calzone in verifying robust -balls on average by 2.8x for and by 5.1x for . Further, CoVerD scales to more challenging -balls than Calzone. In particular, it verifies some -balls, which Calzone does not consider at all, within minutes.
2 Background
In this section, we define the problem of verifying robustness of an image classifier in an -ball and provide background on Calzone [30].
robustness verification
We address the problem of determining the local robustness of an image classifier in an -ball of an image . An image classifier takes as input an image consisting of pixels, each ranges over (all definitions extend to colored images, but omitted for simplicity’s sake). It returns a vector consisting of a score for every possible class. The classification the classifier assigns to an input image is the class with the maximal score: . We focus on classifiers implemented by neural networks. Specifically, our focus is on fully-connected and convolutional networks, since many robustness verifiers can analyze them [31, 13, 21, 2, 33, 25]. However, like Calzone, CoVerD is not coupled to the underlying implementation of the classifier and can reason about any classifier for which there are robustness verifiers that it can rely on. The problem we study is determining whether a classifier is locally robust in the -ball of an input , for . That is, whether every input whose distance from is at most is classified by as is classified. Formally, the -ball of is and is locally robust in if . We note that the distance of two images is the number of pixels that the images differ, that is (where ). In other words, an perturbation to an image can arbitrarily perturb up to pixels in .
Calzone
Calzone, depicted in Figure 1, is an robustness verifier. It verifies by determining the robustness of a classifier in all neighborhoods in which a specific set of pixels is arbitrarily perturbed, for every of size . Namely, to prove robustness, it has to determine for every such whether classifies the same all inputs in the neighborhood consisting of all images that are identical to in all pixels, but the pixels in . We denote this neighborhood by . Such neighborhoods can be specified as a sequence of intervals, one for every pixel, where the interval is if (i.e., it can be perturbed) or if (i.e., it cannot be perturbed). Most existing robustness verifiers can determine the robustness of such interval neighborhoods. However, verifying interval neighborhoods, one for every selection of pixels to perturb, is practically infeasible for . Instead, Calzone builds on the following observation: if is locally robust in a neighborhood for of size , then is also robust in every , for of size . This observation allows Calzone to leverage covering designs to reduce the number of neighborhoods analyzed by an verifier. Given three numbers , for , a covering is a set of blocks, where (1) each block is subset of size of and (2) the blocks cover all subsets of of size : for every of size , there is a block such that . Coverings are evaluated by their size, , where the smaller the better. We next describe the components of Calzone: analysis, planning and covering database.
Calzone’s analysis
Calzone begins the analysis by obtaining a covering from its covering database, where is determined by the planning component (described shortly). It pushes all blocks in the covering into a stack. It then iteratively pops a block from the stack and verifies the robustness of in by running GPUPoly [25]. GPUPoly is a sound robustness verifier which is highly scalable because it performs the analysis on a GPU. However, it relies on a linear relaxation and thus may fail proving robustness due to overapproximation errors. If it determines that is robust, Calzone continues to the next block. Otherwise, Calzone performs an exact analysis or refines the block. If , Calzone invokes a sound and complete mixed-integer linear programming (MILP) verifier [33]. If it determines that is not robust, Calzone returns non-robust, otherwise Calzone continues to the next block. If is greater than , Calzone refines by pushing to the stack all blocks in a covering for and . The blocks’ size is , which is the block size following the current block size , as determined by the planning component. The covering is obtained by retrieving from the covering database the covering and renaming the numbers in the blocks to range over the numbers in (instead of ), denoted as . If Calzone observes an empty stack, it returns robust. This analysis is proven sound and complete. To scale, Calzone parallelizes the analysis over multiple GPUs (for GPUPoly) and CPUs (for the MILP verifier). Technically, the first covering is split between the GPUs, each independently analyzes its assigned blocks and refines if needed.
Calzone’s planning
The planning determines the block sizes of the first covering and of the refinements’ coverings. These are given as a K strategy, a decreasing series , where and . Calzone predicts the K strategy that minimizes the overall analysis time using dynamic programming, defined over the analysis time of the first covering, the average fraction of blocks that will be refined, and the analysis time of the refined blocks. This computation requires GPUPoly’s success rate and average analysis time for neighborhoods , for all . These are estimated by sampling sets for every and submitting their neighborhood to GPUPoly.
Calzone’s covering database
As described, the analysis obtains coverings from a database. This database has been populated by obtaining well-optimized coverings from online resources and extending them for large values of and using general covering constructions. Because of these general constructions, the database’s coverings tend to be far from the Schönheim bound [29], the best-known general lower bound, especially for large values of (the image dimension). This inefficiency results in longer analysis, since more blocks are analyzed.
3 Our Approach: Covering Verification Designs
To scale Calzone’s analysis, it is crucial to reduce the number of blocks that are analyzed by GPUPoly or the MILP verifier. A dominant contributor to this number is the size of the first covering, for two reasons. First, the first covering is over a large (the image dimension), thus its size is significantly larger than the sizes of coverings added upon refinement, which are over significantly smaller (typically and at most ). Second, the first covering has an accumulative effect on the number of refinements, and consequently it dominates the analysis time. Reducing this size is theoretically possible by relying on finite geometry covering constructions [27, 1, 16], which are renowned for computing very small coverings. However, finite geometry coverings are limited to triples in which and are defined by related mathematical expressions over . In Calzone’s analysis, the first covering has to be defined over a given (the image dimension) and (the number of perturbed pixels). Thus, for some values of and , there is no finite geometry covering. For the other values, there are very few values for , leading to long analysis either because they are large and have a low success rate, triggering many refinements, or small and have very large coverings. We propose to tailor induced coverings for robustness analysis in order to leverage finite geometry coverings. To this end, we introduce a new type of a covering design, called a covering verification design (CVD). We next provide background on finite geometry coverings and induced coverings. We then define partially-induced coverings and our new covering type. We discuss its properties, its effectiveness, and the practical challenges in integrating it to verification.
Finite geometry coverings
Finite geometry covering constructions are widely known for obtaining small (sometimes optimal) coverings [27, 1, 16]. Popular finite geometry constructions rely on projective geometry (PG) or affine geometry (AG). We focus on PG, but our approach extends to AG. A PG construction views the problem of constructing a covering for a given (, , ) from a finite geometry point of view, where is the number of points in the geometry. It constructs coverings by computing flats (linear subspaces) of dimension , each containing points. Since every points from are contained in at least one flat [27], the flats provide a covering. Figure 2 shows the Fano plane, a well-known example. In this example, there are points, the flats are of dimension (the lines and the circle), each containing points. The set of flats forms a covering, where each flat is a block: . PG coverings exist for triples where and , for a prime power and (it also exists for , but then , which is unhelpful to our analysis). Because PG is restricted to such triples, Calzone cannot effectively leverage it for the first covering, whose and are given. This is because for common image dimensions (e.g., for MNIST and for CIFAR-10), there are no suitable and . Even if there are suitable and , there are very few possible values, which are unlikely to include or be close to an optimal value of . Thus, either they are smaller than an optimal , leading to larger coverings and a longer analysis time, or that they are larger than an optimal and have a lower success rate, leading to many refinements, resulting, again, in a longer analysis time. For example, for and , the only suitable values are and (i.e., ), namely there is only one triple for these values of and . In this triple, . Since , neighborhoods for which are not likely to be robust, thus such is likely to have a low success rate. Induced coverings [16] enable to leverage finite geometry coverings for other triples, as next explained.
Induced coverings
Given and , a covering can be induced to form a covering [16]. The induced covering is obtained in three steps. First, we select a subset of numbers of size , denoted , and remove every from every block in . This results in a set of blocks of different sizes that covers all subsets of of size [27, Lemma 1]. This follows since every subset of size is a subset of and thus there is such that . The first step removes from only numbers from and thus is contained in the respective block to after this step. The next two steps fix blocks whose size is not . The second step extends every block whose size is smaller than with numbers from . The third step refines every block whose size is larger than to multiple blocks of size that cover all of its subsets of size . This step significantly increases the number of blocks, unless the number of blocks larger than is negligible. We note that these steps provide a covering over the numbers in (i.e., ). A covering for can be obtained by renaming the numbers to range over .
Partially-induced covering
Our new covering design is an instance of a partially-induced covering. A partially-induced covering is the set of blocks obtained by the first step, where the blocks cover all subsets of of size and are of different sizes. For example, for the Fano plane and , the partially-induced covering is: , while for , it is: . Partially-induced coverings have two benefits in our setting: (1) by not extending blocks whose size is smaller than , we increase the likelihood that GPUPoly will prove their robustness, and (2) by not refining blocks whose size is larger than , we (a) preserve the number of blocks as in the original covering, (b) provide GPUPoly an opportunity to verify these blocks, and (c) rely on the optimal refinement sizes (computed by the dynamic programming) for blocks that GPUPoly fails proving robustness. Our covering design partially induces PG coverings, to obtain additional benefits for robustness verification.
Covering verification designs
Given the number of pixels and the number of pixels to perturb , a covering verification design (CVD) is the set of blocks obtained by partially inducing a PG covering , where , using a random set of numbers of size . The numbers in the blocks can later be renamed to range over . For example, since the Fano plane is a PG covering, the partially-induced coverings and are CVDs. A CVD has two important properties. First, it is a partially-induced covering and thus has all the aforementioned advantages in our setting. In particular, its size is equal to the size of the original covering, which is highly beneficial since CVD induces from PG coverings, known for their small size. Second, although different sets lead to different block size distributions, we prove that the mean block size and its variance are the same regardless of the choice of . Further, we identify closed-form expressions for them and show that the variance is bounded by the mean. For example, although the block size distributions of and are different, they have the same average block size () and the same variance (). This property has practical advantages: (1) it allows us to estimate the block size distribution (Section 4.2), and (2) since the variance is bounded by the mean, the smaller the mean block size, the less likely that there are very large blocks, which are less likely to be proven robust by GPUPoly. To prove this property, we rely on the fact that PG coverings (and AG coverings) are also a combinatorial design called a balanced incomplete block design (BIBD) [7, Part VII, Proposition 2.36]. We next describe BIBD and then state our theorem on its mean and variance.
BIBD
Given positive integers , a BIBD is a set of blocks, each is a subset of of size , such that every appears in blocks and every appear together in blocks. For example, the Fano plane is a BIBD with . This is because it has blocks, each block is a subset of of size , every number in appears in blocks and every two different numbers appear together in block. Given a BIBD with parameters , we define a partially-induced BIBD for by selecting a subset of numbers of size and removing every from every block in the BIBD (empty blocks or repetitive blocks are kept). While the distribution of the induced blocks’ sizes depends on , the mean block size and its variance depend only on .
Theorem 3.1
Given a -BIBD, for , and , for every of size , the mean and variance of the block sizes in the partially-induced BIBD satisfy:
-
1.
-
2.
-
3.
Proof
1. We prove . Since and is the number of occurrences of every number in all blocks, the sum of the sizes of the induced blocks is . By counting arguments, for a BIBD it holds that [7, Part II, Proposition 1.2], and so . That is, the sum of the induced blocks’ sizes is . The mean is obtained by dividing by the number of blocks : .
2.
We prove .
Let be a vector such that, for every , is the size of block in the partially-induced BIBD.
It can be written as , where represents the BIBD and the set , used for partially inducing the BIBD.
The matrix is a incidence matrix, where if is in block
and otherwise.
The vector is a -dimensional vector, where if and otherwise.
Thus, the average of the squares of the block sizes, denoted , is (3).
By the variance definition, .
Thus, we need to show: .
By counting arguments [7], we have and
.
Namely, it suffices to show:
.
By (3), we can show .
We prove by induction on that :
Base For , we show : Since ,
by definition of a BIBD, the vector of the induced blocks’ sizes has ones and the rest are zeros.
Thus, . Since , the claim follows.
Induction hypothesis Assume that the claim holds for every .
Step Let such that . Pick some and define of size .
We get , where is the standard unit vector. Thus:
-
•
By the induction hypothesis, .
-
•
Since can be viewed as for some of size 1, we get .
-
•
We show : Since is an incidence matrix of a BIBD, is the matrix with on the diagonal and elsewhere [7, Part II, Theorem 1.8]. Therefore, is a vector whose entries are except for the entry which is . The vector has ones and on the entry (since ). Thus, their dot product is .
Putting it all together: .
3. We show by showing that . Since , we show . We have and , thus we get . Since , we get . ∎
Size of covering verification designs
CVDs enable us to obtain coverings whose sizes are small, often close or better than their respective Schönheim bound. Given a CVD whose mean block size is a real number , we define its respective Schönheim bound as the bound for the covering design of . Note that this bound is not a lower bound on the size of the CVD, since the CVD can have blocks larger than and thereby be smaller than covering designs for . Still, comparing to this bound enables understanding how much smaller our coverings are compared to the coverings considered by Calzone, whose sizes are lower bounded by the Schönheim bound. Figure 3 shows the ratio of the sizes of our CVDs and their respective Schönheim bound and the ratio of the sizes of Calzone’s covering designs and their Schönheim bound. The comparison is for and (Figure 3(a)) and (Figure 3(b)). We compute CVDs from different PG coverings and the figure shows CVDs whose mean block size is at least . For Calzone, we show all coverings in its database. The plots demonstrate that typically the size of a CVD is smaller or equal to the Schönheim bound, and on average, the ratio is for and for . In contrast, Calzone’s coverings are significantly larger than the Schönheim bound, on average the ratio is for and for . The plots also show that Calzone has many more coverings than the number of CVDs. This is because Calzone relies on general techniques to compute coverings and thus it can generate a covering for every (except that it is limited to coverings with at most blocks). In contrast, our CVDs induce PG coverings and are thus limited to coverings whose mean block size is given by the expression given in Theorem 3.1, over and such that there is a PG covering for .
Challenge: memory consumption
The main challenge in computing CVDs is that it requires to compute a PG covering for large values of and , which poses a high memory overhead. To illustrate, in our experiments, CoVerD uses a CVD induced from a PG covering for . If CoVerD stored this covering in the memory, it would require GB of memory, assuming each number in a block takes a byte. To cope, CoVerD computes the partially-induced covering during the PG covering construction. However, even the partially-induced coverings can consume a lot of memory, since the number of blocks can be large. Calzone faced a similar challenge and coped by restricting the size of the covering designs to at most , which allowed it to keep all coverings in the covering database. While CoVerD could take a similar approach, this would prevent it from picking CVDs of larger size which overall may lead to a lower analysis time (since they will require fewer refinements). Instead, CoVerD generates a CVD on-the-fly and uses the covering database only for the refinements, which tend to require coverings of significantly smaller size than the first covering. Another advantage of building the CVD on-the-fly is that it enables CoVerD to analyze any classifier over any image dimension, without any special adaptation. This is in contrast to Calzone, which requires to extend its covering database upon every new image dimension .
4 CoVerD
In this section, we present CoVerD, our robustness verifier. We first describe our system and its components and then provide a running example.
4.1 Our System
Figure 4 shows CoVerD that, given an image classifier , an image with pixels, and the maximal number of perturbed pixels , returns whether is robust in the -ball of . We next describe its planning and analysis components.
Planning
The planning component consists of several steps. First, it samples sets of different sizes to estimate the success rate and average analysis time of their respective neighborhoods, like Calzone. Since CoVerD considers CVDs, it can observe larger block sizes than Calzone, thus the maximal sampled set size is , unlike in Calzone. Because of the larger bound, CoVerD is likely to observe many more values whose success rate is zero. To save execution time while still enabling to determine the success rate and average analysis time of large values, CoVerD reduces the number of samples after observing times values whose success rate is zero. Second, the planning component relies on Calzone’s dynamic programming for computing a K strategy, but uses it differently. Since CoVerD begins the analysis from a CVD consisting of different sized blocks, there is no single K strategy. Instead, it runs Calzone’s dynamic programming for every to define a function map** every set size to the best set size to use upon a refinement of a set of size . Then, the planning component iterates over every candidate CVD and picks the best CVD for the analysis. It picks between the candidates without constructing them, as the construction is time and memory intensive and we wish to execute it only for the chosen candidate. To pick the best candidate, it leverages two observations. First, a CVD candidate is uniquely defined by the parameters of the PG covering, (formally, its parameters are but is identical in all our PG coverings), so it suffices to pick a pair which can later be used to construct the CVD. Second, to predict the CVD with the minimal analysis time, only the block sizes are needed. In Section 4.2, we describe how to estimate a CVD’s block size distribution and estimate its analysis time , in order to predict the best CVD. Given the best candidate , it randomly samples an ordered set of indices from , which is a function of .
Analysis
After determining the best , , and the refinement map** , CoVerD continues to analyze the robustness of the classifier in the -ball of the given image . The analysis constructs the CVD on-the-fly block-by-block. Technically, there is a covering generator that constructs the blocks one-by-one. Every block is pushed to the stack of blocks to verify, and then the analysis proceeds as Calzone. That is, the block is popped, submitted to GPUPoly, and if needed, refinement is executed. After the block is verified (directly or by refinement), the next block in the CVD is obtained from the covering generator. We note that although CoVerD could use CVDs for refinements, the coverings for refinements are smaller than the first covering since these coverings are for triples where is typically few dozens and at most , whereas the first covering is for a triple where is the image dimension. Like Calzone, CoVerD parallelizes the analysis on GPUs. Thus, our covering generator generates disjoint parts of the covering, described in Section 4.3.
4.2 Choosing a Covering Verification Design
In this section, we describe how CoVerD predicts the CVD that enables CoVerD to minimize the overall analysis time. We begin with describing the CVD candidates, then describe how CoVerD estimates their block size distributions, and finally explain how CoVerD predicts the CVD leading to the minimal analysis time.
Candidates
A CVD candidate is defined by the PG covering from which it is partially-induced. Recall that a PG covering is defined for triples , where and for a prime power and . By Theorem 3.1, given a PG covering, the mean block size of the CVD has a closed-form expression . By this expression, given , as increases decreases, and given , as increases decreases. Further, this expression approaches for high values of or . Thus, to obtain a finite set of candidates, we provide a positive lower bound on , denoted MIN_K (our implementation sets it to ). That is, the finite set of candidates CoVerD considers is:
Estimating the block size distribution
For every CVD candidate, defined by , CoVerD estimates the distribution of its block sizes. While Theorem 3.1 provides expressions for the mean block size and the variance, it does not define the block size distribution. We empirically observe that our CVDs have the property that the distribution of their block sizes resembles a discrete approximation of a Gaussian distribution with mean and variance . The higher the mean and the number of blocks, the higher the resemblance. Figure 5(a) visualizes this resemblance for a CVD, with , induced from a PG with parameters , , and . We believe this resemblance exists because a CVD is partially-induced from a PG covering given a random set of numbers . This resemblance may not hold for other choices of , for example for the choice of proposed by [27], which compute a partially-induced covering whose maximal block size is bounded (unlike our CVD). Because of this resemblance, we model the block size as drawn from the Gaussian distribution with the true mean and variance . Even if this modeling is imprecise, in practice, it is sufficient to allow CoVerD identify the candidate CVD leading to the minimal analysis time. Formally, given a CVD candidate defined by , the distribution of the block sizes is , where is our estimation of the number of blocks of size in this CVD. We define the probability that a block size in this CVD is of size as: , where and is the cumulative distribution function (CDF) of a Gaussian distribution with mean and variance . The number of blocks is identical to the number of blocks in the PG covering, which has a closed-form expression [16]. Thus, the estimated number of blocks of size is: . To make the estimated number an integer, we define as the floor of and add with probability of the remainder: where . Figure 5(b) visualizes how close our estimation of the block size distribution is to the distribution of the CVD shown in Figure 5(a). We note that CoVerD considers a candidate and estimates its block size distribution only if its estimated number of overly large blocks (larger than MAX_K) is close to zero. Formally, it considers candidates that satisfy , where is a small number. This is the reason that consists of estimations only for blocks whose size is at most MAX_K.
Predicting the best CVD
Given the candidates and their estimated block size distributions, CoVerD chooses the CVD which will enable CoVerD to minimize the overall analysis time. To this end, it predicts for every candidate CVD its overall analysis time. The prediction relies on: (1) the estimated number of blocks of size , (2) the average analysis time of a block of size , denoted (given by the initial sampling), (3) the fraction of the non-robust blocks of size , which is one minus the success rate of , denoted (given by the initial sampling) and (4) the analysis time of refining a non-robust block of size , denoted (given by the dynamic programming, as defined in [30]). Similarly to Calzone’s dynamic programming, the analysis time is the sum of the analysis time of verifying all blocks in the CVD and the analysis time of the refinements of the non-robust blocks:
This computation ignores blocks of size less than since they do not cover any subset of size and need not be analyzed to prove robustness. After predicting the analysis time of every candidate, CoVerD picks the candidate with the minimal time.
4.3 Constructing a Covering Verification Design
In this section, we present our covering generator that computes a CVD. The covering generator operates as an independent process, one for every GPU, that outputs blocks a-synchronically. At every iteration, every GPU worker obtains a block from its covering generator, analyzes it with GPUPoly, and refines if needed. If the block is robust or its refinement does not detect an adversarial example, the GPU worker obtains the next block from the covering generator. The covering generator relies on the chosen CVD’s parameters and and the ordered set from the planning component. It computes the PG covering for (, , ) block-by-block and induces it to obtain a CVD. Generally, its construction follows the meta-algorithm of generating PG coverings described in [16]. The novel parts are our implementation of inducing blocks immediately upon generating them and partitioning them to enable their analysis to proceed in parallel over the available GPUs. We next describe the covering generator.
Algorithm 1 shows the algorithm of our covering generator. It takes as input the PG parameters , an ordered set of indices from (where ), and the GPU index . As described in Section 3, a PG construction for (, , ) views as the number of points in the geometry. Formally, given the finite field of order , we identify the points of the geometry as a subset of size (technically, these points are representatives of equivalence classes over , as explained in [16]). To later partially-induce the covering using , Algorithm 1 maps every index in to a unique point in and stores all points (column vectors) in a matrix (Algorithm 1). Then, Algorithm 1 begins to construct the PG covering by computing flats (linear subspaces) of dimension , each containing points. As described in [16], every block in the PG covering is a solution (a set of points in ) to independent linear equations over variables. Such a linear system can be represented as a full rank matrix, where its solutions are vectors in the matrix’s null space. Thus, to compute the blocks in the PG covering, Algorithm 1 defines a set of matrices , each is over , of dimension , and full rank (equal to ). Each matrix has exactly points in in its null space. These points form a PG block (a flat of dimension ). To avoid block duplication, the matrices in need to have different null spaces. Thus, Algorithm 1 considers matrices in reduced row echelon form, i.e., is all full rank matrices over in reduced row echelon form (Algorithm 1). The covering generator then iterates these matrices. To avoid a high memory overhead, the matrix is generated only upon reaching its index . If belongs to the disjoint part of the given GPU, its induced block is generated (Algorithm 1). To construct a PG block, one needs to compute all the points in the null space of . However, the generator requires only the partially-induced blocks. Thus, it immediately induces the block by obtaining all points , for , whose respective point belongs to the null space of . To this end, it defines as the multiplication of and (Algorithm 1), forms the induced block by identifying the points that are in the null space of (i.e., every satisfying ), and makes the induced block a subset of by map** every in the induced block to (Algorithm 1).
4.4 A Running Example
In this section, we describe a real execution of CoVerD, for an MNIST image, a fully-connected network (6200_PGD in Section 5), and . CoVerD begins with the planning component. It first estimates the success rate and average analysis time of blocks. For every , it samples blocks (subsets of ) of size and submits their neighborhood to GPUPoly. Based on all samples for , it estimates the success rate and the average analysis time. For instance, for the success rate is and the average analysis time is ms, while for they are and ms. Then, CoVerD runs Calzone’s dynamic programming to map every to the refinement size. For example, is mapped to and to . Next, CoVerD determines the CVD for the first covering, out of candidates. For each candidate, it predicts the block size distribution and the respective overall analysis time of this candidate. To this end, it computes the mean, variance, and number of blocks using the closed-form expressions. For example, the CVD of the candidate has mean block size , variance and blocks. The CVD of has mean block size , variance , and blocks. Although the second candidate has less than half the number of blocks of the first candidate, CoVerD predicts that using the first candidate will enable a faster analysis. This is because its success rate is significantly higher and thus it will require fewer refinements (e.g., the success rate of its mean block size is , whereas the second candidate’s success rate of the mean block size is ). The estimated analysis times (in minutes) are and . The last step of the planning component samples an ordered set of size (the number of pixels in the MNIST image) from . In total, the planning component takes 63.5 seconds.
Then, CoVerD continues to the analysis component. It starts by creating eight instances of the covering generator (Algorithm 1), one for each GPU. A covering generator creates blocks for its GPU one-by-one, given , , and . For every CVD block , the GPU worker defines its neighborhood and submits to GPUPoly. If GPUPoly verifies successfully, the next CVD block is obtained. If GPUPoly fails proving robustness, is refined. As example, if a block of size is refined, the analysis pushes to the stack all blocks in the covering , which is the covering for that is in the covering database, where the numbers are renamed to range over the numbers in . In this example, GPUPoly is invoked times, where of these calls are for blocks in the CVD. The maximal size of block submitted to GPUPoly is and the minimal size is . In particular, CoVerD did not submit any block of size (i.e., there are no calls to the MILP verifier). The analysis takes 23.49 minutes, which is only higher than the estimated time.
5 Evaluation
In this section, we describe the experimental evaluation of CoVerD on multiple datasets and networks and compare it to Calzone.
Implementation and setup
We implemented CoVerD 111https://github.com/YuvShap/CoVerD as an extension of Calzone222https://github.com/YuvShap/calzone. Experiments ran on a dual AMD EPYC 7713 server, 2TB RAM, eight NVIDIA A100 GPUs and Ubuntu 20.04.1. We evaluate CoVerD on the networks evaluated by Calzone, whose architectures are described in ERAN333https://github.com/eth-sri/eran. We consider networks trained for popular image datasets: MNIST and Fashion-MNIST, consisting of greyscale images, and CIFAR-10, consisting of colored images. CoVerD’s hyper-parameters are: the maximal block size is , the number of samples is initially and after failures, it is reduced to , and the bound on the estimated number of overly large blocks is . Our covering database, used for the refinement steps, contains coverings for , . The covering sizes are restricted to at most blocks. This limitation is stricter than Calzone, which limited to , but in practice this is unnoticeable since CoVerD only uses the coverings for refinements, and even Calzone typically refines to coverings whose size is at most . Like Calzone, the database consists of coverings computed by extending coverings from the La Jolla Covering Repository Tables444https://ljcr.dmgordon.org/cover/table.html using construction techniques from [16, Section 6.1]. Additionally, our database includes finite geometry coverings (for , ) and extends coverings using the dynamic programming of [16, Section 5]. Like Calzone, We ran CoVerD with eight GPUPoly instances and five MILP instances, except for the CIFAR-10 network where it ran 50 MILP instances. For the matrix multiplication over finite fields (Algorithm 1), CoVerD relies on an effective library [18] and considers only prime numbers for (since matrix multiplication is too slow for prime powers).
Comparison to Calzone
We begin by evaluating CoVerD on Calzone’s benchmarks (i.e., the same networks, images and timeouts) for . Figure 6 shows the comparison for the most challenging benchmarks of Calzone, and Figure 7 shows comparisons for (the plots for are shown in Appendix 0.A). For a given network and , the plot shows the execution time in minutes of CoVerD and Calzone for every -ball. The -axis orders the -balls by CoVerD’s output: non-robust (in light red background), robust (in light green background), and timeout (in light blue background, e.g., Figure 7, top). Within each section, the -balls are sorted by their execution time for clearer visuality. Timeouts, of CoVerD or Calzone, are shown by bars reaching the red horizontal line. The lower part of each bar shows in a lighter color the execution time of the initial sampling (unless it is too short to be visible in the plot). The sampling time is highlighted since Calzone and CoVerD sample slightly differently: Calzone samples sets of size , for every , while CoVerD samples up to and reduces the number of samples after observing ten values whose average success rate is zero. We note that the other computations of the planning component take a few seconds. The plots’ titles include the speedup in the average analysis time of CoVerD over Calzone for non-robust -balls (NR) and for robust -balls (R).
The plots show that, on the most challenging benchmarks (Figure 6), CoVerD is always faster than Calzone, except for two non-robust -balls which CoVerD completes their analysis within 140 seconds. In the plots of Figure 7, CoVerD is always faster than Calzone except for thirteen -balls whose analysis terminates within seven minutes by both verifiers. In the other plots (Figure 9 in Appendix 0.A), where , Calzone is sometimes faster, but in these cases the analysis time is typically short. In other words, the significance of CoVerD is in shortening the analysis time of -balls with long analysis time. On average, CoVerD is faster than Calzone in verifying robust -balls by 1.3x for , by 2.8x for , and by 5.1x for .
Challenging benchmarks
Next, we show more challenging benchmarks than Calzone. We evaluate the robustness of three networks for -balls with larger values of than Calzone considers, for and for (we remind that Calzone is evaluated for ). Similarly to Calzone’s most challenging benchmarks, these benchmarks evaluate CoVerD for ten images (misclassified images are discarded) and a five hour timeout. Figure 8 shows CoVerD’s analysis time. CoVerD completes the analysis for -balls. Further, it verifies robustness in some -balls within minutes. As before, CoVerD is significantly faster for non-robust -balls.
We provide additional statistics on CoVerD in Appendix 0.A.
6 Related Work
In this section, we discuss the closest related work.
Robustness verification of neural networks
Many works propose robustness verifiers for neural networks. Most works focus on local robustness in neighborhoods, defined by a series of intervals [25, 33, 31, 13, 21, 2, 36, 35, 12]. Some verifiers provide a complete analysis, i.e., they determine whether a network is robust in the given neighborhood [33, 21, 12]. These approaches typically rely on constraint solving (SAT/SMT solvers or MILP solvers) and thus they often do not scale to large networks. Incomplete verifiers scale the analysis by over-approximating the non-linear computations of the network (e.g., the activation functions) by linear approximations or abstract domains [25, 31, 13, 35]. Several local robustness verifiers address -balls, e.g., by computing a bound on the network’s global or local Lipschitz constant [22, 19], or -balls [37, 40]. Other approaches analyze robustness in -balls for using randomized smoothing [6, 38, 23, 28, 11], providing probabilistic guarantees. To the best of our knowledge, Calzone [30] is the first work to deterministically verify local robustness in -balls. Other works prove robustness in neighborhoods defined by high-level features [20, 24, 3].
Covering and combinatorial designs
CVD is related to several combinatorial designs: the combinatorial design defined by [27], covering designs [16] and balanced incomplete block designs [7]. Covering designs, in particular finite geometry coverings, have been leveraged in various domains, including file information retrieval [27], file organization [1] and coding theory [5]. General combinatorial designs have also been leveraged in various domains in computer science [8].
7 Conclusion
We present CoVerD, an robustness verifier for neural networks. CoVerD boosts the performance of a previous robustness verifier by employing several ideas. First, it relies on a covering verification design (CVD), a new combinatorial design partially inducing a projective geometry covering. Second, it chooses between candidate CVDs without constructing them but only predicting their block size distribution. Third, it constructs the chosen CVD on-the-fly to keep the memory overhead minimal. We evaluate CoVerD on fully-connected and convolutional networks. We show that it boosts the performance of proving a network’s robustness to at most perturbed pixels on average by 2.8x, for , and by 5.1x, for . For , CoVerD sometimes proves robustness within minutes.
References
- [1] Abraham, C., Ghosh, S., Ray-Chaudhuri, D.: File organization schemes based on finite geometries. Information and Control 12(2), 143–163 (1968)
- [2] Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI (2019)
- [3] Balunovic, M., Baader, M., Singh, G., Gehr, T., Vechev, M.T.: Certifying geometric robustness of neural networks. In: Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems, NeurIPS (2019)
- [4] Carlini, N., Wagner, D.A.: Towards evaluating the robustness of neural networks. In: IEEE Symposium on Security and Privacy, SP (2017)
- [5] Chan, A., Games, R.: (n,k,t))-covering systems and error-trap** decoding (corresp.). IEEE Transactions on Information Theory 27(5), 643–646 (1981)
- [6] Cohen, J., Rosenfeld, E., Kolter, J.Z.: Certified adversarial robustness via randomized smoothing. In: Proceedings of the 36th International Conference on Machine Learning, ICML. vol. 97. PMLR (2019)
- [7] Colbourn, C.J., Dinitz, J.H. (eds.): Handbook of Combinatorial Designs. Chapman and Hall/CRC, 2nd edn. (2006). https://doi.org/10.1201/9781420010541
- [8] Colbourn, C.J., van Oorschot, P.C.: Applications of combinatorial designs in computer science. ACM Comput. Surv. 21(2), 223–250 (jun 1989)
- [9] Croce, F., Andriushchenko, M., Singh, N.D., Flammarion, N., Hein, M.: Sparse-rs: A versatile framework for query-efficient sparse black-box adversarial attacks. In: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI , The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI. AAAI Press (2022)
- [10] Croce, F., Hein, M.: Mind the box: l-apgd for sparse adversarial attacks on image classifiers. In: Proceedings of the 38th International Conference on Machine Learning, ICML. PMLR (2021)
- [11] Dvijotham, K.D., Hayes, J., Balle, B., Kolter, J.Z., Qin, C., György, A., Xiao, K., Gowal, S., Kohli, P.: A framework for robustness certification of smoothed classifiers using f-divergences. In: 8th International Conference on Learning Representations, ICLR. OpenReview.net (2020)
- [12] Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Automated Technology for Verification and Analysis - 15th International Symposium, ATVA. Lecture Notes in Computer Science, vol. 10482. Springer (2017)
- [13] Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: IEEE Symposium on Security and Privacy, SP (2018)
- [14] Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press (2016), http://www.deeplearningbook.org
- [15] Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: 3rd International Conference on Learning Representations, ICLR (2015)
- [16] Gordon, D.M., Kuperberg, G., Patashnik, O.: New constructions for covering designs. J. COMBIN. DESIGNS 3, 269–284 (1995)
- [17] Grosse, K., Papernot, N., Manoharan, P., Backes, M., McDaniel, P.D.: Adversarial perturbations against deep neural networks for malware classification. CoRR abs/1606.04435 (2016)
- [18] Hostetter, M.: Galois: A performant NumPy extension for Galois fields (11 2020), https://github.com/mhostetter/galois
- [19] Huang, Y., Zhang, H., Shi, Y., Kolter, J.Z., Anandkumar, A.: Training certifiably robust neural networks with efficient local lipschitz bounds. In: Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems NeurIPS (2021)
- [20] Kabaha, A., Drachsler-Cohen, D.: Boosting robustness verification of semantic feature neighborhoods. In: Static Analysis - 29th International Symposium, SAS. Lecture Notes in Computer Science, vol. 13790. Springer (2022)
- [21] Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Computer Aided Verification - 29th International Conference, CAV (2017)
- [22] Leino, K., Wang, Z., Fredrikson, M.: Globally-robust neural networks. In: Proceedings of the 38th International Conference on Machine Learning, ICML. Proceedings of Machine Learning Research, vol. 139. PMLR (2021)
- [23] Li, B., Chen, C., Wang, W., Carin, L.: Certified adversarial robustness with additive noise. In: Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems, NeurIPS (2019)
- [24] Mohapatra, J., Weng, T., Chen, P., Liu, S., Daniel, L.: Towards verifying robustness of neural networks against A family of semantic perturbations. In: IEEE/CVF Conference on Computer Vision and Pattern Recognition, CVPR (2020)
- [25] Müller, C., Serre, F., Singh, G., Püschel, M., Vechev, M.T.: Scaling polyhedral neural network verification on gpus. In: Proceedings of Machine Learning and Systems MLSys (2021)
- [26] Papernot, N., McDaniel, P.D., Jha, S., Fredrikson, M., Celik, Z.B., Swami, A.: The limitations of deep learning in adversarial settings. In: IEEE European Symposium on Security and Privacy, EuroS&P (2016)
- [27] Ray-Chaudhuri, D.K.: Combinatorial information retrieval systems for files. SIAM J. Appl. Math. 16(5), 973–992 (sep 1968)
- [28] Salman, H., Li, J., Razenshteyn, I.P., Zhang, P., Zhang, H., Bubeck, S., Yang, G.: Provably robust deep learning via adversarially trained smoothed classifiers. In: Wallach, H.M., Larochelle, H., Beygelzimer, A., d’Alché-Buc, F., Fox, E.B., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems, NeurIPS. pp. 11289–11300 (2019)
- [29] Schönheim, J.: On coverings. Pacific Journal of Mathematics 14(4), 1405 – 1411 (1964)
- [30] Shapira, Y., Avneri, E., Drachsler-Cohen, D.: Deep learning robustness verification for few-pixel attacks. Proc. ACM Program. Lang. 7(OOPSLA1) (2023)
- [31] Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. PACMPL 3(POPL) (2019)
- [32] Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. In: 2nd International Conference on Learning Representations, ICLR (2014)
- [33] Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In 7th International Conference on Learning Representations, ICLR (2019)
- [34] Todorov, D.: Combinatorial coverings. Ph.D. thesis, PhD thesis, University of Sofia, 1985 (1985)
- [35] Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C., Kolter, J.Z.: Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems (2021)
- [36] Wu, H., Ozdemir, A., Zeljic, A., Julian, K., Irfan, A., Gopinath, D., Fouladi, S., Katz, G., Pasareanu, C.S., Barrett, C.W.: Parallelization techniques for verifying neural networks. In: Formal Methods in Computer Aided Design, FMCAD. IEEE (2020)
- [37] Wu, Y., Zhang, M.: Tightening robustness verification of convolutional neural networks with fine-grained linear approximation. In: Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI. pp. 11674–11681. AAAI Press (2021)
- [38] Yang, G., Duan, T., Hu, J.E., Salman, H., Razenshteyn, I.P., Li, J.: Randomized smoothing of all shapes and sizes. In: Proceedings of the 37th International Conference on Machine Learning, ICML. Proceedings of Machine Learning Research, vol. 119. PMLR (2020)
- [39] Yuviler, T., Drachsler-Cohen, D.: One pixel adversarial attacks via sketched programs. Proc. ACM Program. Lang. 7(PLDI) (2023)
- [40] Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems, NeurIPS (2018)
Appendix 0.A Additional Results
In this section, we provide additional experimental results.
Figure 9 compares CoVerD and Calzone for different networks and .
Dataset | Network | GPUPoly | MILP | |||
---|---|---|---|---|---|---|
R | NR | R | NR | |||
MNIST | 6200_PGD | 3 | 46565.93 | 12939.12 | 2.99 | 34.88 |
4 | 3468151.25 | 637245.50 | 363.00 | 3567.00 | ||
ConvSmall | 3 | 20693.16 | 5822.55 | 0.03 | 2.00 | |
4 | 615418.88 | 221191.00 | 0.03 | 8.17 | ||
5 | 3095356.00 | 36720.00 | 0.00 | 18.00 | ||
ConvSmallPGD | 3 | 9937.48 | 7689.20 | 0.01 | 3.50 | |
4 | 171847.55 | 13430.30 | 0.00 | 3.90 | ||
5 | 1730609.17 | 35571.33 | 0.00 | 1.67 | ||
6 | 5856433.00 | 29218.33 | 0.00 | 3.67 | ||
ConvMedPGD | 3 | 10617.40 | 11101.56 | 0.01 | 2.67 | |
4 | 274938.91 | 59813.17 | 0.05 | 4.33 | ||
5 | 3773350.00 | 13614.00 | 0.00 | 5.00 | ||
ConvBig | 3 | 217192.22 | - | 2.33 | - | |
FASHION | ConvSmallPGD | 3 | 25196.52 | 15810.41 | 1.76 | 48.65 |
4 | 644109.33 | 66506.73 | 1.80 | 67.45 | ||
5 | 2714415.20 | 976522.50 | 33.00 | 8.00 | ||
ConvMedPGD | 3 | 69537.46 | 42235.61 | 8.25 | 35.33 | |
4 | 1560073.43 | 60455.00 | 0.00 | 58.00 | ||
CIFAR-10 | ConvSmallPGD | 3 | 5768227.40 | 92157.75 | 1933.60 | 1509.75 |
We next study the number of completed analysis tasks performed by GPUPoly and the MILP verifier. For robust -balls, this number is equal to the number of tasks CoVerD submits to these verifiers. For non-robust -balls, this number may be smaller than the number of submitted tasks, since CoVerD terminates when an adversarial example is found. We note that CoVerD, like Calzone, submits to the MILP verifier unique blocks (of size ) to avoid repeating the same analysis tasks in the MILP verifier, which is significantly slower than GPUPoly. Table 1 shows the average number of completed analysis tasks for robust -balls and non-robust -balls. As expected, the number of completed tasks of the MILP verifier is significantly smaller than the number of completed tasks of GPUPoly, especially for robust balls. This is because the MILP verifier is executed for unique blocks of size that GPUPoly failed to verify.
Next, we justify the value chosen for MAX_K, the upper bound on the size of blocks in the CVD candidates. This hyper-parameter has been introduced by Calzone to limit the of the considered coverings. Limiting the maximal value of is required for the covering database, the sampling, and the dynamic programming. This limitation should not impact Calzone’s performance, because overly large blocks are unlikely to be robust and thus are unhelpful to the analysis. In Calzone, since for most networks and images, larger blocks are typically not robust. To illustrate, Figure 10 shows the success rate of GPUPoly for the ConvSmallPGD network trained for MNIST and neighborhoods as a function of , for eight values of (the first eight images in the MNIST test set). We note that ConvSmallPGD has the highest success rates for large values of , among our evaluated networks. For every image, we compute the success rate of every by sampling sets of size and submitting to GPUPoly. The success rate is the fraction of verified sets. The plot shows that the success rates are very low for , justifying Calzone’s choice of MAX_K. Unlike Calzone, CoVerD computes for the first covering a CVD, consisting of blocks of different sizes. A CVD whose mean block size is contains blocks larger than . To allow CoVerD to consider CVDs with mean block sizes similar to those in Calzone’s coverings, we increase MAX_K to . This number enables CoVerD to consider CVDs with mean block size . This follows since, by Theorem 3.1, the standard deviation of the block size distribution of a CVD with mean block size is at most . Thus, the probability that a CVD with mean has a block of size larger than is negligible, since such sizes are greater than the mean by at least x the standard deviation.
Lastly, we justify the value of . As described, CoVerD’s sampling is different from Calzone’s sampling. Calzone samples sets of pixels of size for every . CoVerD begins by sampling sets of pixels of size , for every and decreases to when detecting values of whose estimated success rate is zero. Technically, the sampling is distributed among the eight GPUs, each samples independently. Each GPU samples sets of size for every from to , in an increasing order. After a GPU observes values of whose estimated success rate is zero, it sets . By decreasing , the sampling time decreases while still enabling CoVerD to estimate the success rate and average analysis time of large values of . We evaluate CoVerD’s sampling over a single image and four networks. Table 2 shows the minimal where at least one GPU decreases , denoted , and the minimum where all GPUs decrease , denoted . We compare CoVerD’s estimated success rates to the estimation of Calzone’s sampling extended to , relying on samples for every . For all networks, the estimated success rates of of CoVerD and Calzone are zero, except for MNIST ConvSmall and , where Calzone’s sampling estimated the success rate as . Figure 11 shows the estimated analysis time of every by CoVerD’s sampling and by Calzone’s sampling. The dashed vertical lines in the plots indicate . The plots show that the estimated analysis time of CoVerD is very close to Calzone’s estimated analysis time, despite of sampling significantly fewer sets. As expected, its estimations are noisier for . The benefit of CoVerD’s sampling is that it significantly reduces the overall sampling time, on average by x and up to x compared to Calzone’s sampling (extended to ).
Dataset | Network | ||
---|---|---|---|
MNIST | 6200_PGD | 69 | 72 |
ConvSmall | 94 | 99 | |
ConvMedPGD | 90 | 94 | |
FASHION | ConvMedPGD | 62 | 65 |