A Dual Approach to Scalable Verification of Deep Networks

INTRODUCTION

Neural networks and deep learning have revolutionized machine learning achieving state of the art performance on a wide range of complex prediction tasks (Krizhevsky et al., 2012; Goodfellow et al., 2016). However, in recent years, researchers have observed that even state of the art networks can be easily fooled into changing their predictions by making small but carefully chosen modifications to the input data (known as adversarial perturbations) (Szegedy et al., 2013; Kurakin et al., 2016; Carlini and Wagner, 2017a; Goodfellow et al., 2014; Carlini and Wagner, 2017b). While modifications to neural network training algorithms have been proposed to mitigate this phenomenonMadry et al. (2018), a comprehensive solution that is fully robust to adversarial attacks remains elusive (Carlini and Wagner, 2017b; Uesato et al., 2018).

Neural networks are typically tested using the standard machine learning paradigm: If the performance (accuracy) of the network is sufficiently high on a holdout (test) set that the network did not have access to while training, the network is deemed acceptable. This is justified by statistical arguments based on an i.i.d. assumption on the data generating mechanism, that is each input output pair is generated independently from the same (unknown) data distribution. However, this evaluation protocol is not sufficient in domains with critical safety constraints (Marston and Baca, 2015). In these cases, we may require a stronger test: for example, we may require that the network is robust against adversarial perturbations within certain bounds.

In the context of adversarial examples, a natural idea is to test neural networks by checking if it is possible to generate an adversarial attack to change the label predicted by the neural network (Kurakin et al., 2016) and train them to be robust to these examples Madry et al. (2018). Generating adversarial examples is a challenging computational task itself, and the attack generated by a specific attack algorithm may be far from optimal. This may lead one to falsely conclude that a given model is robust to attacks even though a stronger adversary may have broken the robustness. Recent work (Athalye et al., 2018; Uesato et al., 2018) has shown that evaluating models against weak adversaries can lead to incorrect conclusions regarding the robustness of the model. Thus, there is a need to go beyond evaluation using specific adversarial attacks and find approaches that provide provable guarantees against attacks by any adversary.

Verification of neural networks has seen significant research interest in recent years. In the formal verification community, Satisfiability Modulo Theory (SMT) solvers have been adapted for verification of neural networks (Ehlers, 2017; Huang et al., 2017; Katz et al., 2017). While SMT solvers have been successfully applied to several domains, applying them to large neural networks remains a challenge due to the scale of the resulting SMT problem instances. Furthermore, these approaches have been largely limited to networks with piecewise linear activation functions since most SMT solvers are unable to deal efficiently with nonlinear arithmetic. More recently, researchers have proposed a set of approaches that make use of branch and bound algorithms either directly or via mixed-integer programming solvers (Bunel et al., 2017; Cheng et al., 2017; Tjeng and Tedrake, 2017). While these approaches achieve strong results on smaller networks, scaling them to large networks remains an open challenge. These approaches also rely heavily on the piecewise linear structure of networks where the only nonlinearities are maxpooling and ReLUs.

In this paper, we develop a novel approach to neural network verification based on optimization and duality. The approach consists of formulating the verification problem as an optimization problem that tries to find the largest violation of the property being verified. If the largest violation is smaller than zero, we can conclude that the property being verified is true. By using ideas from duality in optimization, we can obtain bounds on the optimal value of this problem in a computationally tractable manner. Note that this approach is sound but incomplete, in that there may be cases where the property of interest is true, but the bound computed by our algorithm is not tight enough to prove the property. This strategy has been used in prior work as well (Kolter and Wong, 2018; Raghunathan et al., 2018). However, our results improve upon prior work in the following ways:

Our verification approach applies to arbitrary feedforward neural networks with any architecture and any activation function and our framework recovers previous results (Ehlers, 2017) when applied to the special case of piecewise linear activation functions.

We can handle verification of systems with discrete inputs and combinatorial constraints on the input space, including cardinality constraints.

The computation involved only requires solving an unconstrained convex optimization problem (of size linear in the number of neurons in the network), which can be done using a subgradient method efficiently. Further, our approach is anytime, in the sense that the computation can be stopped at any time and a valid bound on the verification objective can be obtained.

For the special case of single hidden layer networks, we develop specialized verification algorithms with provable tightness guarantees.

We attain state of the art verified bounds on adversarial error rates on image classifiers trained on MNIST and CIFAR-10 under adversarial perturbations in the infinity norm.

Related Work

