Overcoming the Convex Barrier for Simplex Inputs
Authors: Harkirat Singh
M. Pawan Kumar
Philip Torr
Krishnamurthy Dj Dvijotham
Venue: NeurIPS 2021 Poster (2021)
Keywords: Neural Network Verification
Optimisation for Deep Learning

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 $\ell_\infty$ 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 $\ell_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. 

Overcoming the Convex Barrier for Simplex Inputs
Harkirat Singh University of Oxford harkirat&robots. ox ac. uk
M. Pawan Kumar DeepMind mpavan@deepmind.com com
Philip H.S. Torr University of Oxford
Krishnamurthy (Dj) Dvijotham DeepMind dvi dvij@google.com
phst@robots ox. ac
Abstract
Recent progress in neural network verification has challenged the notion of a conver 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 neural network to Lo 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 input perturbations within the probability simplex. We prove 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 É robustness for CIFAR-I0 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.
Introduction
Verification refers to the challenging computational problem of determining whether a neural network satisfies given specification. Perhaps the most popular specification is prove disprove that neural network classifier robust to perturbations of the input that lie within an Lp ball (de Palma
al. a0 Wong and Kolter 2018 Zhang al. 20188 Weng al. 2018 Mirman al. 2018 Dvijotham et al. 20188, with impressive state of the art results recently achieved in Wang et al. [2021]
The ability verify neural networks would open the door 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, is unsurprising that 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 conver burrier, 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 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 successfully overcome this barrier. Specifically, Anderson et al. [2019] proposed a tight relaxation that precisely defines the convex hull of composition of linear function of vector within an for ball with the ReLU non-linearity. While their relaxation has 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
primary reason for the slow convergence of branch-and-bound
35th Conference on Neural Information Processing Systems (NcurIPS 2021).

---

primal [Anderson et al., 2019], active sets to solve the dual de Palma et al. 202 a b] approximate linear bound propagation algorithms (Tjandraatmadja et al. 2020
and even
Buoyed by the possibility of realizing practical verification using tight relaxations, we consider an important specification, namely, robustness perturbations that lie in probability simplex. Examples of such specification include robustness to & 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 linear transformation of the probability simplex with a convex non- non-linearity such as ReLU or SoftPlus. Somewhat surprisingly. we show that, unlike the previously considered case of lo 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 novel technique to propagate the simplex constraints through the hidden layers of the network, we derive tight relaxation for the output of network whose size scales linearly with the size of the network. Furthermore, we suitably extend 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 & perturbations for MNIST and CIFAR-I0 10 classification. Our method achieves 13.6% higher verified accuracy on MNIST and up to 14.4% higher verified accuracy on CIFAR-10 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, 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 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 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.
consider the Food
Preliminaries
We provide a formal mathematical description of our verification problem, and briefly discuss the existing relaxations in order to contextualise our contributions.
2.1 Problem description
probability simplex as Am. that is, Am = fx E RT x 2 0, < 13. As mentioned in the previous section, we are inter- ested in verifying specifications of given neural network when its input is constrained to lie in simplex. We focus on networks with a layered architecture to keep notation simple, but our ideas casily extend to any fordadd network, including residual networks. We consider neural network with n layers. Each layer is assumed to be composed of two operations: (i) an affine operation (fully connected layer convolution layer), which denote by L=(:); and (ii) a non-linear activation function, which we denote by o-).. In other words, given its input Tg-1 E R**-1, the k-th layer performs the operation कh (=(xx-1) E RT* followed by 3 = (.x)) Rm*, While we place no restriction on the linear operation, we make the following assumption on the activation function.
We denote the m-dimensional
We assume that the activation function is an element-wise convex function (for example, ReLU or SoftPlus).
Assumption 1.
Verification problem: Using the above notation, the verification problem we solve can be formu- lated as
min (.x))
(1a)

---

s.t. 2x = Lx (x , 2 =(b+)
k E [p]]
(Ib)
2o E Ano
(1c)
where [n] denotes the set {l.... n... The objective function & is scalar-valued linear function of the output of the final layer of the the network. For example, say we wish to verify that classification network is not vulnerable to any adversarial attacks. In this case, we define V as the difference between the true logit and target logit outputted by the network. The sign of the optimum value of
problem ( 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.
& perturbations: Consider a network with a continuous valued input æ E Rm We are interested in verifying the behavior of the network under input perturbations that lie within & ball: fæ x æ²|11 S c}. This imput domain can be reformulated simplex as
1 0
0
0
0
0
0
1 -1
0
0
x eM A2m:
M (mX2m)
0
0 0
Bag of words models: Consider a text classification network that takes text as input and makes predictions based on 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 precomputed set like GloVe [Pennington al. 2014] Word2Vec [Mikolov et al., 2013). Next, take the mean of the word embeddings to obtain the final representation. We denote the word embeddings as a matrix E E Rdxx", where each d-dimensional column represents embedding of putative word in vocabulary of size v. Using the above matrix, the text embedding is given by Ex where æ represents the normalized counts of words from the vocabulary in the text. In other words, æ E A, assuming that arbitrarily long text with arbitrary numbers repetitions of each word in the vocabulary are allowed.
2.2 Planet and disjunctive relaxations
Ehlers 2017 proposed a convex relaxation for the ReLU activation function, which 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: 2 w + b where
RTM followed by y = Re)U(@). To this end, it utilizes lower and upper bounds on &. In our case, since & E Am. we can compute the bounds as i = Wmin + < w" x + < Wmax + = ü. Here, Wmin and Wmax denote the minimum and maximum entries of w respectively. Using the bounds on J, the Planet ReLU(w" x + b), x E Am} is defined as
relaxation for the set S {u, x
PA y 2 T
x + b. y 2, û
w x + + +-b-)) i). x Am
(3)
In Anderson et al. [2019 2020], the authors propose a tighter relaxation and characterize the exact convex hull of the set
{(x, relu (w x + 6)) : x S u).
However, this characterization involves exponentially many inequalities. And efficient algorithms based on need to resort to cutting plane methods, adding violated incqualities sequentially. Doing so is computationally challenging and requires significant effort to implement in 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, 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 al. 2020 is limited the maximum of two affine functions.
3

