Overcoming the Convex Barrier for Simplex Inputs
Year: 2022

Abstract:
Recent progress in neural network verification has challenged the notion of a convex barrier, that is, an inherent weakness in the convex relaxation of the output of a neural network. Specifically, there now exists a tight relaxation for verifying the robustness of a neural network to `∞ input perturbations, as well as efficient primal and dual solvers for the relaxation. Buoyed by this success, we consider the problem of developing similar techniques for verifying robustness to input perturbations within the probability simplex. We prove a somewhat surprising result that, in this case, not only can one design a tight relaxation that overcomes the convex barrier, but the size of the relaxation remains linear in the number of neurons, thereby leading to simpler and more efficient algorithms. We establish the scalability of our overall approach via the specification of `1 robustness for CIFAR-10 and MNIST classification, where our approach improves the state of the art verified accuracy by up to 14.4%. Furthermore, we establish its accuracy on a novel and highly challenging task of verifying the robustness of a multi-modal (text and image) classifier to arbitrary changes in its textual input.

heading: 1 Introduction
text: Verification refers to the challenging computational problem of determining whether a neural network satisfies a given specification. Perhaps the most popular specification is to prove or disprove that a neural network classifier is robust to perturbations of the input that lie within an `p ball [de Palma et al., 2021a, Wong and Kolter, 2018, Zhang et al., 2018, Weng et al., 2018, Mirman et al., 2018, Dvijotham et al., 2018], with impressive state of the art results recently achieved in Wang et al. [2021]. The ability to verify neural networks would open the door to better understanding their nature, and allow us to apply deep learning in safety critical domains where errors can have a large cost. Given the importance of the problem, it is unsurprising that it has attracted considerable atttention from the machine learning and automated verification communities [Katz et al., 2017, Ehlers, 2017].
Early work in verification lead to the notion of a convex barrier, that is, a limitation in the tightness of the bounds obtainable by the convex relaxation of the output of a neural network [Salman et al., 2019]. This weakness was seen as a primary reason for the slow convergence of branch-and-bound algorithms for verification, which rely on convex relaxations to compute the bounds, on a large number of specifications on standard datasets. However, recent work has been able to successfully overcome this barrier. Specifically, Anderson et al. [2019] proposed a tight relaxation that precisely defines the convex hull of a composition of a linear function of a vector within an `∞ ball with the ReLU non-linearity. While their relaxation has a large number of constraints (exponential in the size of the vector), they provide an efficient algorithm for identifying the most violated constraint at any infeasible point. This enables the use of efficient cutting plane algorithms to solve the
35th Conference on Neural Information Processing Systems (NeurIPS 2021).
primal [Anderson et al., 2019], active sets to solve the dual [de Palma et al., 2021a,b], and even approximate linear bound propagation algorithms [Tjandraatmadja et al., 2020].
Buoyed by the possibility of realizing practical verification using tight relaxations, we consider an important specification, namely, robustness to perturbations that lie in a probability simplex. Examples of such a specification include robustness to `1 perturbations or to word substitutions [Huang et al., 2019]. Previous approaches for addressing this specification relied on fairly loose relaxations based on interval bound propagation [Huang et al., 2019, Gowal et al., 2018]. To alleviate this deficiency, we derive the convex hull of the composition of a linear transformation of the probability simplex with a convex non-linearity such as ReLU or SoftPlus. Somewhat surprisingly, we show that, unlike the previously considered case of `∞ balls, the probability simplex helps greatly simplify the description of the convex hull. In fact, the number of constraints required is linear in the dimensionality of the simplex. By using a novel technique to propagate the simplex constraints through the hidden layers of the network, we derive a tight relaxation for the output of a network whose size scales linearly with the size of the network. Furthermore, we suitably extend a linear bound propopagation algorithm [Zhang et al., 2018] to solve the tight relaxation efficiently, thereby realizing practical verification over simplex inputs.
We demonstrate the scalability of our approach using the specification of robustness to `1 perturbations for MNIST and CIFAR-10 classification. Our method achieves 13.6% higher verified accuracy on MNIST and up to 14.4% higher verified accuracy on CIFAR-10 compared to the state of the art baselines on the same networks given the same computational budget.
To further demonstrate the benefits of our tight relaxation, we consider a novel and highly challenging specification of global robustness in multi-modal classification. Specifically, we consider the Food 101 dataset [Wang et al., 2015], where each sample consists of an image of a food item together with its recipe. Our specification requires a neural network trained to classify the food item to be robust to arbitrary changes in the text of a sample. This specification captures the scenario where the image is carefully curated while the text is crowd-sourced and can therefore be easily manipulated by adversarial actors. While similar specifications have been considered in previous works [Jia et al., 2019, Huang et al., 2019], they focus on substituting a very small subset of words with their synonyms, which leads to simpler verification problems. We show that, on our significantly more difficult global verification task, our method achieves up to 25% higher verified accuracy in the same amount of time as the state of the art baseline.

heading: 2 Preliminaries
text: We provide a formal mathematical description of our verification problem, and briefly discuss the existing relaxations in order to contextualise our contributions.

heading: 2.1 Problem description
text: We denote the m-dimensional probability simplex as ∆m, that is, ∆m = {x ∈ Rm | x ≥ 0, 1>x ≤ 1}. As mentioned in the previous section, we are interested in verifying specifications of a given neural network when its input is constrained to lie in a simplex. We focus on networks with a layered architecture to keep notation simple, but our ideas easily extend to any feed-forward network, including residual networks. We consider a neural network with n layers. Each layer is assumed to be composed of two operations: (i) an affine operation (fully connected layer or convolution layer), which we denote by Lk(·); and (ii) a non-linear activation function, which we denote by σ(·). In other words, given its input xk−1 ∈ Rnk−1 , the k-th layer performs the operation x̂k = Lk(xk−1) ∈ Rnk , followed by xk = σ(x̂k) ∈ Rnk . While we place no restriction on the linear operation, we make the following assumption on the activation function.
Assumption 1. We assume that the activation function σ is an element-wise convex function (for example, ReLU or SoftPlus). Verification problem: Using the above notation, the verification problem we solve can be formulated as
min x Ψ (x̂n) (1a)
s.t. x̂k = Lk (xk−1) ,xk = σ(x̂k) k ∈ [n], (1b) x0 ∈ ∆n0 , (1c)
where [n] denotes the set {1, · · · , n}. The objective function Ψ is a scalar-valued linear function of the output of the final layer of the the network. For example, say we wish to verify that a classification network is not vulnerable to any adversarial attacks. In this case, we define Ψ as the difference between the true logit and a target logit outputted by the network. The sign of the optimum value of problem (1) can be used to either prove or disprove the aforementioned specification.
We illustrate the practical importance of considering simplex inputs using two examples. These examples will also form the basis of our experimental setup.
`1 perturbations: Consider a network with a continuous valued input x ∈ Rm. We are interested in verifying the behavior of the network under input perturbations that lie within an `1 ball: {x |∥∥x− x0∥∥
1 ≤ }. This input domain can be reformulated as a simplex as
x = x0 + Mz, z ∈ ∆2m, M (m×2m) =  1 −1 0 0 . . . 0 0 0 0 1 −1 . . . 0 0 ... 0 0 0 0 . . . 1 −1  . (2) Bag of words models: Consider a text classification network that takes text as input and makes predictions based on an embedding of the text. A commonly used embedding is the so-called “bag of words”. Here, we first take an embedding for every word in the text (for example, using a precomputed set like GloVe [Pennington et al., 2014] or Word2Vec [Mikolov et al., 2013]). Next, we take the mean of all the word embeddings to obtain the final representation. We denote the word embeddings as a matrix E ∈ Rd×v , where each d-dimensional column represents an embedding of a putative word in a vocabulary of size v. Using the above matrix, the text embedding is given by Ex where x represents the normalized counts of words from the vocabulary in the text. In other words, x ∈ ∆v assuming that arbitrarily long text with arbitrary numbers of repetitions of each word in the vocabulary are allowed.

heading: 2.2 Planet and disjunctive relaxations
text: Ehlers [2017] proposed a convex relaxation for the ReLU activation function, which is commonly referred to as Planet in the literature. The Planet relaxation has been widely used in many verification algorithms [Bunel et al., 2020b, Dvijotham et al., 2018, Bunel et al., 2020a, Lu and Kumar, 2020]. Briefly, it relaxes the sequence of two operations: x̂ = wTx + b where x ∈ Rm, followed by y = ReLU(x̂). To this end, it utilizes lower and upper bounds on x̂. In our case, since x ∈ ∆m, we can compute the bounds as ˜̀= wmin + b ≤ wTx + b ≤ wmax + b = ũ. Here, wmin and wmax denote the minimum and maximum entries of w respectively. Using the bounds on x̂, the Planet relaxation for the set S = {y,x | y = ReLU(wTx + b),x ∈ ∆m} is defined as
P∆ : y ≥ wTx + b, y ≥ 0, y ≤ ũ ũ− ˜̀ ( wTx + b− ˜̀ ) , x ∈ ∆m. (3)
In Anderson et al. [2019, 2020], the authors propose a tighter relaxation and characterize the exact convex hull of the set {(x, relu ( wTx + b ) ) : ` ≤ x ≤ u}.
However, this characterization involves exponentially many inequalities. And efficient algorithms based on it need to resort to cutting plane methods, adding violated inequalities sequentially. Doing so is computationally challenging and requires significant effort to implement in a scalable manner. Further, this does not handle the simplex constraint on the input. Thus using this relaxation would require replacing the simplex constraint with the unit hypercube, a much weaker constraint on the inputs.
Anderson et al. [2020] also propose an ideal formulation for the product of k simplices. Their formulation needs additional variables and still requires cutting planes. However, eliminating the auxiliary variable, as in our case, leads to a concise formulation. Further, our relaxation is derived for convex activation functions, whereas the formulation of Anderson et al. [2020] is limited to the maximum of two affine functions.