A separate but related thread of work is on certifiable training, ie, training neural networks so that they are guaranteed to satisfy a desired property (for example, robustness to adversarial examples within a certain radius) (Kolter and Wong, 2018; Raghunathan et al., 2018). These approaches use ideas from convex optimization and duality to construct bounds on an optimization formulation of verification. However, these approaches are limited to either a class of activation functions (piecewise linear models) or architectures (single hidden layer, as in Raghunathan et al. (2018)). Further, in Kolter and Wong (2018), the dual problem starts with a constrained convex formulation but is then converted into an unconstrained but nonconvex optimization problem to allow for easy optimization via a backprop-style algorithm. In contrast, our formulation allows for an unconstrained dual convex optimization problem so that for any choice of dual variables, we obtain a valid bound on the adversarial objective and this dual problem can be solved efficiently using subgradient methods.

We also note that the ultimate goals of (Kolter and Wong, 2018; Raghunathan et al., 2018) are different from our paper: they modify the training procedure of the neural network so that the network is trained to be easily verifiable. In contrast, our work focuses on extending verification algorithms to apply to a broader class of architectures, activation functions and - in this sense, we view our work as complementary to (Kolter and Wong, 2018; Raghunathan et al., 2018). In fact, since the objective of our dual optimization is differentiable with respect to the network weights, we can extend our approach to training verifiable networks easily by simultaneously optimizing the network weights and dual variables to minimize the dual objective. We leave the study of such an extension for future work.

Another related line of work has to do with theoretical analysis of adversarial examples. It has been shown that feedforward ReLU networks cannot learn to distinguish between points on two concentric spheres without necessarily being vulnerable to adversarial examples within a small radius (Gilmer et al., 2018). Under a different set of assumptions, the existence of adversarial examples with high probability is also established in Fawzi et al. (2018). In Wang et al. (2017), the authors study robustness of nearest neighbor classifiers to adversarial examples. As opposed to these theoretical analyses, our approach searches computationally for proofs of existence or non-existence of adversarial examples. The approach does not say anything a-priori about the existence of adversarial examples, but can be used to investigate their existence for a given network and compare strategies to guard against adversarial attacks.

VERIFICATION AS OPTIMIZATION

Our techniques apply to general feedforward architectures and recurrent networks, but we focus on layered architectures for the development in this paper. The input layer is numbered , the hidden layers are numbered $1,\ldots,L-1$ and the output layer is numbered $L$. The size of layer $l$ is denoted $n_{l}$

We denote by $x^{in}$ the input to the neural network, by $z^{l}$ the pre-activations of neurons at layer $l$ before application of the activation function and by ${x}^{l}$ the vector of neural activations after application of the activation function (to $z^{l-1}$). For convenience, we define ${x}^{0}=x^{in}$. We use ${x}^{l}(x^{in}),z^{l}(x^{in})$ to denote the activations at the $l$-th layer as a function of the input $x^{in}$. Upper and lower bounds on the pre/post activations are denoted by ${\underline{x}}^{{l}},{\overline{x}}^{{l}},{\underline{z}}^{{l}},{\overline{z}}^{l}$ respectively. The activation function at layer $l$ is denote $h^{l}$ and is assumed to be applied component-wise, ie,

Note that max-pooling is an exception to this rule - we discuss how max-pooling is handled separately in the Appendix section 6.2.1. The weights of the network at layer $l$ are denoted $W^{l}$ and the bias is denoted $b^{l}$, $z^{l}=W^{l}{x}^{l}+b^{l}$.

2 VERIFICATION PROBLEM

As mentioned earlier, verification refers to the process of checking that the output of the neural network satisfies a certain desirable property for all choices of the input within a certain set. Formally, this can be stated as follows:

where $x^{in}$ denotes the input to the network, $x^{nom}$ denotes a nominal input, $\mathcal{S}_{in}(x^{nom})$ defines the constrained subset of inputs induced by the nominal input, and $\mathcal{S}_{out}$ denotes the constraints on the output that we would like to verify are true for all inputs in $\mathcal{S}_{in}(x^{nom})$. In the case of adversarial perturbations in image classification, $x^{nom}$ would refer to the nominal (unperturbed image), $\mathcal{S}_{in}(x^{nom})$ would refer to all the images that can be obtained by adding bounded perturbations to $x^{nom}$, and $x^{in}$ would refer to a perturbed image.

In this paper, we will assume that: $\mathcal{S}_{out}$ is always a described by a finite set of linear constraints on the values of final layer ie. $\mathcal{S}_{out}=\cap_{i=1}^{m}\{{x}^{L}:{\left({c^{i}}\right)}^{T}{x}^{L}+d^{i}\leq 0\}$, and $\mathcal{S}_{in}\left({x^{nom}}\right)$ is any bounded set such that any linear optimization problem of the form

