Venue: NeurIPS 2021 Conference

Reviews:

final_score: rating: 7: Good paper, accept
review_content: 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.
main_review: Strengths:

1. 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.

2. 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.

3. 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.


Improvements that can be made:

1. 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.

2. 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).

3. 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.

4. 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.

Minor questions:

1. 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?

Overall, 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.

References:

[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.


limitations_and_societal_impact: No potential negative societal impact.
review_title: null

final_score: rating: 6: Marginally above the acceptance threshold
review_content: 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.
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. 

Quality: 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. 

Eq. 4(b), of the form y>=\sigma(w.x+b), why should this always describe a convex region for all convex activations?

In 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?

In 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?

In terms of the experiments, can you compare against a state-of-the-art incomplete verifier? e.g., CROWN or DeepPoly?

Clarity: 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.

Significance: 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.

Additional question:
1. Can your framework be used for computing multi-neuron relaxations as in [1]?

Overall, 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.
 

References:
1. Beyond the Single Neuron Convex Barrier for Neural Network Certification. NeurIPS 2019.

===============
Post 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.
limitations_and_societal_impact: The authors address both adequately.
review_title: null

final_score: rating: 6: Marginally above the acceptance threshold
review_content: 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. 
main_review: 
Pros:
* The paper novelly proposes to use simplex input specification for $\ell_1$ robustness verification, which enables a tighter relaxation and upper bounds for activations.
* The proposed method leads to better verified accuracy with low computational cost on $\ell_1$ robustness verification.


Cons:
* 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. 
* 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?

Minor comments:
* 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. 

-----

Updates after rebuttal

Thanks 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. 

For 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. 

Overall, I'm currently on the borderline for this paper.

limitations_and_societal_impact: They are discussed in the conclusion section.
review_title: null

final_score: rating: 6: Marginally above the acceptance threshold
review_content: 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).

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.

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.
However, 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}$).

The work seems well connected with related works (with the notable exception of [1], which describes a similar algorithm to [Zhang et al. 2018b]*)

Questions:
- 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?
- 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.)
- 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?
- Am I correct in assuming that Gurobi Simplex in Section 5 utilizes the relaxation presented in 3.2?

Minor:
- L117, bad line break before the fullstop.
- L125 should likely be $\mathbf{x}_{k}, k \in [n-1]$.
- Figure 4 should be a Table.

*Citations in the [Name, Year] format refer to citations in the paper, while [Number] citations refer to:

[1] An Abstract Domain for Certifying Neural Networks, Singh et al., POPL'19

[2] Fast and Precise Certification of Transformers, Bonaert et al., PLDI'21

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.
review_title: null

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)