heading: 3 A Concise Convex Relaxation
text: In this section, we derive our novel tight convex relaxation for problem (1). In order to make the exposition clearer, we assume that we have access to simplex constraints for all xk, k ∈ [n− 1]. As will be seen in the next section, such constraints can be derived by propagating the simplex constraint on the input x0 through the network.

heading: 3.1 An exact convex relaxation for a single neuron
text: We begin by considering the simple case of a single neuron, which will form the building block of our final relaxation. Similar to the previous relaxations, we consider the set S = {y,x | y = σ(wTx + b),x ∈ ∆m}, where σ is a convex activation function, for example ReLU. We aim to characterize the convex hull CH∆ of the set S. Theorem 3.1. The convex hull CH∆ of S is defined by the following convex constraints
y ≥ σ ( wTx + b ) , x ∈ ∆m, (4a)
y ≤ ∑ i xi ( σ ( wTei + b ) − σ (b) ) + σ (b) , (4b)
where ei ∈ Rm, eii = 1, eij = 0∀j 6= i, denotes the i-th coordinate vector in Rm.
By the definition of a convex hull, the proposed relaxation is the tightest possible relaxation for a single neuron with x ∈ ∆m. Note that, when σ is the ReLU activation function, the only difference between the proposed relaxation and the Planet relaxation P∆ is the upper bound on y. Figure 1 compares the upper bound of the Planet relaxation P∆ with the proposed relaxation CH∆ for the case where m = 2. As can be seen, our relaxation is significantly tighter than Planet, which paves the way for tractable verification over simplex inputs. The following proposition formally characterizes the difference between the tightness of CH∆ and P∆. Proposition 3.2. For any input dimension m, CH∆ is provably tighter thanP∆. Specifically, we can characterize the gap between CH∆ and P∆ by the gap in the optimal value of the problem
max x
y − y′ subject to (y,x) ∈ P∆, (y′,x) ∈ CH∆.
The gap in the optimal value is proportional to the variance in the weight vector w (see supplementary material for details).
The proofs of the above theorem and proposition are provided in the supplementary material. The proof of Theorem 3.1 utilizes a fundamental result from convex analysis,
that any linear function obtains the same maximum value over S as over its convex hull CH∆. Note that our relaxation overcomes the convex barrier by providing bounds that are significantly tighter than the Planet relaxation. Convex barrier is a term introduced in Salman et al. [2019], which is defined as the gap between the optimal value of the original verification problem and the optimal convex relaxation of the non-linearity.
Comparison to Tjandraatmadja et al. [2020] Our relaxation requires only a linear number of inequalities to describe the convex hull for the composition of a linear function with a convex activation function for simplex inputs. In contrast, the Anderson relaxation [Tjandraatmadja et al., 2020, Anderson et al., 2020] requires an exponential number of constraints. The submodularity based proof for deriving the relaxation from Tjandraatmadja et al. [2020] can help us understand the discrepancy. The method makes use of the Kuhn triangulation of [0, 1]n [Todd, 1976], which
describes the collection of simplices whose union is [0, 1]n, and requires an exponential number of simplices. Since a unique affine interpolation of the function needs to be constructed on each of these simplices, it requires an overall exponential number of inequalities. In contrast, our relaxation only requires a linear number of inequalities. Note that the input simplex ∆n is not one of the simplices from the Kuhn triangulation whose union is the unit hypercube. We provide a visualization for this intuition in the supplementary material.