can be solved efficiently. This includes convex sets and also sets describing combinatorial structures like spanning trees, cuts in a graph and cardinality constraints.

See the following examples for a concrete illustration of the formulation of the problem:

Consider an adversarial attack that seeks to perturb an input $x^{nom}$ to an input $x^{in}$ subject to a constraint on the perturbation $\left\|{x^{in}-x^{nom}}\right\|\leq\epsilon$ to change the label from the true label $i$ to a target label $j$. We can map this to (1) as follows:

where $c$ is a vector with $c_{j}=1,c_{i}=-1$ and all other components . Thus, $\mathcal{S}_{out}$ denotes the set of outputs for which the true label $i$ has a higher logit value than the target label $j$ (implying that the targeted adversarial attack did not succeed).

Consider a network with a single real valued output and we are interested in ensuring that the output is monotonically increasing wrt each dimension of the input $x^{in}$. We can state this as a verification problem:

Thus, $\mathcal{S}_{out}$ denotes the set of outputs which are large than the network output at $x^{nom}$. If this is true for each value of $x^{nom}$, then the network is monotone.

In several cases, it makes sense to constrain a perturbation not just in norm but also in terms of the number of dimensions of the input that can be perturbed. We can state this as:

Thus, $\mathcal{S}_{out}$ denotes the set of outputs which are larger than the network output at $x^{nom}$. If this is true for each value of $x^{nom}$, then the network is monotone.

3 OPTIMIZATION PROBLEM FOR VERIFICATION

Once we have a verification problem formulated in the form (1), we can easily turn the verification procedure into an optimization problem. This is similar to the optimization based search for adversarial examples (Szegedy et al., 2013) when the property being verified is adversarial robustness. For brevity, we only consider the case where $\mathcal{S}_{out}$ is defined by a single linear constraint $c^{T}z+d\leq 0$. If there are multiple constraints, each one can be verified separately.

If the optimal value of this problem is smaller than (for each $c,d$ in the set of linear constraints defining $\mathcal{S}_{out}$), we have verified the property (1). This is a nonconvex optimization problem and finding the global optimum in general is NP-hard (see Appendix section 6.4.1 for a proof). However, if we can compute upper bounds on the value of the optimization problem and the upper bound is smaller than , we have successfully verified the property. In the following section, we describe our main approach for computing bounds on the optimal value of (5).

4 BOUNDING THE VALUE OF THE OPTIMIZATION PROBLEM

We assume that bounds on the activations $z^{l},{x}^{l},l=0,\ldots,L-1$ are available. Section 6.1 discusses details of how such bounds may be obtained given the constraints on the input layer $\mathcal{S}_{in}\left({x^{nom}}\right)$. We can bound the optimal value of (5) using a Lagrangian relaxation of the constraints:

Note that any feasible solution for the original problem (5) is feasible for the above problem, and for any such solution, the terms involving $\lambda,\mu$ become (since the terms multiplying $\lambda,\mu$ are for every feasible solution). Thus, for any choice of $\lambda,\mu$, the above optimization problem provides a valid upper bound on the optimal value of (5) (this property is known as weak duality (Vandenberghe and Boyd, 2004)).

We now look at solving the above optimization problem. Since the objective and constraints are separable in the layers, the variables in each layer can be optimized independently. For $l=1,\ldots,L-1$, we have

which can be solved trivially by setting each component of ${x}^{l}$ to its upper or lower bound depending on whether the corresponding entry in ${\lambda}^{{l-1}}-{\left({W^{l}}\right)}^{T}{\mu}^{{l}}$ is non-negative. Thus,

where ${\left[{x}\right]}_{+}=\max(x,0),{\left[{x}\right]}_{-}=\min(x,0)$ denote the positive and negative parts of $x$.

Similarly, collecting the terms involving $z^{l}$, we have, for $l=0,\ldots,L-1$

Since $h^{l}$ is a component-wise nonlinearity, each dimension of $z^{l}$ can be optimized independently. For the $k$-th dimension, we obtain

This is a one-dimensional optimization problem and can be solved easily- for common activation functions (ReLU, tanh, sigmoid, maxpool), it can be solved analytically, as discussed in appendix section 6.2. Finally, we need to solve

which can also be solved easily given the assumption on $\mathcal{S}_{in}$. We work out some concrete cases in 6.3.

