Fast Geometric Projections for
Local Robustness Certification

We propose the Fast Geometric Projections (FGP) algorithm, which takes a model, $F$, an input, $x$, and a bound, $\epsilon$, and either proves that Equation 1 is satisfied (i.e., $\epsilon$-local robustness), finds an adversarial input at distance less than $\epsilon$ from $x$, or returns $\mathsf{unknown}$. Our algorithm assumes $F(x)=\text{argmax}\{f(x)\}$, where $f:\mathbb{R}^{m}\to\mathbb{R}^{n}$ is the function computed by a neural network composed of linear transformations with ReLU activations (i.e., $f$ is a feed-forward ReLU network).

The algorithm relies on an analysis of all possible activation regions around $x$. An activation region is a maximal set of inputs having the same activation pattern of ReLU nonlinearities.

Formally, let $f_{u}(x)$ denote the pre-activation value of neuron $u$ in network $F$ when evaluating $x$. We say that neuron $u$ is activated if $f_{u}(x)\geq 0$. An activation pattern, $A$, is a Boolean function over neurons that characterizes whether each neuron is activated. Then the activation region, $\bar{A}$, associated with pattern $A$ is the set of inputs that realize $A$: $\bar{A}:=\{x\mid\forall u.(f_{u}(x)\geq 0)\iff A(u)\}$.

Because we assume that $F$ is a piecewise-linear composition of linear transformations and ReLU activations, we can associate the activation status $A(u)$ of any neuron with a closed half-space of $\mathbb{R}^{m}$ (Jordan et al., 2019). The activation constraint, $C_{u}$, for neuron $u$ and pattern $A$ is the linear inequality $w_{u}^{T}x+b_{u}\leq 0$, where $w_{u}$ and $b_{u}$ satisfy $\forall x\in\mathbb{R}^{m}.w_{u}^{T}x+b\leq 0\iff A(u)$. The coefficients, $w_{u}$ are equal to the gradient of $f_{u}$ with respect to its inputs, evaluated at a point in $\bar{A}$. Crucially, because the gradient is the same at every point in $\bar{A}$, the constraints can be computed from the activation pattern alone via backpropagation. More details on this computation are given in Appendix B.

The intersection of these constraints yields the activation region $\bar{A}$, and the facets of $\bar{A}$ correspond to the non-redundant constraints. The convexity of activation regions follows from this observation, as does the fact that the decision boundaries are also linear constraints of the form $f(x)_{i}\geq f(x)_{j}$ for classes $i$ and $j$.

The FGP algorithm performs a search of all activation regions that might be at distance less than $\epsilon$ from $x$. We begin by analyzing the region, $\bar{A}_{0}$, associated with the activation pattern of the input, $x$, as follows.

First, we check to see if $\bar{A}_{0}$ contains a decision boundary, $C$, that is at distance less than $\epsilon$ from $x$; if so, we take the projection, $p$, from $x$ onto $C$. Intuitively, the projection is an input satisfying $C$ that is at minimal distance from $x$, i.e., $\forall x^{\prime}.C(x^{\prime})\Longrightarrow\|x-p\|\leq\|x-x^{\prime}\|$. Similarly we define the distance, $d$, from $x$ to a constraint or decision boundary, $C$, as $d(x,C):=\min_{x^{\prime}:C(x^{\prime})}{\|x-x^{\prime}\|}$, i.e., $d$ is the distance from $x$ to its projection onto $C$. If $p$ does not have the same class as $x$ according to $F$ (or lies directly on the decision boundary between classes), then $p$ is an adversarial example. If $p$ has the same class as $x$, it means that the projection to the decision boundary is outside of the activation region we are currently analyzing; however, this is not sufficient to conclude that no point on the decision boundary is inside both the current activation region and the $\epsilon$-ball (see Figure 1(b)). Therefore, we return $\mathsf{unknown}$.