---

3 A Concise Convex Relaxation
In this section, we derive our novel tight convex relaxation for problem ( In order to make the exposition clearer, we assume that we have access to simplex constraints for all æR. k E [n 1]. As will seen in the next section, such constraints can be derived by propagating the simplex constraint on the input Zo through the network.
3.1 An exact convex relaxation for a single neuron
We begin by considering the simple case of single neuron, which will form the building block of our final relaxation. Similar to the previous relaxations, we consider the set S = {y. y = aw x + 6). }m where a is convex activation function, for example ReLU. We aim to characterize the convex hull CHa of the set S.
Theorem 3.1. The convex hull CHa of S is defined by the following convex constraints
y 2 (w"a x b), E Am:
(4a)
y - Σ xi (a (w" et + b) (b)) + (b),
(4b)
where e ERT, e RR 1, OVj A denotes the i-th coordinate vector in RRm.
By the definition of a convex hull, the proposed relaxation the tightest possible relaxation for single neuron with æ E Am. Note that, when a is the ReLU activation func- tion, the only difference between the proposed relaxation and the Planet relaxation PA is the upper bound on y. Fig- ure compares the upper bound of the Planet relaxation PA with the proposed relaxation CHA for the case where m = As can be seen, our relaxation is significantly tighter than Planet, which paves the way for tractable ver- ification over simplex inputs. The following proposition formally characterizes the difference between the tightness of CHA and PA-
24
Proposition 3.2. For any input dimension m, CHA is provably tighter than Pa. Specifically, we can characterize the gap between CH and PA by the gap in the optimal value of the problem
Figure 1: The input domain is shown in light blue, while the out- put function y ReLU(w" x + b) is shown in blue. It can be seen that the upper bound corresponding to the Planet relaxation (shown in green), is signifi- cantly looser comparison the upper bound corresponding to the proposed re- laxation (shown in orange). Even the Anderson relaxation (shown in yellow) is much looser than our relaxation.
A
max y - y' subject (y.x) PA. (3/ E CHA
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 pro- vided in the supplementary material. The proof of Theo- rem 3.J Jutilizes a fundamental result from convex analysis, that any linear function obtains the same maximum value over S as over its convex hull CHA.
Note that our relaxation overcomes the convex barrier by providing bounds that are significantly tighter than the Planet relaxation. Convex barrier is term introduced in Salman et al. (2019), which defined as the gap between the optimal value of the original verification problem and the optimal convex relaxation of the non-linearity.
Comparison to Tajandraatmadja et al. 2020 inequalities to describe the convex hull for the composition of a linear function with convex activation function for simplex inputs. 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 Tjjanraatmadjaa et al.] [2020) can help us understand the discrepancy. The method makes use of the Kuhn triangulation of [0, 1 [Todd 1976), which
Our relaxation requires only linear number of

---

describes the collection of simplices whose union is 10", and requires an exponential number of simplices. Since 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 linear number of inequalities. Note that the input simplex A, not one of the simplices from the Kuhn triangulation whose union is the unit hypercube. We provide visualization for this intuition in the supplementary material.
3.2 Final relaxation
Using the convex hull for single neuron, we can now describe our overall relaxation. Recall that we have assumed æy E An. for each &t E [n - 1]. This is ensured through a simplex propagation algorithm described in the next section. In addition, we also compute interval bounds on the pre- activations &R E [ex, ug.. Using the interval bounds, we define 0g = "a- 7 = -l,+ uy (œ) = (L+ (0)))
(Lx (0)). Furthermore, since &n is itself a linear function of #n-1, with a slight overload of notation, we denote the objective function of relaxation V (x:,1))- Using the above notation, the overall proposed convex
8g O (Lx (x) - >w) and u (a) E, (o (Lx (ei))
relaxation problem (T) for the ReLU activation function can be written as
min m
V (In-1)
(5a)
s.t.
3y 2 Lx (xk-1) 1) 1) 20 20
k E [n 1], (Planet lower bound)
(5b)
2s S u (xx-x11);
k E [n 1]. (Planet upper bound)
(5c)
S u/g (2x-1))
k [n 1), (from equation 4b
(5d)
Bx A
k E {0) U
(n - 1].
(5e)
Similar relaxations can be derived for other convex activation functions by linearizing the convex function around given point. However, we focus on the ReLU case for brevity of exposition, particularly since ReLU is the most commonly used convex activation function.
Algorithm
Our verification algorithm is composed of two phases: (i) propagating simplex constraints the activations at every layer; and (ii) computing a lower bound on problem (I). We describe these in the following subsections.
4.1 Simplex propagation
We assume that the output of each layer is non-negative. If this is not the case, we can simply add constant to the activation of each layer that the output becomes non-negative, Let us denote hg (x) a (L& (æ)). Since hx(() is an element-wise convex function of its inputs, h4'h(,, (.) is also a convex function. Using the fact that the maximum convex function over the simplex is attained at one of the vertices, it can be shown that the following inequality holds true
Σ The S
max JE(0....AZ-1>
1T (e²) = ag.
(6)
Here, Tia denotes the i-th coordinate of the vector of activations 2% at the output of layer hg-
Note that the above inequality can be rewritten in the form Σ, 2.s S 1, where Eيs = usi so that
au
we can propagate simplex-lit like constraint simply by rescaling activations at the layer appropriately. Details for conditioning the intermediate layers into simplex using inequalities the above form are provided in the supplementary material.
4.2 Efficient solver
The optimization problem 5 a Linear Program and as such can solved easily by off-the-shelf solvers [urrbbi.. 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.
5

---

Zhang et al. (2018), Singh et al. 2019] developed efficient solvers for relaxations that rely on bounds on the output 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] at. 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 form that can be solved efficiently using single backward pass. Concretely, we combine the lower bounds (5b) and the non-negativity constraint from (5e) into single lower bound using weighting coefficients ag. We also combine the upper bounds (ncland [d) into a single upper bound with weighting coefficients di. The values of the weighting coefficients ag. and aj constrained to lie between 0 and 1. This leads to the following optimization problem
L(a, a) min
V (In-1)
(7a)
s.t.
3g E
(7b)
2 Og
④ 1x (ak-1)
k E In 1}, k E in 1].
(7c)
a up C 1) + + - ax ) @ u' (Ix-1)
(7d)
It turns out that the above formulation can be solved efficiently by a single backward pass over the network. In order derive the solution, is useful to introduce the notion of decomposition of an affine function into monotone, anti-mot monotoo and constant parts.
Definition 4.1. For any scalar-valued affine function ʃ (a=), define
0f
V, 1 (x) min Of dxx 1) x, l f
8+ (x) max
Zx'
so that (ax) = 5+ (x) S (x:
/e
Since f+ only involves the positive coefficients in the gradient of f. it is monotonically increasing, and similarly, / is monotonically decreasing. Exploiting this and the fact that V is a scalar valued linear function, we obtain
V (In-1) = + (In + Vp (In-1) 1) + Vo
2 V an-1 O Un-1 (x + (1 an- A 1 (#n 1)) + 1 (an-1 ② Ln-1 (Øn 2))
The lower bound above is an affine function of xx-2 and hence leads to a recursive algorithm where compute lower bounds the specification expressed as a function of 2k-1 given lower bound on the specification expressed as a linear function of ætg-
Therefore, this leads to a recursive algorithm for computing lower bound on the optimal value of
77. that is presented the Subroutine SIMPLEX BACKWARD function on line II in Algorithm It can in fact be proven that this is the exact optimal value, using argument similar to Salman et al. 2019]. Section 3.
The computation required to express a lower bound on the specification given as linear function of #++1 to a lower bound expressed as linear function of x shown on line (14) of Algorithm[[] 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 and its value at which gives the vector of coeffients and the bias term of the affine function of Thus, the cost of implementing line of of the algorithm is equal to the cost performing backpropagation through a single layer of the network.
Denote the projection onto the unit hypercube as π (x) min (max (æ,, 0) 1). Our overall algorithm is presented in Algorithm [] It consists of two main functions SIMPLEX BAACWARD and SIM- PLEX VERIFY. The SIMPLEX BACKWARD algorithm computes (a, a) for 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 with respect to a, a to obtain the tightest possible lower bound on the (equation]] D]. The idea of optimizing the weighting coefficients a, a to obtain tighter bounds is inspired from the algorithm of Xu et 2202), with suitable adaptations the setting involving novel relaxation.

---

Proposition 4.2. Algorithm computes a lower bound on the optimal value of T
Proof. Follows by recursively applying the lower bound at each layer while defining fk-
The complexity of SIMPLEX BACKWARD function for com- puting bounds for given value of a' a', is the same as the cost of two backward passes through the network. This is twice the cost of CROWN [Zhang et al. 2018 one iteration of auto-lirpa Xu ct al. 2021]. which uses a single backward pass.
Computational Complexity:
Algorithm Simplex Verify
1: function SIMPLEX VERIFY
2: Initialise a and à with values between 0 and
3: for E [0, Emaz - 1] do
4: I(a', @') = SIMPLEX BEEESK__AKWAAWWWCCC a'
5:
Compute gradients dL dL da da via backpropagation
6: a++1 a + update gradient ascent (or Adam)
7: a++1 a ++ t (a' ( (1t+1)
(projection)
8: end for
9: return L(a"+1, 1(a+11a'+)) a
end function
11: function SIMPLEX BACKWARD(W, a.a)
12: fN +
13: for k E [n 1, do
14: Set fü (x) + skti (Tx uu (m) + ax) 3 un (a)) + fbt1 (a, @ LG (a)) + +8++1-
15:
end for
16:
I(a, a) min fo (ar))
17:
return L(a,a a)
18:
end function
Experiments
In this section, demonstrate the effectiveness of the proposed method specifications: (i) robustness to & perturbations for image classifiers (Sec 5.1). and (ii) robustness of multi-modal classifiers text perturbations (See 5.2).
5.1 E robustness verification
Experimental Setup We verify the l robustness of networks from de Palma et al. 2021a Bunel al. 2020b) and VNN-COMP [020]. We compute the lower bound the robustness margin (difference between the ground truth logit and the other logits) using the verification methods. An image is said 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-I0 we evaluate on 1000 random images from the test set (Krizhevsky and Hinton [2009]. The MNIST and CIFAR-10 datasets are widely used the machine learning community, and available under the creator's '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 & de-eecentt attack) from Tramer and Boneh 2019 with c 0.3 for all networks except the VNN-comp big network, which is trained with e = 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 | We also test on the SGD trained CIFAR Wide model from de Palma et al. 102 We verify robustness against input perturbations lying & 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.

---

Dataset
MNIST
CIFAR-I0
OVAL
OVAL
OVAL
OVAL
OVAL
VNN Med
VNN
Model
Wide SLIDE
Base
Wide
Deep
Wide
Big
Training
SLIDE
SLIDE
SLIDE
SGD
SLIDE
SLIDE
Nominal
98.8%
75.1%
79.3%
72.1%
74.4%
81.4%
83.6%
Accuracy
Pgd
98.2%
73.5%
77.0%
69.8%
73.3%
80.5%
82.3%
Gurobi Planet
31.7%
34.1%
18.4%
11.1%
13.5%
Verified
Gurobi Simplex
45.2%
48.6%
29.4%
13.4%
23.7%
Accuracy
Opt-Lirpa Planet
31.0%
33.6%
17.9%
10.8%
13.5%
48.8%
60.0%
Simplex Verify
44.6%
48.0%
28.8%
13.4%
22.4%
59.4%
66.4%
Gurobi Planet
74.61s
22.80s
114.92s
86.84s
114.70s
Verified
Gurobi Simplex
72.47s
22.95s
72.17s
59.22s
70.42s
Time/Sample
Opt-Lirpa Planet
0,04s
0.04s
0.04s
0.06s
0.04s
0.05s
0.06s
Simplex Verify
0.04s
0.04s
0.04s
0.05s
0.04s
0.05s
0.06s
Table I: Verified accuracy and verification time different solvers on MNIST and CIFAR-10 10 models.
test on the entire test set for MNIST, and random 1000 test images for CIFAR-I0. 10. Simplex Verify denotes our proposed solver. Our proposed method achieves much higher verified accuracy in comparison to the state of the art baseline, in the same amount of time. *-" denotes instances not solved within 5 minute timeout.
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] [017) 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) 17-4960X CPU @ 3.60GHz processor. We also compare against optimized LiRPA solver for the Planet relaxation [Ehlers] 2017]. and refer to as Opt-Lirpa Planet. The solver remains the same 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 our solver described in Sec 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- poper-parametent are provided in the supplementary material.
solver, with the only difference being that the upper bound corresponding
Results Table [ 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 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 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 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
We also compare the tightness of the bounds achieved by differrntt methods. We obtained the lower bounds provided by different solvers. We can get the upper bounds using the sparse PGD attack, SLIDE [Tramer and B 2019]. A smaller gap between the PGD upper bound and verified lower bound, indicates tighter verifccttonn Figure2a|shan shoss 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 26 shows the pointwise comparison of the gap for Opt-Lirpa Planet and our Simplex Verify. Simplex Verify achieves much tighter verification.
8

---

Tamang th
Gap.a Td
Tmmy
Cap 12 Plgt
372-
238
Chart Streeee 30
220
9.28
343
4h
Gundb andt
Surdd Manes
Up: and
(a) Comparison of runtime (left) and gap of lower (b) Comparison of runtime (left) and gap of lower bounds PGD upper bounds (right), for Gurobi bounds PGD upper bounds (right), for Simplex Verify and Opt-Lirpa Planet.
Simplex and Gurobi Planet.
Figure 2: Pointwise comparison of the lower bounds CIFAR- 10 test set on the adversarially trained Wide
model, for a subset of the methods. Darker colour shades mean higher point density (on logarithmic scale). The oblique dotted line corresponds to the equality.
5.2 Multi-modal classifier robustness verification
Experimental Setup In this section, we are interested in verifying the robustness of multi-modal classifiers text-based attacks. The motivation are scenarios where image based models are aug- mented with text to improve the accuracy of the classifier. However, this makes the model vulnerable to text based attacks. The aim of this experiment 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 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 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 the attack. The aim of this specification is to characterise the worst-case sensitivity of the model. We 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- 152ett--12221 model. It also extract a Bag of words embedding for the text. The model concatenates the embeddings and feeds them into 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 offte--o--h-arrr ahe 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 10 classes. More details are provided in the supplementary.
Related Work Huang et al. [2019) considered verification against synonym replacements or char- acter flip perturbations text classification models. The input specification was modeled simplex and they proposed to use Interval bound propagation (IBP) for the same. Concurrent to Huang et al. 2219]] Jia et al. [0119] considered a specification where every word in the text can be replaced with similar word and used IBP. Xu et al. [2020) use more recent LiRPA variants for verification of synonym-bor based word substitution with a maximum of 6 word substitutions. Concurrent to our work, Bonnerrt et al. [2021) proposed new method for certifying Transformers to synonym based attacks. They provide lifting from for 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 any setting. 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 composition over a convex activation function and an activation function where the input is constrained to be the simplex, and propose an efficient algorithm for the relaxation. It is also important to note that we perform experiments on verification-agnosti 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
http::/visiir 111p..