Once these problems are solved, we can construct the dual optimization problem:

This seeks to choose the values of $\lambda,\mu$ so as to minimize the upper bound on the verification objective, thereby obtaining the tightest bound on the verification objective.

This optimization can be solved using a subgradient method on $\lambda,\mu$.

For any values of $\lambda,\mu$, the objective of (7) is an upper bound on the optimal value of (5). Hence, the optimal value of (7) is also an upper bound. Further, (7) is a convex optimization problem in $\left({\lambda,\mu}\right)$.

If each $h$ is a ReLU function, then (7) is equivalent to the dual of the LP described in Ehlers (2017).

The LP formulation from Ehlers (2017) is also used in Kolter and Wong (2018). The dual of the LP is derived in Kolter and Wong (2018) - however this dual is different from (7) and ends up with a constrained optimization formulation for the dual (the details of this can be found in appendix section 6.4.2). To allow for an unconstrained formulation, this dual LP is transformed to a backpropagation-like computation. While this allows for folding the verification into training, it also introduces nonconvexity in the verification optimization - our formulation of the dual differs from Kolter and Wong (2018) in that we directly solve an unconstrained dual formulation, allowing us to circumvent the need to solve a non-convex optimization for verification.

5 TOWARDS THEORETICAL GUARANTEES FOR VERIFICATION

The bounds computed by solving (7) could be loose in general, since (5) is an NP-hard optimization problem (section 6.4.1). SMT solvers and MIP solvers are guaranteed to find the exact optimum for piecewise linear neural networks, however, they may take exponential time to do so. Thus, an open question remains: Are there cases where it is possible to perform exact verification efficiently? If not, can we approximate the verification objective to within a certain factor (known a-priori)? We develop results answering these questions in the following sections.

Prior work: For any linear classifier, the scores of each label are a linear function of the inputs $w^{T}_{i}x+b_{i}$. Thus, the difference between the predictions of two classes $j$ (target class for an adversary) and class $i$ (true label) is ${\left({w_{i}-w_{j}}\right)}^{T}x$. Maximizing this subject to $\left\|{x-x^{0}}\right\|_{2}\leq\epsilon$ can be solved analytically to obtain the value ${\left({w_{i}-w_{j}}\right)}^{T}x^{0}+\left\|{w_{i}-w_{j}}\right\|_{2}\epsilon$. This observation formed the basis for algorithms in (Raghunathan et al., 2018) and (Hein and Andriushchenko, 2017). However, once we move to nonlinear classifiers, the situation is not so simple and computing the worst case adversarial example, even in the 2-norm case, becomes a challenging task. In (Hein and Andriushchenko, 2017), the special case of kernel methods and single hidden layer classifiers are considered, but the approaches developed are only upper bounds on the verification objective (just like those computed by our dual relaxation approach). Similarly, in Raghunathan et al. (2018), a semidefinite programming approach is developed to compute bounds on the verification objective for the special case of adversarial perturbations on the infinity norm. However, none of these approaches come with a-priori guarantees on the quality of the bound, that is, before actually running the verification algorithm, one cannot predict how tight the bound on the verification objective would be. In this section, we develop novel theoretical results that quantify when the verification problem (5) can be solved either exactly or with a-priori approximation guarantees. Our results require strong assumptions and do not immediately apply to most practical situations. However, we believe that they shed some understanding on the conditions under which exact verification can be performed tractably and lead to specialized verification algorithms that merit further study.

We assume the following for all results in this section: 1) We study networks with a single hidden layer, i.e. $L=2$, with activation function $h^{0}=h$ and a linear mapping from the penultimate to the output layer ${x}^{2}=h^{1}\left({z^{1}}\right)=z^{1}=W^{1}{x}^{1}+b^{1}$. 2) The network has a differentiable activation function $h$ with Lipschitz-continuous derivatives denoted $h^{\prime}$ (tanh, sigmoid, ELU, polynomials satisfy this requirement). 3) $\mathcal{S}_{in}\left({x^{nom}}\right)=\{x^{in}:\left\|{x^{in}-x^{nom}}\right\|_{2}\leq\epsilon\}$.

Since the output layer is a linear function of the penultimate layer ${x}^{1}$, we have

For brevity, we simply denote ${\left({W^{1}}\right)}^{T}c$ as $c$, drop the constant term $c^{T}b^{1}$ and let $W=W^{0},b=b^{0},z^{nom}=Wx^{nom}+b$ and $W_{i}$ denote the $i$-th row of $W$. Then, (5) reduces to:

