Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 5: Marginally below acceptance threshold
review_content: This paper describes a dual solver for neural network verification. In particular, the authors consider a linear relaxation of neural networks with relu activations and develop an active set based method. Numerical comparisons show that the proposed method provides speed-ups in verifying deep networks.

Although the authors present promising empirical results, a precise and rigorous analysis and of the active set strategy is lacking.  It would be great if the authors can clarify several points raised below.


1. Does the active set approach provide any guarantees on the tightness of the solution? It looks like exponentially many optimization variables in eq 6 are initialized at zero, which provides a lower-bound on eq 2. However, it's not clear if the produced lower-bounds are effective.

2. Does the greedy active set extension strategy converge to an optimal solution of the relaxation? Is the algorithm sensitive to the selection criterion and frequency?

3. The authors employ projected gradient with Adam to maximize the dual function d(\alpha,\beta). Does this approach provably converge to the solution of eq 9? It would be nice to describe the performance of other optimizers, e.g., plain SGD.

4. In eq (1a), is \hat x_n a scalar? It would be better to specify that n_n=1.

5. It looks like the integer constraints z\in \{0,1\} are missing in eq 2? 

6. Last paragraph on page 2, by an optimal solution of the problem 2 are you referring to the linear relaxation?
review_title: This paper describes a dual solver for neural network verification. Although the authors present promising empirical results, a precise and rigorous analysis and of the active set strategy is lacking. 

final_score: rating: 8: Top 50% of accepted papers, clear accept
review_content: This paper presents an algorithm for verification of neural networks with ReLU activations. Essentially, it takes the tightened ReLU relaxation of (Anderson et al. 2020), builds its Lagrangian dual, and then applies a column generation scheme to accommodate the explosion of decision variables. The authors present computational results showing that, due to the amenability of the methods to GPU accelaration, they can produce stronger verification bounds than comparable methods working with weaker relaxations in a modest amount more time. Moreover, they show that the method can be successfully embedded in a branch-and-bound-like framework for exact verification.

I like the paper and think it makes a good contribution to the literature. The paper builds heavily on (Anderson 2020), but the algorithm approach is very different and the authors clearly had to do some work (e.g. rederiving the dual to ensure efficient inner problem solves, making convolutions+masking work on the GPU) to make everything work out. The computational results also seem compelling, though I have some potential concerns about the comparison being made.

My main concern is the use of "Gurobi 1 cut" as the baseline for comparison. Given that there is a one-to-one mapping between cuts in the primal formulation (Gurobi 1 cut) and variables in the dual formulation (the new approach), I am curious why the authors did not choose symmetric generation schemes for the two. Would the solve times be significantly lower if only one cut per layer is added (as in ActiveSet), instead of one per neuron? If so, what benefit do multiple iterations of cut generation offer? Is LP incrementalism or warm-starting used, or is the second LP solved from scratch? Even with these changes, I would imagine that the ActiveSet method still runs (much?) faster than the primal approach, but it's quite possible that the bound improvement would shrink.

Minor comments:
* p1: The phrasing "The main bottleneck of the above approach" is ambigious (which approach?). If the approach includes (ii), then the bottleneck will be the enumeration tree, not the convex subproblems.
* p2: The "which is linearly-sized" reads like it applies to the optimal solution of (2), not the formulation (2) itself.
* p18: I think there are some extra primes in the text of Appendix F.2.
review_title: Review for "Scaling the convex barrier with active sets"

final_score: rating: 7: Good paper, accept
review_content: The authors present a custom solver for verifying properties of neural networks (such as robustness properties). Prior work for neural network verification relies on generating bounds by solving convex relaxations ("convex barrier"). The authors describe a sparse dual solver for a new relaxation which is tighter (but has higher computational complexity). The solver is represented (for the most part) as standard operations built into pytorch, and so it can be easily run on GPUs (they do require a specialized operator to support masked forward/backward passes, and they describe how this is done efficiently for convolutional networks). The solver involves repeatedly solving modified instances of a problem, where only a small active set of dual variables (instead of exponentially many) is considered at each step.

Experimental results are promising in that it outperforms generic solvers in terms of both the bounds achieved and the time taken to do so. This does seem to be a promising approach.


review_title: Review for "Scaling the Convex Barrier with Active Sets"

final_score: rating: 7: Good paper, accept
review_content: The paper proposes a dual approach for solving the exponentially-sized linear programs that arise from the relaxation of the single ReLUs by Anderson et al. (2020). The algorithm is demonstrably faster than existing methods in experiments resembling those from Bunel et al. (2020). The idea of applying a dual active set method is arguably quite straightforward from an optimization perspective. What makes the contribution in this paper strong is 

(1) A good implementation in multiple ways. The performance of active set methods highly depends on the how the sets are maintained (section 3.2). Also, making the algorithm run efficiently in practice requires taking advantage of GPUs and the neural network structure (section 3.3, G). I believe that without doing these well, it is likely that such an approach would be significantly slower than existing methods. I look forward to seeing the authors code released.