---

PGD upper bounds for Opt-Lirpa Planet and Simplex Verify. Note here that smaller gap indicates tighter verification. For 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 []] we present the verified accuracy achieved by the different methods with the nom- inal and Pgd accuracy. We present results for networks trained with different weighting for nominal and PGD loss during the adver- sarial training. Network trained only on im- ages achieves 87. 37.82% accuracy. Note that our method achieves remarkably higher verified ac- curacy, up to 25% higher, as compared to Opt- Lirpa Planet in the same amount of time. This shows the benefit of our approach over the exist- ing solvers.
22
Simplox Vartee
15.0
Opt-Lipa Flanes
Opo4 Plantt
Figure 3: Pointwise comparison of runtime (left) and gap of lower bounds to PGD upper bounds (right) for the global specification on Food-101 dataset.
Discussion and Broader Impact
As machine learning continuously finds new ap- plication domains, the robustness of machine learning systems in the face of adversarsarial behavior becomes increasingly relevant. Neu- ral network verification, which seeks to obtain provable guarantees on robustness of neural networks, has mostly focused on fo perturba- tions. However, real security threats often in- volve more drastic changes that could lead to arbitrary perturbations the input. this paper, we have we have proposed an efficient algorithm for verification of neural networks against sim- plex constrained perturbations. We have shown the practical importance of this specification through two applications. Firstly, we verify the ro- bustness of image classifiers to & perturbations, which could be an appropriate threat model when perturbations of different features are correlated. Secondly, we consider a challenging specification, allowed 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 verification accuracy by up to 25%.
Nominal Pgd
86.3%
87.3%
92.3%
Accuracy
84.7%
84.5%
19.2%
Verified
Opt-Lirpa Planet
17.9%
08.0% 08.00%
01.2%
Accuracy
Simplex Verify
42.2%
32.8%
01.3%
Table 2: Verified accuracy achieved by different solvers on the 2164 test images of the reduced Food-10 101 dataset. Results are presented for networks trained with differ- ent weighting for nominal and PGD loss. Our method (Simplex Verify) achieves up to 24% higher verified ac- curacy, in the same amount of time as the state of the art baseline Opt-Lipra Planct.
whereby any arbitrary text perturbations
Multi-moda data is used 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 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 adversary.
the multi-modal input. Another limitation
Acknowledgements and Disclosure of Funding
Harkirat was supported using Tencent studentship through the University of Oxford. Philip H.S. Torr was supported by the EPSRC grant: Turing AI Fellowship: EP/W002981/1 1/1, EPSRC/MURI grant EP/N019474/1 and the Royal Academy of Engineering. We also thank Rudy Bunel for feedback on the draft.
References
R. Anderson, J. Huchette, C. Tjandraatmadja, and Vielma. Strong mixed-integer programming formulations for trained neural networks. Conference on Integer Programming and Combinatorial
10