Suppose that $h$ has a Lipschitz continuous first derivative:

Then $\forall$ $\epsilon\in(0,\frac{\nu}{2L})$, the iteration:

starting at $x^{0}=x^{nom}$ converges to the global optimum $x^{\star}$ of (8) at the rate $\left\|{x^{k}-x^{\star}}\right\|\leq{\left({\frac{\epsilon L}{\nu-\epsilon L}}\right)}^{k}$

Thus, when $\epsilon$ is small enough, a simple algorithm exists to find the global optimum of the verification objective. However, even when $\epsilon$ is larger, one can obtain a good approximation of the verification objective. In order to do this, consider the following quadratic approxiimation of the objective from (8):

This optimization problem corresponds to a trust region problem that can be solved to global optimality using semidefinite programming (Yakubovic, 1971):

where $X\succeq 0$ denotes that $X$ is constrained to be a positive semidefinite matrix. While this can be solved using general semidefinite programming solvers, several special purpose algorithms exist for this trust region problem that can exploit its particular structure for efficient solution, (Hazan and Koren, 2016)

Suppose that $h$ is thrice-differentiable with a globally bounded third derivative. Let

For each $\epsilon>0$, the difference between the optimal values of (10), (8) is at most $\kappa\epsilon^{3}$.

EXPERIMENTS

In this section, we present numerical studies validation our approach on three sets of verification tasks: Image classification on MNIST and CIFAR: We use our approach to obtain guaranteed lower bounds on the accuracy of image classifers trained on MNIST and CIFAR-10 under adversarial attack with varying sizes of the perturbation radius. We compare the bounds obtained by our method with prior work (in cases where prior work is applicable) and also with the best attacks found by various approaches. Classifier stability on GitHub data: We train networks on sequences of commits on GitHub over a collection of 10K repositories - the prediction task consists of predicting whether a given repository will reach more than 40 commits within 250 days given data observed until a certain day. Input features consist a value between 0 and 1 indicating the number of days left until the 250th day, as well as another value indicating the progress of commits towards the total of 40. As the features evolve, the prediction of the classifier changes (for example, predictions should become more accurate as we move closer to the 250th day). In this situation, it is desirable that the classifier provides consistent predictions and that the number of times its prediction switches is as small as possible. It is also desirable that this switching frequency cannot be easily be changed by perturbing input features. We use our verification approach combined with dynamic programming to compute a bound on the maximum number of switches in the classifier prediction over time. Digit sum task: We consider a more complex verification task here: Given a pair of MNIST digits, the goal is to bound how much the sum of predictions of a classifier can differ from the true sum of those digits under adversarial perturbation subject to a total budget on the perturbation across the two digits.

Computing this quantity precisely requires solving the NP-hard problem (5) for each test example, but we can obtain upper bounds on it using our (and other) verification methods and lower bounds using a fixed attack algorithm (in this paper we use a bound constrained LBFGS algorithm similar to (Carlini and Wagner, 2017b)). Since theorem 2 shows that for the special case of piecewise linear neural networks, our approach reduces to the basic LP relaxation from Ehlers (2017) (which also is the basis for the algorithms in Bunel et al. (2017) and Kolter and Wong (2018)), we focus on networks with smooth nonlinearities like tanh and sigmoid. We compare our approach with The SDP formulation from Raghunathan et al. (2018) (note that this approach only works for single hidden layer networks, so we just show it as producing vacuous bounds for other networks).

Each approach gets a budget of $300$ s per verifiation problem (choice of test example and target label). Since the SDP solver from (Raghunathan et al., 2018) only needs to be run once per label pair (and not per test example), its running time is amortized appropriately.

Results on smooth activation functions: Figures 1(a),1(b) show that our approach is able to compute nearly tight bounds (bounds that match the upper bound) for small perturbation radii (up to 2 pixel units) and our bounds significantly outperform those from the SDP approach (Raghunathan et al., 2018) ( which is only able to compute nontrivial bounds for the smallest model with 20 hidden units).