(2) Providing the proper context for the work -- The paper builds upon prior contributions from Anderson et al. and other works that study the dual aspect of the problem. The authors do a good job explaining how their work fits in and how it compares to other approaches. This both provides a nice theoretical grounding for this work and is also useful pedagogically.

(3) Detailed experiments on reasonably sized neural networks and providing hyperparameters.

Two things I would like the authors to address:

(1) Experimental results - CPU-only

How does an all CPU version of the algorithm compare to Gurobi? This would be a better apples-to-apples comparison since commercial solvers do not make use GPUs. I would understand if a CPU-only implementation is slower since Gurobi is highly-tuned.

(2) Comparison with Tjandraatmadja et al. (2020)

I would like the authors to contrast their approach more against the the one by Tjandraatmadja et al. The formulations used there are different (and the focus of that paper is different), they do describe a cutting plane approach, which in a sense can be viewed as an approach that incrementally increases the number of dual variables. The authors can either do so here in the response, or if they think it would benefit the paper add it in.

-------------------------
Update after author response:
Thanks to the authors for addressing my questions!
review_title: A solid contribution to the neural network verification literature

final_score: rating: 6: Marginally above acceptance threshold
review_content: 1) Summary
The manuscript proposes an optimisation scheme to compute bounds on the output of piecewise linear feedforward networks. Improving upon the planet relaxation, the authors provide a tighter relaxation scheme with exponentially man constraints that they tackle by a dual solver using active sets. Some experiments are conducted in order to benchmark the relaxation with others.

2) Strengths
+ The paper is mostly well written.
+ The evaluation seems pretty exhaustive as it comes to competing optimisation schemes.

3) Concerns
- The practical utility for deriving a proper bound for a relevant architecture is still limited.
- It does not seem that the paper makes code and data available to the public.

4) Remarks/Questions
  a) Section 2: The optimization problem in Equation (1) needs to be sharpened. On the one hand, $x^hat_n$ needs to be a scalar quantity in order to have a meaningful objective and on the other hand, the only free variable is $x_0$ as all the other variables depend on it. The first part also applies to Equations (2) and (3). Also, the solution is not necessarily unique in the ReLu case if many neurons are silent.
  b) References: capitalization not correct e.g. "smt"
  c) Please provide a more concise statement what you require from the oracle. Do you require that $min_{x in C} a'*x$ can be computed in $O(1)$?
  d) What restricts the approach to piecewise linear functions?
review_title: Tighter optimisation schem for piecewise linear network verification

final_score: rating: 6: Marginally above acceptance threshold
review_content: The paper focuses on the notion of dual solvers, which are solvers that have the ability to prove as well as disprove that a specified property of neural networks holds over all inputs in a specified domain. Unsurprisingly, the bottle neck for this approach is the computation of lower bounds, which can be translated into a non-linear (and NP-hard) optimization problem. Dual solvers typically instead attempt to solve a linear formulation of the problem, and recently Anderson et al. introduced a new MIP formulation for the problem which is more accurate than previously used formulations at the cost of potentially requiring a significantly larger number of constraints.

In this work, the authors introduce a dual solver called "Active Set" that is designed to solve Anderson's tighter formulation, with the aim of achieving increased accuracy while keeping the computational costs low. The solver seems correct, even though I couldn't verify the details; generally speaking, it operates by starting with the easier but less accurate formulation that is classically used, and making it more precise by the gradual introduction of (an "active set" of) variables from a modified version of Anderson et al's more accurate formulation. Experimental evaluations show that the new solver can be used both for incomplete verification and complete verification; in both cases, it is possible to use Active Set to obtain an implementation that can either achieve higher accuracy (for incomplete verification) or avoid a timeout for a greater percentage of instances (for complete verification). 

The paper is well written. The preliminaries and writeup in general are clearly aimed at experts with some background knowledge in the given area (which prevented me from verifying the technical details), but I believe that it fits well within the scope of ICLR. The main contribution is the design of a new solver and its experimental evaluation; the theoretical contribution is negligible. It is also easy to imagine that there could be many alternate ways one could use Anderson et al.'s recent formulation to improve the state of the art - in that sense, the results achieved by the authors are not surprising. But that does not mean that there were no challenges left to overcome, and the experimental evaluations seem to be reasonable. So I think that the paper's contribution is sufficient to warrant a presentation at ICLR.

Question:
-Are there other "standard" datasets that could be considered instead of CIFAR-10, and would it be difficult to also use these for experimental evaluations?

Minor remarks:
-page 2: "if more compute budget is..."  should be "if a larger computational budget is..."

Post-rebuttal comment:
I acknowledge having read the authors' response and I have also glanced over the updated version of the paper.
review_title: A new solver employing a recently introduced formulation

Meta-review: Dear authors,

as you have noticed this paper was not easy to review. I have hence invited 2 additional reviewers which I strongly respect and are very knowledgeable. After carefully reading the paper myself, I have to agree with one of the reviewers who said "... it [your paper] makes a good contribution to the literature ....". To be honest, we were working in my group on a very similar approach but did not manage to finish it (and I know how hard it is).

To conclude, when preparing to the final version, please try to go over the reviews, I am sure they can make your paper even stronger :) 

Decision: Accept (Poster)