---

Optimization, 2019.
R. Anderson, J. Huchette, W. Ma, C. Tjandraatmadja, and J. P. Vielma. Strong mixed-integer programming formulations for trained neural networks. Mathematiccal Programming, 2020.
G. Bonaert, D. I. Dimitrov, M. Baader, and M. Vechev. Fast and precise certification of transformers. In PLDI, 2021.
R. Bunel, A. De Palma, A. Desmaison, K. Dvijotham, Kohli, P. H. Torr, and M. P. Kumar. Lagrangian decomposition for neural network verification. Conference Uncertainty in Artificial Intelligence, 2020a.
R. Bunel, J. Lu, I. Turkaslan, P. Kohli, P. Torr, and M. P. Kumar. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(2020), 2020b.
A. de Palma, H. Behl, R. R. Bunel, P. Torr, and M. P. Kumar. Scaling the convex barrier with active sets. In International Conference on Learning Representations, 2021a.
A. de Palma, H. S. Behl, R. Bunel, H. S. Torr, and M. P. Kumar. Scaling the convex barrier with sparse dual algorithms. CoRR, 2021b.
G. W. Ding, L. Wang, and X. Jin. AdverTorch v0.1: An adversarial robustmess toolbox based on pytorch. arXiv preprint 1502.0990.070000 2019.
K. Dvijotham, R. Stanforth, S. Gowal, T. Mann, and P. Kohli. A dual approach to scalable verification of deep networks. Uncertainty in Artificial Intelligence, 2018.
R. Ehlers. Formal verification of piece-wise linear feed-forward neural networks. Automated Technology for Verification and Analysis, 2017.
S. Gowal, K. Dvijotham, R. Stanforth, R. Bunel, C. Qin, J. Uesato, R. Arandjelovic, T. Mann, and P. Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv: 121. 2018.
Gurobi. CRLhhtpp:/ htttp://www.gurol/ com/
I. Gurobi Optimization. Gurobi optimizer reference manual, 2020. URl.htttp://www.gueee http://wwwwwroboccoo
P.-S. Huang, R. Stanforth, Welbl, C. Dyer, D. Yogatama, S. Gowal, K. Dvijotham, and P. Kohli. Achieving verified robustness to symbol substitutions via interval bound propagation. In EMNLP, 2019.
N. L. Ignazio Gallo, Gianmarco Ria and R. L. Grassa Image and text fusion for upmc food-101 using bert and cnns. In International Conference on Image and Vision Computing New Zealand (IVCNZ 2020). 2020.
R. Jia, A. Raghunathan, K. Göksel, and P. Liang. Certified robustness to adversarial word substitutions. In Proceedings of the 2014 conference on empirical methods in natural language processing (EMNLP), 2019.
G. Katz, Barrett, D. Dill, K. Julian, and M. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. International Conference on Computer-Aided Verification, 2017.
D. Kiela, S. Bhooshan, H. Firooz, and D. Testuggine. Supervised multimodal bitransformers for classifying images and text. 2019.
D. P. Kingma and J. Ba. Adam: A method for stochastic optimization. International Conference on Learning Representations, 2015.
A. Krizhevsky and G. Hinton. Learning multiple layers of features from tiny images. Master's 's thesis, Department of Computer Science, University of Toronto, 2009.
Y. Lecun. The mnist database of handwritten digits. htnp//yann.lecune http://aam.leuuu..co/eebbmmmi// com.eedd/mnssi////.o. URL
https: //cci mii ac actpp//aaid//////////ooaaaa