Results on models trained adversarially: We use the adversarial training approach of (Madry et al., 2018) and train models on MNIST and CIFAR that are robust to perturbations from the LBFGS-style attack on the training set. We then apply our verification algorithm to these robust models and obtain bounds on the adversarial error rate on the test set. These models are all multilayer models, so the SDP approach from (Raghunathan et al., 2018) does not apply and we do not plot it here. We simply plot the attack versus the bound from our approach. The results for MNIST are plotted in figure 2(b) and for CIFAR in figure 2(a). On networks trained using a different procedure, the approaches from Raghunathan et al. (2018) and Kolter and Wong (2018) are able to achieve stronger results for larger values of $\epsilon$ (they work with $\epsilon=.1$ in real units, which corresponds to $\epsilon=26$ in pixel units we use here). However, we note that our verification procedure is agnostic to the training procedure, and can be used to obtain fairly tight bounds for any network and any training procedure. In comparison, the results in Kolter and Wong (2018) and Raghunathan et al. (2018) rely on the training procedure optimizing the verification bound. Since we do not rely on a particular adversarial training procedure, we were also able to obtain the first non-trivial verification bounds on CIFAR-10 (to the best of our knowledge) shown in figure 2(a). While the model quality is rather poor, the results indicate that our approach could scale to more complicated models.

2 GITHUB CLASSIFIER STABILITY

We allow the adversary to modify input features by up to 3% (at each timestep) and our goal is to bound the maximum number of prediction switches induced by each attack over time. We can model this within our verification framework as follows: Given a sequence of input features, we compute the maximum number of switches achievable by first computing the target classes that are reachable through an adversarial attack at each timestep (using (7)), and then running a dynamic program to compute the choices of target classes over time (from within the reachable target classes) to maximize the number of switches over time.

Figure 3(a) shows how initially predictions are easily attackable (as little information is available to make predictions), and also shows how the gap between our approach and the best attack found using the LBFGS algorithm evolves over time.

3 COMPLEX VERIFICATION TASK: DIGIT SUM

In order to test our approach on a more complex specification, we study the following task: Given a pair of MNIST digits, we ask the question: Can an attacker perturb each image, subject to a constraint on the total perturbation across both digits, such that the sum of the digits predicted by the classifier differs from the true sum of those digits by as large an amount as possible? Answering this question requires solving the following optimization problem:

where $s$ is the true sum of the two digits. Thus, the adversary has to decide on both the perturbation to each digit, as well as the size of the perturbation. We can encode this within our framework (we skip the details here). The upper bound on the maximum error in the predicted sum from the verification and the lower bound on the maximum error computed from an attack for this problem (on an adversarially trained two hidden layer sigmoid network) is plotted in figure 3(b). The results show that even on this rather complex verification task, our approach is able to compute tight bounds.

CONCLUSIONS

We have presented a novel framework for verification of neural networks. Our approach extends the applicability of verification algorithms to arbitrary feedforward networks with any architecture and activation function and to more general classes of input constraints than those considered previously (like cardinality constraints). The verification procedure is both efficient (given that it solves an unconstrained convex optimization problem) and practically scalable (given its anytime nature only required gradient like steps). We proved the first known (to the best of our knowledge) theorems showing that under special assumptions, nonlinear neural networks can be verified tractably. Numerical experiments demonstrate the practical performance of our approach on several classes of verification tasks.

ACKNOWLEDGEMENTS

The authors would like to thank Brendan O’Donoghue, Csaba Szepesvari, Rudy Bunel, Jonathan Uesato and Shane Legg for helpful comments and feedback on this paper. Jonathan Uesato’s help on adversarial training of neural networks is also gratefully acknowledged.

References

APPENDIX

The quality of the bound in theorem 1 depends crucially on having bounds on all the intermediate pre and post activations $z^{l},{x}^{l}$. In this section, we describe how these bounds may be derived. One simple way to compute bounds on neural activations is to use interval arithmetic given bounds on the input ${\underline{x}}^{{0}}\leq x\leq{\overline{x}}^{{0}}$. Bounds at each layer can then be computed recursively for $l=0,\ldots,L-1$ as follows:

However, these bounds could be quite loose and could be improved by solving the optimization problem

We can relax this problem using dual relaxation approach from the previous section and the optimal value of the relaxation would provide a new (possibly tighter) upper bound on ${x}^{l}_{k}$ than ${\overline{x}}^{{l}}_{k}$. Further, since our relaxation approach is anytime (ie for any choice of dual variables we obtain a valid bound), we can stop the computation at any time and use the resulting bounds. This is a significant advantage compared to previous approaches used in [Bunel et al., 2017]. Similarly, one can obtain tighter upper and lower bounds on ${x}^{l}$ for each value of $l,k$. Given these bounds, one can infer tighter bounds on $z^{l}$ using (11).

Plugging these tightened bounds back into (6) and rerunning the dual optimization, we can compute a tighter upper bound on the verification objective.

2 CONJUGATES OF TRANSFER FUNCTIONS