Otherwise, we collect all activation constraints in $\bar{A}_{0}$; there is one such activation constraint per neuron $u$ in the network; thus each constraint corresponds to the neighboring region, $\bar{A}^{u}_{0}$, which has the same activation pattern as $\bar{A}_{0}$, except with neuron $u$ flipped, i.e., $A_{0}(u^{\prime})\neq A_{0}^{u}(u^{\prime})\Longleftrightarrow u=u^{\prime}$. For each constraint $C_{u}$, we check whether it might be at distance less than $\epsilon$ from $x$ using a geometric projection. Although $C_{u}$ is only valid in the polytope corresponding to the activation region $\bar{A}_{0}$, we compute the distance to the hyperplane corresponding to the infinite prolongation of $C_{u}$. As such, we only obtain a lower bound on the distance from $x$ to $C_{u}$. If the computed distance is smaller than $\epsilon$, we enqueue the corresponding activation region if it has not been searched yet. Thus the queue contains unexplored regions that might be at distance less than $\epsilon$ from $x$. The algorithm continues to analyze each enqueued region in the same way, each explored region enqueuing neighbouring regions that might be at distance less than $\epsilon$ from $x$, until the queue is empty. Exhausting the queue means that we did not find any adversarial examples in any activation region that might intersect with the $\epsilon$-ball centered at $x$. We therefore conclude that $x$ is locally $\epsilon$-robust. An illustration of a simple execution of this algorithm is shown in Figure 1(a).

To improve the performance and precision of our algorithm, we use several additional heuristics.

Batching. The gradient backpropagations for computing constraints and the dot product projections for calculating distances lend themselves well to batching on the GPU. In our implementation we dequeue multiple elements from the queue at once and calculate the constraints and constraint distances for the corresponding regions in parallel, leading to a speedup of up to 2x on large examples for a well-chosen batch size ($\sim$10-100).

Caching Intermediate Computations. We observe that activation constraints for the first layer are invariant across all regions, as there is no earlier neuron to depend on. Thus, we can precompute all such constraints once for all inputs to be analyzed.

Exploring the Full Queue. If the analysis of a decision boundary is inconclusive, the FGP algorithm, as presented, stops and returns $\mathsf{unknown}$. We also implement a variant where we instead record the presence of an ambiguous decision boundary but continue exploring other regions in the queue. If we empty the queue after unsuccessfully analyzing a decision boundary, we nevertheless return $\mathsf{unknown}$. However, oftentimes a true adversarial example is found during the continued search, allowing us to return $\mathsf{not\_robust}$ conclusively.

Table 1 displays the results of experiments evaluating the impact of exploring the entire search queue instead of stopping at the first decision boundary (as described in Section 2.1). The experimental results show that this heuristic decreases the number of $\mathsf{unknown}$ results by approximately $50\%$ while only having a minor impact on the speed of the execution. Moreover, we reduce the number of $\mathsf{unknown}$ results to the extent that we recover the results obtained by GeoCert in every instance for which GeoCert terminates, except 3 non-robust points on mnist40x3, while nevertheless performing our analysis two to three orders of magnitude more quickly.

We now consider the related problem of finding a lower bound on the local robustness of the network. A variant of the FGP algorithm can provide certified lower bounds by using a priority queue; constraints are enqueued with priority corresponding to their distance from $x$, such that the closest constraint is always at the front of the queue. We keep track of the current certified lower bound in a variable, $\beta$. At each iteration, we set $\beta$ to the maximum of the old $\beta$ and the distance from $x$ to the constraint at the front of the queue.

The algorithm terminates either when all constraints at distance less than the initially specified $\epsilon$ were handled, or when a decision boundary for which the initial algorithm returns $\mathsf{unknown}$ or $\mathsf{not\_robust}$ is found. In the first case, we return $\epsilon$; in the second, we return the value stored in $\beta$ at this iteration.

The proof of this variant is similar to the proof of the FGP algorithm. It relies on the following loop invariant, which we prove in Appendix A.2.

We first compare the efficiency of our implementation to that of other tools certifying local robustness. GeoCert (Jordan et al., 2019) and MIP (Tjeng & Tedrake, 2017) are the tools most comparable to ours as they are able to exactly check for robustness with respect to the $\ell_{2}$ norm. We used commit hash 8730aba for GeoCert, and v0.2.1 for MIP. Specifically, we compare the median run time over the analyses of each of the selected 100 instances, the number of examples on which each tool terminates, the result of the analyses that terminate, and the corresponding verified robust accuracy (VRA), i.e., the fraction of points that were both correctly classified by the model and verified as robust. In addition, we report an upper bound on the VRA for each model, obtained by running PGD attacks (hyperparameters included in Appendix C) on the correctly-classified points on which every method either timed out or reported $\mathsf{unknown}$. Results are given for an $\ell_{2}$ norm bound of $\epsilon=0.25$, with a computation budget of two minutes per instance. The results for these experiments are presented in Table 2(a).