heading: 3.2 Final relaxation
text: Using the convex hull for a single neuron, we can now describe our overall relaxation. Recall that we have assumed xk ∈ ∆nk for each k ∈ [n− 1]. This is ensured through a simplex propagation algorithm described in the next section. In addition, we also compute interval bounds on the preactivations x̂k ∈ [`k, uk]. Using the interval bounds, we define θk = ukuk−`k , γk = −`k, uk (x) = θk (Lk (x)− γk) and u′k (x) = ∑ i xi ( σ ( Lk ( ei )) − σ (Lk (0)) ) + σ (Lk (0)). Furthermore, since x̂n is itself a linear function of xn−1, with a slight overload of notation, we denote the objective function of our relaxation as Ψ (xn−1). Using the above notation, the overall proposed convex relaxation of problem (1) for the ReLU activation function can be written as
min x Ψ (xn−1) (5a)
s.t. xk ≥ Lk (xk−1) ,xk ≥ 0 k ∈ [n− 1], (Planet lower bound) (5b) xk ≤ uk(xk−1), k ∈ [n− 1], (Planet upper bound) (5c) xk ≤ u′k(xk−1), k ∈ [n− 1], (from equation 4b) (5d) xk ∈ ∆ k ∈ {0} ∪ [n− 1]. (5e)
Similar relaxations can be derived for other convex activation functions by linearizing the convex function around a given point. However, we focus on the ReLU case for brevity of exposition, particularly since ReLU is the most commonly used convex activation function.

heading: 4 Algorithm
text: Our verification algorithm is composed of two phases: (i) propagating simplex constraints on the activations at every layer; and (ii) computing a lower bound on problem (1). We describe these in the following subsections.

heading: 4.1 Simplex propagation
text: We assume that the output of each layer is non-negative. If this is not the case, we can simply add a constant to the activation of each layer so that the output becomes non-negative. Let us denote hk(x) = σ (Lk (x)). Since hk(.) is an element-wise convex function of its inputs, 1Thk(.) is also a convex function. Using the fact that the maximum of a convex function over the simplex is attained at one of the vertices, it can be shown that the following inequality holds true∑
i
xki ≤ max j∈{0,...,nk−1}
1Thk ( ej ) = αk. (6)
Here, xki denotes the i-th coordinate of the vector of activations xk at the output of layer hk. Note that the above inequality can be rewritten in the form ∑ i x̃ki ≤ 1, where x̃ki = xki αk
, so that we can propagate simplex-like constraint simply by rescaling activations at the layer appropriately. Details for conditioning the intermediate layers into simplex using inequalities of the above form are provided in the supplementary material.

heading: 4.2 Efficient solver
text: The optimization problem (5) is a Linear Program and as such can be solved easily by off-the-shelf solvers [Gurobi]. However, given the size of modern deep networks, such an approach would struggle to scale. Hence, researchers have recently started developing scalable custom solvers for relaxations of neural network outputs.
Zhang et al. [2018], Singh et al. [2019] developed efficient solvers for relaxations that rely on bounds on the output of a neuron that are expressed as linear functions of the input. Such solvers have been scaled to be extremely efficient and amenable to use within branch and bound frameworks [Wang et al., 2021]. Inspired by their success, we extend their capabilities to solve our novel tight relaxations derived in the previous section. To this end, we first relax problem (5) to a form that can be solved efficiently using a single backward pass. Concretely, we combine the lower bounds (5b) and the non-negativity constraint from (5e) into a single lower bound using weighting coefficients ak. We also combine the upper bounds (5c and 5d) into a single upper bound with weighting coefficients āk. The values of the weighting coefficients ak and āk are constrained to lie between 0 and 1. This leads to the following optimization problem
L(a,a) = min x Ψ (xn−1) (7a)
s.t. x0 ∈ ∆ , (7b) xk ≥ ak Lk (xk−1) k ∈ [n− 1], (7c) xk ≤ ak uk (xk−1) + (1− ak) u′k (xk−1) k ∈ [n− 1]. (7d)
It turns out that the above formulation can be solved efficiently by a single backward pass over the network. In order to derive the solution, it is useful to introduce the notion of decomposition of an affine function into monotone, anti-monotone and constant parts. Definition 4.1. For any scalar-valued affine function f (x), define
f+ (x) = ( max ( ∂f
∂x , 0
))T x, f− (x) = ( min ( ∂f
∂x , 0
))T x, f c = f (0) , (8)
so that f (x) = f+ (x) + f− (x) + f c.
Since f+ only involves the positive coefficients in the gradient of f , it is monotonically increasing, and similarly, f− is monotonically decreasing. Exploiting this and the fact that Ψ is a scalar valued linear function, we obtain
Ψ (xn−1) = Ψ + (xn−1) + Ψ − (xn−1) + Ψ0 ≥ Ψ− ( an−1 un−1 (xn−2) + (1− an−1) u′n−1 (xn−1) ) + Ψ+ ( an−1 Ln−1 (xn−2) ) + Ψc. (9)
The lower bound above is an affine function of xn−2 and hence leads to a recursive algorithm where we compute lower bounds on the specification expressed as a function of xk−1 given a lower bound on the specification expressed as a linear function of xk.
Therefore, this leads to a recursive algorithm for computing a lower bound on the optimal value of (7), that is presented in the Subroutine SIMPLEX_BACKWARD function on line 11 in Algorithm 1. It can in fact be proven that this is the exact optimal value, using an argument similar to Salman et al. [2019], Section 3.
The computation required to express a lower bound on the specification given as a linear function of xk+1 to a lower bound expressed as a linear function of xk is shown on line (14) of Algorithm 1. Note that this computation can be conveniently done in frameworks that support automatic differentiation, by computing the gradient of the expression on the right hand side of line 14 at 0 and its value at 0, which gives the vector of coeffients and the bias term of the affine function of xk. Thus, the cost of implementing line 14 of the algorithm is equal to the cost of performing backpropagation through a single layer of the network.
Denote the projection onto the unit hypercube as π (x) = min (max (x, 0) , 1). Our overall algorithm is presented in Algorithm 1. It consists of two main functions SIMPLEX_BACKWARD and SIMPLEX_VERIFY. The SIMPLEX_BACKWARD algorithm computes L (a,a) for a fixed value of a,a. However, this lower bound is valid for any choice of these parameters. Hence SIMPLEX_VERIFY performs projected gradient ascent on L with respect to a,a to obtain the tightest possible lower bound on the (equation 1). The idea of optimizing the weighting coefficients a,a to obtain tighter bounds is inspired from the algorithm of Xu et al. [2021], with suitable adaptations to the setting involving our novel relaxation.
Proposition 4.2. Algorithm 1 computes a lower bound on the optimal value of (1).
Proof. Follows by recursively applying the lower bound at each layer while defining fk.
Computational Complexity: The complexity of SIMPLEX_BACKWARD function 11 for computing bounds for a given value of at, āt, is the same as the cost of two backward passes through the network. This is twice the cost of CROWN [Zhang et al., 2018], or one iteration of auto-lirpa [Xu et al., 2021], which uses a single backward pass.
Algorithm 1 Simplex Verify 1: function SIMPLEX_VERIFY(Ψ) 2: Initialise a and ā with values between 0 and 1 3: for t ∈ J0, tmax − 1K do 4: L(at,at) = SIMPLEX_BACKWARD(Ψ,at,at) 5: Compute gradients dLdat , dL dat
via backpropagation 6: at+1, āt+1 ← update gradient ascent (or Adam) 7: at+1,at+1 ← π ( at+1 ) , π(at+1) (projection) 8: end for 9: return L(at+1, āt+1)
10: end function 11: function SIMPLEX_BACKWARD(Ψ,a,a) 12: fN ← Ψ 13: for k ∈ Jn− 1, 0K do 14: Set fk (x)← f−k+1 (ak uk (x) + (1− ak) u ′ k (x))+f + k+1 (ak Lk (x))+f c k+1. 15: end for 16: L(a,a) = minx0∈∆ f0 (x0) 17: return L(a,a) 18: end function

heading: 5 Experiments
text: In this section, we demonstrate the effectiveness of the proposed method on two specifications: (i) robustness to `1 perturbations for image classifiers (Sec 5.1), and (ii) robustness of multi-modal classifiers to text perturbations (Sec 5.2).

heading: 5.1 `1 robustness verification
text: Experimental Setup We verify the `1 robustness of networks from [de Palma et al., 2021a, Bunel et al., 2020b] and VNN-COMP [2020]. We compute the lower bound on the robustness margin (difference between the ground truth logit and the other logits) using the verification methods. An image is said to be verified if the lower bound across all possible labels is positive. We evaluate the effectiveness of various methods for incomplete verification on the MNIST [Lecun] and CIFAR-10 [Krizhevsky and Hinton, 2009] datasets. For MNIST, we evaluate on the entire test set, and for CIFAR-10 we evaluate on 1000 random images from the test set [Krizhevsky and Hinton, 2009]. The MNIST and CIFAR-10 datasets are widely used in the machine learning community, and are available under the creator’s consent and MIT license respectively. For both MNIST and CIFAR-10, we use the model architectures from [de Palma et al., 2021a]. The models are trained using the SLIDE attack (sparse `1-descent attack) from Tramer and Boneh [2019] with = 0.3 for all networks except the VNN-comp big network, which is trained with = 0.05. We used the publicly available training implementation of [Ding et al., 2019] (see supplementary material for details). The code is made available under the LGPL License online 1. We also test on the SGD trained CIFAR Wide model from [de Palma et al., 2021a]. We verify robustness against input perturbations lying in `1 norm ball with = 0.35 for the MNIST network, = 0.2 for the VNN-comp big network and = 0.5 for all the other CIFAR-10 networks.
1https://github.com/BorealisAI/advertorch.
Methods We compare against other propagation based solvers and Gurobi. Gurobi baselines employ the commercial black-box solver Gurobi [Gurobi Optimization, 2020]. Gurobi solves the problems to optimality, giving the tightest possible bounds for the corresponding relaxations. Gurobi Planet corresponds to solving the Planet relaxation [Ehlers, 2017] of the network. Gurobi Simplex corresponds to solving our relaxation using Gurobi. Both the methods are run on 4 CPU threads on an Intel(R) Core(TM) i7-4960X CPU @ 3.60GHz processor. We also compare against an optimized LiRPA solver for the Planet relaxation [Ehlers, 2017], and refer to it as Opt-Lirpa Planet. The solver remains the same as our solver, with the only difference being that the upper bound corresponding to our relaxation is not present (see supplementary material for details). Note that the intermediate layer bounds in Opt-Lirpa Planet are not jointly optimized. Simplex Verify corresponds to our solver described in Sec 4.2. Both the LiRPA based solvers use Adam [Kingma and Ba, 2015] for updating the weighting vectors a, and are run on a single Nvidia Titan Xp GPU. All the methods use the same intermediate bounds, which are computed using Opt-Lirpa Planet run for 20 iterations. We compare the effectiveness of the different methods for computing the final layer bounds. Further details about the baselines and experimental settings, including the hyper-parameters, are provided in the supplementary material.
Results Table 1 shows the verified accuracy and average verification time per sample of different methods. Gurobi Simplex achieves much higher verified accuracy (up to 16.5% higher) in comparison to Gurobi Planet. This is in line with Theorem 3.1 and Proposition 3.2 because our proposed relaxation is much tighter than Planet. This also shows the benefit of using tighter relaxations. For a fair comparison, the number of iterations of both LiRPA based methods were tuned such that each of them take the same amount of time. We tuned the number of iterations on a subset of images. It is worth noting that the proposed solver, Simplex Verify, achieves much higher verified accuracy than Opt-Lirpa Planet, in the same amount of time. Simplex Verify also achieves comparable accuracy to Gurobi Simplex, while being nearly 3 orders of magnitudes faster, which shows the effectiveness of the proposed solver in solving Problem 5.
We also compare the tightness of the bounds achieved by different methods. We obtained the lower bounds provided by different solvers. We can get the upper bounds using the sparse PGD attack, SLIDE [Tramer and Boneh, 2019]. A smaller gap between the PGD upper bound and verified lower bound, indicates tighter verification. Figure 2a shows the pointwise comparison of the gap to PGD for Gurobi Planet and Gurobi Simplex, on the same data. PGD gap is much smaller for Gurobi Simplex in comparison to Gurobi Planet, thereby showing that our relaxation achieves much tighter verification. Figure 2b shows the pointwise comparison of the gap for Opt-Lirpa Planet and our Simplex Verify. Simplex Verify achieves much tighter verification.

heading: 5.2 Multi-modal classifier robustness verification
text: Experimental Setup In this section, we are interested in verifying the robustness of multi-modal classifiers to text-based attacks. The motivation are scenarios where image based models are augmented with text to improve the accuracy of the classifier. However, this makes the model vulnerable to text based attacks. The aim of this experiment is to show the adversarial vulnerability of such models and verify their robustness. For this experiment we verify the robustness of models on the UPMC FOOD-101 dataset [Wang et al., 2015], which is a commonly used dataset for multi-modal classification (see [Kiela et al., 2019]). This dataset consists of images and recipes of different food items. It is made available by the creators’ consent online 2. The specification that we are interested in verifying is as follows: for a given image and text pair, only the text is perturbed and any possible text from the given vocabulary is allowed in the attack. The aim of this specification is to characterise the worst-case sensitivity of the model. We are not aiming for perfect robustness to the noise in text, but aim to check its sensitivity. We use a ConcatBOW model for this task as proposed in Kiela et al. [2019]. The model extracts an image embedding using a standard pretrained ResNet-152 model. It also extract a Bag of words embedding for the text. The model concatenates the embeddings and feeds them into a multilayer perceptron (MLP) classifier, which has 1,846,200 parameters. Arbitrary changes in the text can be modelled as a simplex as described in Section 2.1. The model follows the same architecture as the state-of-the-art model for this dataset [Ignazio Gallo and Grassa, 2020], except that we replace Bert embeddings with BOW embeddings. We reduce the dataset from 101 classes to 10 classes. More details are provided in the supplementary.
Related Work Huang et al. [2019] considered verification against synonym replacements or character flip perturbations on text classification models. The input specification was modeled as a simplex and they proposed to use Interval bound propagation (IBP) for the same. Concurrent to Huang et al. [2019], Jia et al. [2019] considered a specification where every word in the text can be replaced with a similar word and used IBP. Xu et al. [2020] use more recent LiRPA variants for verification of synonym-based word substitution with a maximum of 6 word substitutions. Concurrent to our work, Bonaert et al. [2021] proposed a new method for certifying Transformers to synonym based attacks. They provide a lifting from `∞ analysis techniques to other norms, and propose a new convex relaxation for a number of settings, but none of these characterize the convex hull exactly in any setting. In contrast to these works, we consider a much more challenging specification where any possible text from the vocabulary is allowed. This specification includes arbitrary length sentences. Further, even our baseline, Opt-Lirpa Planet, is much tighter than IBP. We also propose a tighter relaxation which characterises the convex hull for our setting of a composition over a convex activation function and an activation function where the input is constrained to be in the simplex, and propose an efficient algorithm for the relaxation. It is also important to note that we perform experiments on verification-agnostic networks unlike Huang et al. [2019].
Results We compare the lower bounds on the robustness margin for Opt-Lirpa Planet and Simplex Verify. We use PGD attack for computing the upper bound. The networks are trained to be robust to simplex perturbations using PGD training. Figure 3 shows the pointwise comparison of the gap to
2http://visiir.lip6.fr/
PGD upper bounds for Opt-Lirpa Planet and Simplex Verify. Note here that a smaller gap indicates tighter verification. For a fair comparison, the iterations of the propagation algorithms were again tuned such that each of them takes the same amount of time (0.08s). It can be seen that Simplex Verify achieves much tighter bounds in the same amount of time.
In Table 2, we present the verified accuracy achieved by the different methods with the nominal and Pgd accuracy. We present results for networks trained with different weighting for nominal and PGD loss during the adversarial training. Network trained only on images achieves 87.82% accuracy. Note that our method achieves remarkably higher verified accuracy, up to 25% higher, as compared to OptLirpa Planet in the same amount of time. This shows the benefit of our approach over the existing solvers.

heading: 6 Discussion and Broader Impact
text: As machine learning continuously finds new application domains, the robustness of machine learning systems in the face of adversarsarial behavior becomes increasingly relevant. Neural network verification, which seeks to obtain provable guarantees on robustness of neural networks, has mostly focused on `∞ perturbations. However, real security threats often involve more drastic changes that could lead to arbitrary perturbations in the input. In this paper, we have we have proposed an efficient algorithm for verification of neural networks against simplex constrained perturbations. We have shown
the practical importance of this specification through two applications. Firstly, we verify the robustness of image classifiers to `1 perturbations, which could be an appropriate threat model when perturbations of different features are correlated. Secondly, we consider a challenging specification, whereby any arbitrary text perturbations are allowed on multi-modal (image and text input) classifiers. This highlights the vulnerability of multi-modal classifiers to text attacks. The proposed algorithm improves the state of the art verification accuracy by up to 25%.
Multi-modal data is used in various domains including social media, and the internet in general. We believe that our work could find application in verifying classifiers which label advertisements and social media posts as illegal or hateful. Although we tackle arbitrary perturbation in the text input, our work does not verify against all possible perturbations on the multi-modal input. Another limitation is that we have considered only a particular class of multi-modal architectures. It is also important to verify other commonly used architectures. Further, verification exposes flaws in neural network models, which on the one hand can help improve their robustness, but on the other hand, can be exploited by an adversary.
Acknowledgements and Disclosure of Funding
Harkirat was supported using a Tencent studentship through the University of Oxford. Philip H.S. Torr was supported by the EPSRC grant: Turing AI Fellowship: EP/W002981/1, EPSRC/MURI grant EP/N019474/1 and the Royal Academy of Engineering. We also thank Rudy Bunel for feedback on the draft.

Review summaries:
This paper proposes to use probability simplex specifications for robustness verification. With the simplex, the convex hull for relaxing activation functions can be made tighter using a newly proposed upper bound for relaxation. Then the simplex specification and the new relaxation are used in solving the verification problem in a manner similar to backward bound propagation in CROWN, and the relaxation parameters are optimized with projected gradient ascent. By applying the method to $\ell_1$ robustness verification, and also a multi-modal setting with text perturbation, experiments show that using the simplex specification with the proposed method leads to better verified accuracy and low verification cost. 

The paper proposes a new convex relaxation for verifying neural networks with convex activations with specifications defined over simplex inputs. These convex relaxations are more precise than the triangle relaxation from Ehlers et. al and based on computing the convex hull of the set {(x,f(w.x+b))} where x belongs to a simplex and f is a convex activation function. The size of the resulting relaxation is linear in the number of neurons. Building on this, the authors develop a verification algorithm that propagates simplex input through the network and a solver for solving the verification problem posed as an optimization problem based on the obtained convex relaxations. The experimental results show that the verifier developed in this work is more effective than prior work.

This paper proposes an efficient bound propagation method for verifying the robustness of neural networks under L1 (simplex) constraints. The authors show that for the L1 norm setting, the convex hull for a linear and relu layer can be exactly computed efficiently, unlike the setting for Linf norm. Then, the authors designed an efficient algorithm that uses a single pass of backward bound propagation to solve the resulting linear programming problem. The bound propagation algorithm has optimizable parameters that can be optimized to achieve the tightest bound.

The paper proposes  a particular relaxation for the verification of neural network robustness under perturbation that can be phrased as functions over the probability simplex (e.g. $\ell_1$-norm).  Mathematically, the verification is first phrased as an optimization problem, that mirrors the layer structure of the neural network. For the ReLU (or other convex activation functions) they employ the well-known convex relaxation from [Ehlers, 2017]* ("Planet") and improve upon it by a new upper bound, which utilizes the fact that the input (and all intermediate neuron values post-activation) are subject to a simplex constraint. This relaxation forms the convex hull of the possible values of a post-activation neuron and thus is tight (for a single neuron). The resulting optimization problem forms a linear program with 2 linear lower bounds, 2 linear upper bounds and a simplex constraint for each neuron. To allow for faster and more scalable evaluation the optimization problem is relaxed following the approach of [Zhang et al. 2018]. The 2 upper and lower bounds are relaxed into one each, that is a linear interpolation weighted by an $\alpha  \in [0, 1]$. In this formulation the optimum of the problem can be found by alternatingly computing the neuron bounds (as a function of fixed $\alpha$) and optimizing the values of $\alpha$ via gradient decent.  Experimentally the authors show that both, the relaxed version and the linear program version outperform Plant relaxations in terms of certified accuracy by a large margin on image classification (MNIST and CIFAR-10) under $\ell_{1}$ perturbations and robustness to text-perturbations for BoW-representations in an multi-modal setting (simplified Food-101). The relaxed version almost matches the linear program version in performance, but is significantly faster.  *Citations in the [Name, Year] format refer to citations in the paper.