We are interested in computing $g^{\star}=\max_{y\in[\underline{y},\overline{y}]}g(y)=\mu y-\lambda h\left({y}\right)$. This is a one dimensional optimization problem and can be computed via brute-force discretization of the input domain in general. However, for most commonly used transfer functions, this can be computed analytically. We derive the analytical solution for various commonly used transfer functions: ReLUs: If $h$ is a ReLU, $g(y)$ is piecewise linear and specifically is linear on $[\underline{y},0]$ and on $[0,\overline{y}]$ (assuming that $0\in[\underline{y},\overline{y}]$, else $g(y)$ is simply linear and can be optimized by setting $y$ to one of its bounds). On each linear piece, the optimum is attained at one of the endpoints of the input domain. Thus, the overall maximum can be obtained by evaluating $g$ at $\underline{y},\overline{y},0$ (if $0\in[\underline{y},\overline{y}])$. Thus, $g^{\star}=\begin{cases}\max\left({g(\underline{y}),g(\overline{y}),g(0)}\right)&\text{ if }0\in[\underline{y},\overline{y}]\\ \max\left({g(\underline{y}),g(\overline{y})}\right)&\text{ otherwise}\end{cases}$. Sigmoid: If $h$ is a sigmoid, we can consider two cases: a) The optimum of $g$ is obtained at one of its input bounds or b) The optimum of $g$ is obtained at a point strictly inside the interval $[\underline{y},\overline{y}]$. In case (b), we require that the derivative of $g$ vanishes, i.e:$\mu-\lambda\sigma(y)(1-\sigma(y))=0$. Since $\sigma(y)\in$, this equation only has a solution if $\lambda\neq 0$ and $\frac{\mu}{\lambda}\in\left[0,\frac{1}{4}\right]$ In this case, the solutions are $\sigma(y)=\frac{1\pm\sqrt{1-\frac{4\mu}{\lambda}}}{2}$ Solving for $y$, we obtain $y=\sigma^{-1}\left({\frac{1\pm\sqrt{1-\frac{4\mu}{\lambda}}}{2}}\right)$ where $\sigma^{-1}$ is the logit function $\sigma^{-1}(t)=\log\left({\frac{t}{1-t}}\right)$. We only consider these solutions if they lie within the domain $[\underline{y},\overline{y}]$. Define:

Thus, we obtain the following expression for $g^{\star}$:

If $h$ is a max-pool, we need to deal with it layer-wise and not component-wise. We have $h\left({y}\right)=\max\left({y_{1},\ldots,y_{t}}\right)$ and are interested in solving for

Note here that $\lambda$ is a scalar while $\mu$ is a vector. This can be solved by considering the case of each component of $y$ attaining the maximumum separately. We look at the case where $y_{i}$ attains the maximum below:

Fixing $y_{i}$ and optimizing the other coordinates, we obtain

This one-dimensional function can be optimized via binary search on $y_{i}$. After solving for each $i$, taking the maximum over $i$ gives the value $g^{\star}$

2.2 Upper bounds for general nonlinearities

In general, we can compute an upper bound on $g$ even if we cannot optimize it exactly. The idea is to decouple the $y$ from the two terms in $g$: $\mu y$ and $-\lambda h(y)$ and optimize each independently. However, this gives a very weak bound. This can be made much tighter by applying it separately to a decomposition of the input domain $[\underline{y},\overline{y}]=\cup_{i}[a_{i},b_{i}]$:

Finally we can bound $\max_{[\underline{y},\overline{y}]}g(y)$ using

As the decomposition gets finer, ie, $|a_{i}-b_{i}|\to 0$, we obtain an arbitrarily tight upper bound on $g$) this way.

3 OPTIMIZING OVER THE INPUT CONSTRAINTS

In this section, we discuss solving the optimization problem defining $f_{0}({\mu}^{{0}})$ in (7)

where $\left\|{\cdot}\right\|_{\star}$ is the dual norm to the norm $\left\|{}\right\|$. Further this bound can be achieved for an appropriate choice of $x$. Hence, the optimal value is precisely $b^{T}\mu-\left\|{W^{T}\mu}\right\|_{\star}$. Combinatorial objects: Linear objectives can be optimized efficiently over several combinatorial structures. For example, if $x$ is indexed by the edges in a graph and $\mathcal{S}_{in}$ imposes constraints that $x$ is binary valued and that the edges set to $1$ should form a spanning tree of the graph, the optimal value can be computed using a maximum spanning tree approach. Cardinality constraints: $x$ may have cardinality constrained imposed on it: $\left\|{x}\right\|_{0}\leq k$, saying that at most $k$ elements of $x$ can be non-zero. If further we have bounds on $x\in[\underline{x},\overline{x}]$, then the optimization problem can be solved as follows: Let $v(\mu)={\left[{W^{T}\mu}\right]}_{+}\odot\overline{x}+{\left[{W^{T}\mu}\right]}_{-}\odot\underline{x}$ and let $[v]_{i}$ denote the $i$-th largest component of $v$. Then the optimal value is $\sum_{i=1}^{k}[v(\mu)]_{i}+b^{T}\mu$.