---

J. Lu and M. P. Kumar. Neural network branching for neural network verification. In International Conference on Learning Representations, 2020.
Mikolov, K. Chen, G. Corrado, and J. Dean. Efficient estimation of word representations vector space, arXiv preprint M.Kiv:3301.37800 2013.
M. Mirman, T. Gehr, and M. Vechev. Differentiable abstract interpretation for provably robust neural networks. International Conference on Machine Learning, 2018.
J. Pennington, R. Socher, and C. D. Manning. Glove: Global vectors for word representation.
In Proceedings of the 2014 conference on empirical methods in natural language processing (EMNLP), pages 1532-1543, 2014.
H. Salman, G. Yang. H. Zhang, C.-J. Hsieh, and P. Zhang. A convex relaxation barrier to tight robustness verification of neural networks. Neural Information Processing Systems, 2019.
G. Singh, T. Gehr, M. Püschel, and M. Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM Programming Languages, 2019.
C. Tjandraatmadja, R. Anderson, J. Huchette, W. Ma, K. Patel, and J. P. Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. arXiv preprini arXiv:2006. 14076, 2020.
M. Todd. The Computation of Fixed Points and Applications. Lecture Notes in Mathematies; 513.
Springer-Veriee 1976.
F. Tramer and D. Boneh. Adversarial training and robustness for multiple perturbations. In Advances in Neural Information Processing Systems, volume 32, 2019.
VNN-COMP. International verification of neural networks competition (VNN-COMP), Verification of Neural Networks workshop at the International Conference Computer-Aided Verification, 2020. BRLLhttps: h/tp::://sitees google. com/ wiwevvveiiiiiieeeee
S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv: 203.v::00030624 2021.
X. Wang, D. Kumar, N. Thome, M. Cord, and F. Precioso. Recipe recognition with large multimodal food dataset. 2015 IEEE International Conference on Multimedia Expo Workshops (ICMEW). 2015.
T.W. Weng, H. Zhang, H. Chen, Z. Song, C.-J. Hsieh, D. Boning, I. S. Dhillon, and L. Daniel. Towards fast computation of certified robustness for relu networks. International Conference on Machine Learning, 2018.
E. Wong and Z. Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. International Conference on Machine Learning. 2018.
K. Xu, Z. Shi, H. Zhang, Y. Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances Neural Information Processing Systems, 33, 2020.
K. Xu, H. Zhang, S. Wang, Y. Wang, S. Jana, X. Lin, and C.-J. Hsich. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers, 2021.
H. Zhang, T.-W. Weng, P.-.. Chen, C.-J Hsieh, and L. Daniel. Efficient neural network robustness certification with general activation functions. In Advances in neural information processing 2018
systems, pages
12