We observe that FGP always outperforms GeoCert by two to three orders of magnitude, without sacrificing precision; i.e., we rarely return $\mathsf{unknown}$ when GeoCert terminates. MIP frequently times out with a time budget of 120 seconds, indicating that we are faster by at least four orders of magnitude. This is consistent with the 100 to 1000 seconds per solve on a MNIST model with three hidden layers of 20 neurons each reported by Tjeng & Tedrake (2017); their technique performs best on the $\ell_{1}$ or $\ell_{\infty}$ norms. In addition, we find that FGP consistently verifies the highest fraction of points, and yields the best VRA. Moreover, on mnist20x3, FGP comes within 2 percentage points of the VRA upper bound. This suggests that FGP comes close to verifying every robust instance on this model.

We now evaluate the variant of our algorithm computing certified lower bounds on the robustness radius (Section 2.3). To this end, we compare the performance of our approach to FastLin (Weng et al., 2018), which is designed to provide quick, but potentially loose lower bounds on the local robustness of large ReLU networks. We compare the certified lower bound reported by our implementation of FGP after 60 seconds of computation (on models large enough such that FGP rarely terminates in 60 seconds) to the lower bound reported by FastLin; FastLin always reported results in less than two seconds on the models analyzed. The results are presented in Table 2(b). The mean lower bound is reported for both methods, and we observe that on the models tested, FGP is able to find a better lower bound on average, though it requires considerably more computation time.

Because the optimal bound may vary between instances, we also report the median ratio of the lower bounds obtained by the two methods on each individual instance. Here we see that FastLin may indeed be quite loose, as on a typical instance it achieves as low as 4% and only as high as 69% of the bound obtained by FGP. Finally, we note that when FGP terminates by finding a decision boundary, if the projection onto that boundary is a true adversarial example, then the lower bound is tight. In our experiments, there were few such examples — three on fmnist500x4 and one on fmnist1000x3 — however, in these cases, the lower bound obtained by FastLin was very loose, achieving 4-15% of the optimal bound on fmnist500x4, and only 0.8% of the optimal bound on fmnist1000x3. This suggests that while FastLin has been demonstrated to scale to large networks, one must be careful with its application, as there may be cases in which the bound it provides is too conservative.

The only aspect of FGP that depends on the norm is the projection and the projected distance computation, making our approach highly modular with respect to the norm. As such, we added support for $\ell_{\infty}$ robustness certification by providing a projection and a projected distance computation in FGP.

In this section, we compare the efficiency of this implementation to GeoCert (Jordan et al., 2019) and ERAN (Singh et al., 2019a). ERAN uses abstract interpretation to analyze networks using conservative over-approximations. As such, the analysis can certify that an input is robust, but can yield false positives when flagging an input as not robust. In this evaluation, we use the DeepPoly abstract domain, and the complete mode of ERAN which falls back on constraint solving when an input is classified as not robust.

Our experimental setup is similar to the one presented in Section 3.1. For each network, we arbitrarily pick 100 inputs from the test set and report the median analysis time of each tool. We give each tool a time budget of 120 seconds per input. We report the number of instances on which each tool terminates within this time frame, as well as the results of the analyses that terminate. Results are given in Table 3 for an $\ell_{\infty}$ norm bound of $\epsilon=0.01$, which contains roughly the same volume as the $\ell_{2}$ ball used in most of our evaluation.

We refer to each model by the dataset it was trained on, followed by the architecture of the hidden layers. For example, “mnist20x3” refers to a model trained on MNIST with 3 hidden layers of 20 neurons each. Models marked with an asterisk were trained with MMR (Croce et al., 2019); other models were trained using PGD adversarial training (Madry et al., 2018).

We observe that we consistently outperform GeoCert by about two orders of magnitude, both on models trained with MMR and using adversarial training. On models trained for robustness (upper rows of Table 3), FGP is 0.5x to 5x faster than ERAN. In particular, FGP seems to scale better to deeper networks, while ERAN performs better on wider networks. Interestingly, ERAN does not benefit as much from MMR training as FGP and GeoCert. On large models trained with MMR, our tool is one to two orders of magnitude faster than ERAN, and ERAN is only about 2x faster than GeoCert.

Finally, while FGP is able to determine robustness for almost all inputs deemed robust by GeoCert or ERAN, it struggles to find adversarial examples for non-robust points, which results in a higher number of $\mathsf{unknown}$ cases compared to the $\ell_{2}$ variant. This is not highly surprising, as projections are better-suited to the Euclidean space than to $\ell_{\infty}$ space. While the projection in Euclidean space is unique, this is not always the case in $\ell_{\infty}$ space; we pick one arbitrary projection which thus might not lead to an adversarial example.