4 PROOFS OF THEORETICAL RESULTS

Consider the case of sigmoid transfer function with an $\infty$ norm perturbation. Then, the verification problem reduces to :

This is an instance of a sigmoidal programming problem, which is proved to be NP-hard in Udell and Boyd

4.2 Proof of theorem 2

Now, the LP relaxation from [Ehlers, 2017] can be written as

We can rewrite this optimization problem as

which is still a convex optimization problem, since all the constraints are either linear of the form $\max(0,z)\leq x$ which is a convex constraint since the LHS is a convex function and the RHS is linear.

Taking the dual of this optimization problem, we obtain

where $s^{l}_{k}=\frac{{\overline{z}}^{l}_{k}}{{\overline{z}}^{l}_{k}-{\underline{z}}^{{l}}_{k}}$. Let ${\lambda}^{{l}}_{k}={\lambda}^{{l}}_{k;a}-{\lambda}^{{l}}_{k;b}$ for $l,k$ such that $0\in[{\underline{z}}^{{l}}_{k},{\overline{z}}^{l}_{k}]$. Further let $\mathcal{I}_{l,k}=[{\underline{z}}^{{l}}_{k},{\overline{z}}^{l}_{k}]$ and let $\mathcal{I}_{a}$ denote the set of $l,k$ such that ${\underline{z}}^{{l}}_{k}\geq 0$, $\mathcal{I}_{b}$ the set of $l,k$ such that ${\overline{z}}^{l}_{k}\leq 0$ and $\mathcal{I}_{c}$ the set of $l,k$ such that $0\in\mathcal{I}_{l,k}$. We can then rewrite the dual as

We now solve for the maximum over $z^{l}_{k}$ considering three cases: (a) $l,k\in\mathcal{I}_{a}$: The maximization is over a linear function and the maximum is attained at one of the bounds, hence the maximum evaluates to

Adding the constant $-{\lambda}^{{l}}_{k,b}s^{l}_{k}{\underline{z}}^{{l}}_{k}$ we obtain

Minimizing the above expression with respect to ${\lambda}^{{l}}_{k;b}$ subject to ${\lambda}^{{l}}_{k;b}\geq\max\left({0,-{\lambda}^{{l}}_{k}}\right)$, we obtain

(since the expression is monotonically increasing in ${\lambda}^{{l}}_{k;b}$, minimizing it subject to these constraints we just set ${\lambda}^{{l}}_{k;b}$ to the larger of its lower bounds). Now, for the second term to attain the maximum, we require that ${\lambda}^{{l}}_{k}\leq 0,{\mu}^{{l}}_{k}=s^{l}_{k}{\lambda}^{{l}}_{k}$, in which case all the last three terms attain the maximum. Thus, the maximum is equal to the max of three terms:

Given this, the rest of the dual exactly matches the calculations from section 3.3.

4.3 Proof of theorem 3

We leverage results from [Polyak, 2003] which argues that a smooth nonlinear function can be efficicently optimized over a “small enough” ball. Specifically, we use theorem 7 from [Polyak, 2003]. In order to apply the theorem, we need to bound the Lipschitz costant of the derivative of the function $f(x)=\sum_{i}c_{i}h_{i}(W_{i}x+b_{i})$. Writing down the derivative, we obtain

where $t\in[W_{i}x+b_{i},W_{i}y+b_{i}]$. Thus, we have

Thus $f^{\prime}$ is Lipschitz with Lipschitz constant $\sigma_{\max}\left({W^{T}\operatorname*{diag}\left({c}\right)}\right)\sigma_{\max}\left({W}\right)\gamma$. Further

Hence by theorem 7 from [Polyak, 2003], the theorem follows. ∎

4.4 PROOF OF THEOREM 4

We have $\left\|{z}\right\|_{2}\leq\epsilon\implies|W_{i}z|\leq\left\|{W_{i}}\right\|_{2}\epsilon$ (by Cauchy-Schwartz). Thus, for eacn $i$, we have

Adding the error terms over all terms in the objective function, we obtain the result. ∎