Reviews:
[{"review_id": "ZRl_gUsEJ-C", "reviewer": "Reviewer_3E9J", "summary": "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.", "questions": "", "limitations": "", "rating": 7, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strengths:\n\n1. The paper has an exciting theoretical finding that when L_1 norm perturbation is used on input x, the convex hull of a relu and a linear layer can be exactly and efficiently computed. Unlike the case where the input x has a Linf norm perturbation (Tjandraatmadja et al., 2020), in the L_1 norm case there is only one simple linear upper hyperplane rather than potentially exponentially many in the number of neurons. This is a quite important finding showing that the difficulty of getting tight convex relaxations for different norms might be quite different, and may inspire future research on investigating additional norm constraints.\n\n2. With the help of the simple and tight convex relaxation, the authors developed an efficient bound propagation based algorithm in the same spirit of CROWN (Zhang et al., 2018). This allows us to compute verification bounds very efficiently and also makes it possible to use GPU accelerators and scale to large networks. Additionally, like the optimized CROWN bounds in (Xu et al., 2021), the proposed bound propagation procedure can also be optimized to achieve the tightest possible relaxation. This is very useful for obtaining tight bounds.\n\n3. Experimentally, the proposed approach achieves much better L_1 norm verified accuracy compared to existing Planet relaxation based verifiers such as Optimized CROWN/LiRPA, and much faster than Active Set based verifiers.\n\n\nImprovements that can be made:\n\n1. The simplex propagation in section 4.1 can produce loose bounds when the network is deep. It looks like an IBP-like bound for the L1 norm, which is exact for one layer but can become increasingly loose when propagating to later layers. Why not use the efficient solver (Section 4.2) to solve each layer's simplex constraints $\\alpha_k$ by treating $1^T h_k(x)$ as the objective? This was also done in a recursive manner in the original CROWN algorithm - the intermediate layer bounds are also computed via CROWN, rather than IBP. This also enables joint optimization of intermediate layer's bounds (here it is L1 norm simplex) in a similar manner as (Xu et al., 2021), which can potentially significantly improve the results.\n\n2. In experiments, it seems both Opt-LiRPA and Simplex Verify are very fast on the MNIST and CIFAR-10 models under testing. Ideally, to better demonstrate the scalability of the proposed method, a few larger networks should be included into evaluation (e.g., you can look for appropriate networks in VNN COMP).\n\n3. The epsilon used in experiments are fairly small, and PGD attack accuracy is very close to the nominal accuracy. For evaluating the attack accuracy in the L1 norm setting, you can try the EAD attack [1] which is specifically designed for the L1 norm case. This can probably reduce the gap between attack accuracy and verified accuracy.\n\n4. I think theorem 3.1 is the most important result of this paper, and it might be worthwhile to have more discussions on this and give some insights on why adding the simplex constraints on x allows an efficient relaxation, and why an efficient relaxation is not possible for Linf norm case.\n\nMinor questions:\n\n1. For Opt-LiRPA are the intermediate layer bounds jointly optimized like in (Xu et al., 2021)? Based on the algorithm listed in the appendix it seems not?\n\nOverall, I feel this paper makes a significant contribution to the neural network verification problem, and I support the acceptance of this paper. However I hope the authors can further work on the possible improvements mentioned above to make this paper more solid.\n\nReferences:\n\n[1] Chen, Pin-Yu, Yash Sharma, Huan Zhang, Jinfeng Yi, and Cho-Jui Hsieh. \"Ead: elastic-net attacks to deep neural networks via adversarial examples.\" In Thirty-second AAAI conference on artificial intelligence. 2018.\n\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "No potential negative societal impact.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "5"}, "extra_text": {}}, {"review_id": "X03_puKurV8", "reviewer": "Reviewer_vqRE", "summary": "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).\n\nMathematically, the verification is first phrased as an optimization problem, that mirrors the layer structure of the neural network.\nFor 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).\nThe resulting optimization problem forms a linear program with 2 linear lower bounds, 2 linear upper bounds and a simplex constraint for each neuron.\nTo 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.\n\nExperimentally 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.\n\n*Citations in the [Name, Year] format refer to citations in the paper.\n", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "The work seems relevant to the community and technical parts are well presented and are clear about their limitations. The mathematical arguments seem correct.\nHowever, outside of the mathematical parts, the text and presentation of the paper seems rushed: formulations are repeated within the same argument (particularly in Section 5 or L204/207), Figure 1 makes it hard to see the difference between the bounds, and for Theorem 3.1 it may be useful to the reader to state the key idea of the proof (linear functions attain the same maxima over both $\\mathcal{S}$ and $\\mathcal{CH}$).\n\nThe work seems well connected with related works (with the notable exception of [1], which describes a similar algorithm to [Zhang et al. 2018b]*)\n\nQuestions:\n- Can you provide further motivation for simplex constraints beyond $\\ell_1$ and bag-of-words? Can you approach be used as a building block to handle self-attention layers (which usually form a probability simplex) in neural networks even if the input specification is not in the simplex constraint?\n- Can you contrast your work with [2]? They also seem to provide a lifting from $\\ell_{\\infty}$ analysis techniques to other norms (and thereby the simplex constraint from $\\ell_{1}$). (As the work is more-or-less parallel I don't expect a full numerical comparison.)\n- While your focus is mostly on convex activation functions, could you also handle S-shaped activation functions like [Zhang et al. 2018b, 1]? (I assume their bound, based on the upper and lower bound pre-activation would also work for you.) Is the key issue preventing this the argument from L173?\n- Am I correct in assuming that Gurobi Simplex in Section 5 utilizes the relaxation presented in 3.2?\n\nMinor:\n- L117, bad line break before the fullstop.\n- L125 should likely be $\\mathbf{x}_{k}, k \\in [n-1]$.\n- Figure 4 should be a Table.\n\n*Citations in the [Name, Year] format refer to citations in the paper, while [Number] citations refer to:\n\n[1] An Abstract Domain for Certifying Neural Networks, Singh et al., POPL'19\n\n[2] Fast and Precise Certification of Transformers, Bonaert et al., PLDI'21\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "The authors do briefly consider the broader impact of their work, in a way that seems fitting given the setting of the paper.\n", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "9"}, "extra_text": {}}, {"review_id": "P2lz9CpQoSr", "reviewer": "Reviewer_aXAA", "summary": "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.", "questions": "", "limitations": "", "rating": 6, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Originality: I found the technical contributions presented here to be incremental over prior work. The single neuron convex relaxation is based upon the framework of Tjandraatmadja et al., except that the difference here is that the input x is defined over the neurons in all previous layers and the set describing x is a simplex. Similarly, the efficient solver presented in Section 4.2 appears to be an extension of Xu et. al adapted to the simplex. \n\nQuality: I have questions regarding the proof of Theorem 3.1 presented in the appendix. Why should a convex activation function applied on a convex set produce a convex output as mentioned in Lines 8-9 in the appendix. Further, line 12-13 says that the optimum value of a linear function over the non-convex set S is the same as on its convex hull, I am not sure if that is a true statement in general. \n\nEq. 4(b), of the form y>=\\sigma(w.x+b), why should this always describe a convex region for all convex activations?\n\nIn lines 172-173, it is written that \" 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\",  wouldn't your analysis become unsound?\n\nIn lines 239-240, it says \"For a target label, the image is said to be verified if the lower bound for a label is positive\", so you do not verify that the network is not robust but only that it cannot be classified to a target class?\n\nIn terms of the experiments, can you compare against a state-of-the-art incomplete verifier? e.g., CROWN or DeepPoly?\n\nClarity: The paper motivates the problem well. However, some of the technical details might be inaccessible to a general audience. The authors should consider providing more examples to demonstrate how their method works. Also, the technical delta over the works of Tjandraatmadja et al. and Xu et. al is not clear.\n\nSignificance: Two years ago, a convex barrier was proposed which exposed the limitations of existing convex relaxations. Since then, a number of methods have been developed that provide more precise convex relaxations than the convex barrier while maintaining scalability. This work explores the same direction. The experimental results demonstrate that the proposed relaxations are effective. The global robustness property considered here can serve as a good benchmark for comparing verifiers.\n\nAdditional question:\n1. Can your framework be used for computing multi-neuron relaxations as in [1]?\n\nOverall, given the concerns above I think the paper is below the bar of acceptance, but I will be happy to increase my grades if the authors can address my concerns.\n \n\nReferences:\n1. Beyond the Single Neuron Convex Barrier for Neural Network Certification. NeurIPS 2019.\n\n===============\nPost rebuttal: The authors addressed my concerns regarding the correctness of the theorem and therefore I am happy to raise my score. However, I still find the work to be somewhat incremental over Tjandraatmadja et al. therefore I will not push for acceptance but also not strongly against seeing this paper getting accepted.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "The authors address both adequately.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "6"}, "extra_text": {}}, {"review_id": "Fn_RoasF6bW", "reviewer": "Reviewer_BsvV", "summary": "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. ", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "\nPros:\n* The paper novelly proposes to use simplex input specification for $\\ell_1$ robustness verification, which enables a tighter relaxation and upper bounds for activations.\n* The proposed method leads to better verified accuracy with low computational cost on $\\ell_1$ robustness verification.\n\n\nCons:\n* There lacks a detailed discussion on the convex barrier which is the focus of this paper, and why the proposed method can overcome the barrier. \n* The multi-modal setting (with both image and text as input) does not seem to quite make sense to me. The text can be arbitrarily perturbed, with arbitrary length and substitution words from the vocabulary. If a model should be robust to such perturbation, should it just ignore the information from the text?\n\nMinor comments:\n* Line 296, Jia et al., 2019 was published in 2019 and is probably not a concurrent work, unless there is an earlier preprint of this work. \n\n-----\n\nUpdates after rebuttal\n\nThanks to the authors for the rebuttal! With the rebuttal, I think now I can better understand how the convex barrier is overcome. I think it will be good if the authors can include more detailed discussions on the convex barrier and reason that the proposed method can overcome the barrier into the revision, since currently \"barrier\" does not appear again in the main text since page 2, which makes it difficult to understand. \n\nFor Sec 5.2 on the multi-modal experiments, I still think it seems to be unreasonable to me, because the model can trivially become robust to such perturbations by totally ignoring the actually useless text. I think it may be better to use a more reasonable setting to demonstrate the benefits of the proposed method. \n\nOverall, I'm currently on the borderline for this paper.\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "They are discussed in the conclusion section.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "5"}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper studies the robustness verification problem for neural networks over simplex inputs. Unlike the Linf case where a tight bound requires exponential complexity, the paper proposes an efficient method to propagate the simplex through ReLU networks where the size of relaxation remains linear in the number of neurons and shows the algorithm can successfully compute tight bounds on several benchmarking datasets. After discussions, the reviewers think that although the method is an extension of (Tjandraatmadja et al.), the derived closed-form expression is new and it is interesting to see that such a nice form can be obtained in the L1 case. Therefore we recommend acceptance of the paper. 

The reviewers also think the paper is not well written and hope the authors improve the presentation of the paper based on the review comments. 

Decision: Accept (Poster)