Venue: NeurIPS 2021 Conference

Reviews:

final_score: rating: 7: Good paper, accept
review_content: summary: This paper proposes a mixed-integer programming formulation for trained ReLU neural networks, which will enable people to solve many related problems like optimal adversary, verification and minimally distorted adversary. The main advantage of this formulation comes from partitioning node inputs into a number of groups and use the disjunctive programming to form the convex hull. By selecting different partition size, one can recover the convex hull or the big-M formulation. For the purpose of balancing model size and tightness of the formulation, numerical experiments suggest that moderate size of partitions performs the best. 
main_review: This paper is nicely written, the studied problem is interesting, and experiments are extensive and convincing. However, I do have a few comments, concerns and questions outlined as follows.

1. Many details and closely related results/reports are contained in the appendix. I think this paper might be a better fit for the full-length journal paper. (This would also give the authors more space for clarifications.)  
2. The main novelty of this paper comes from transforming the original big-M formulation into disjunctive formulation, and then introduce new variables to partition the summation terms, which will allow us to obtain a more refined upper/lower bounds. To that regard, I think the novelty is not fundamental.
3. The format for the formulations in this paper (including the appendix) should be properly adjusted and aligned. 
4. Line 89, page 3: "$\sum_{n}z_n, n=1, \ldots, N$" should be "$\sum_{n=1}^N z_n$".
5. $z_n = \sum_{S_n} w_i x_i$ should be $z_n = \sum_{i \in S_n} w_i x_i$ across the paper.
6. Second disjunction in equation (12): "$y \leq 0$" should be "$y \geq 0$".
7. Equation (18), (19): I think (18) should be $\sum_i \min(A, B) + b$, and (19) should be $\sum_i \max(C, D) + b$, where $A,B,C,D$ are those terms inside the brackets. 
8. Line 147: what are (??)?
9. For those convex hull based cuts, in order to add them, how do you solve the corresponding separation problem?
10. Equation (52) in Appendix: here the subscript should be $I'_j$. Also, what is the reason for listing inequality (50) and (52) here?
11. Inequalities (65), (66) in Appendix: you should mention what are these constraints (65), (66) when $w_n=0$.

limitations_and_societal_impact: Yes, the authors mentioned the problem of the poor selection of hyperparameter, and formulation sometimes does not integrate well with default cuts.
review_title: null

final_score: rating: 7: Good paper, accept
review_content: summary: This work proposes a novel MILP formulation of ReLU networks that can control the size of the considered problem in a trade-off against the tightness of the relaxation. Theoretical analysis is provided along with experiments.
main_review: The problem seems well motivated and while I am not familiar with the recent advances in MILP formulation of DNs the paper is well written, well motivated, and well explained. Additionally the experimental details are clear enough to allow reproduction.

Many ablation studies are provided to see at which point in this trade-off one is able to obtain best computation times and comparison with recent work seems thorough.

I did not find English issues.
limitations_and_societal_impact: Yes
review_title: null

final_score: rating: 7: Good paper, accept
review_content: summary: The paper introduces a class of novel mixed-integer programming formulations for optimizing the output of a trained ReLU network. Its approach is to model a ReLU as a disjunction where the preactivation function is partitioned in its indices. This results a parameterized formulation that can range from the traditional big-M formulation to an ideal formulation at its extremes. Since the former is weak but light and the latter is strong but large, this allows us to find a trade-off where the formulation is both reasonably strong and not too large so that its performance is better than either extreme. Moreover, the paper presents an optimization-based bounds tightening approach that can be applied to these formulation. The authors show that this formulation has good computational performance compared to its extremes for three classes of problems in the area of neural network verification.
main_review: This paper offers a solid and novel contribution to the area of MIP formulations for trained neural networks. These problems are particularly relevant in the area of neural network verification, but they also appear when neural networks are used as surrogate models for optimization. The paper is overall well-written, cites relevant work, and easy to understand for a reader with the relevant MIP and disjunctive programming background (although it is not clear to me if this is an easy read for someone without this background).

There are two main methodological contributions here that are related but could be viewed as orthogonal: the development of a partition-based formulation for ReLUs by disaggregating disjunctions (along with partition heuristics), and the use of optimization-based bound tightening within ReLU formulations. Both ideas are very interesting and contribute to a practical advancement. In particular, it is known that OBBT bounds for the big-M values make a large difference in practice (e.g. [30] from paper, and this is also confirmed again in this paper in Figure 3), so it stands to reason that incorporating OBBT bounds into other inequalities of the ReLU results in computationally stronger results.

The computational setup appears sound to me and sufficiently detailed for publication. Three classes of problems are investigated, although they are very similar to each other. A comparison is made with both traditional big-M formulations used in various works, and with the closest related work (Anderson et al., [3] in the paper). The method proposed does appear to produce a significant improvement over big-M, and a slight improvement over an implementation of the cuts from Anderson et al. with optimally tuned cut frequency. Note that if it matched that work, the results would still be valuable because this implementation is simpler, and tuning the number of partitions would be easier than tuning the cut frequency in Anderson et al.

I recommend this paper for acceptance, but I propose a few minor corrections (particularly regarding mathematical formalization) and suggestions below.

Mathematical formalization issues:

1. The statements that (6)-(11) models (5), and (13)-(17) models (12) are not mathematically precise. Note that (5) (= (12)) models a disjunction of two unbounded sets, whereas the formulations model a disjunction of two bounded sets. What the formulations model are a bounded version of (5) and (12). In (12), the bounds are in the z variables and they can be different bounds for each side of the disjunction because they may depend on previous layers of the neural network, and one can take the disjunction into account to tighten them, which is what is done in Section 3.1. Some explanation along these lines should be added. I do like that (5) and (12) are cleanly stated and it is easier to understand without having to worry about bounds, so I would suggest clarifying and formalizing this right after they are defined, but independently of how you present it, this should be made mathematically precise.

2. Similarly to above, Proposition 3 requires bounding conditions for correctness, since (1) assumes that $x \in \mathbb{R}^\eta$ (and thus the convex hull of (1) would simply be the epigraph of the function and not the formulation in the paper).

3. The proof of Proposition 4 is slightly incomplete: it argues that it is strictly tighter because the constraints in (20) are facet-defining, but misses the possibility that two constraints are the same. However, it is easy to see that they are distinct because the support of all constraints are different. Adding "and distinct from each other" after facet-defining should be sufficient to fix this, since this is easy to see.

4. Line 86-87 states "these formulations are tighter than (6)-(11)". Does this mean (2)-(4), or do you mean they are tighter given the OBBT method (see note above about formalizing the disjunction)? This should be clarified. Bounds aside, they represent the exact same disjunction so there is no reason for them to be tighter than (6)-(11). Also, to be precise, you should say that the linear relaxations of these formulations are tighter.


Suggestions for improving connections to previous work:

5. In Proposition 1, I believe it is interesting to point out that the set of inequalities (20) is a particular subset of the inequalities (28a) in Proposition 12 in Anderson et al. where $UB_i$ and $LB_i$ would be given by interval arithmetic. This is completely expected given that we should recover the ideal formulation with $N = \eta$, but clarifying the exact connection between the two works is helpful for the reader to understand how this fits into the framework of Anderson et al. The strength of the partition-based method can be interpreted as preselecting a special subset of inequalities from the ideal formulation in Anderson et al. (although in this paper the lifted formulation is used).

6. Implicit in Proposition 1 is that OBBT can be applied directly to the cuts from Anderson et al. It would be nice to point this out explicitly; I even think that this counts as a contribution. In addition, I would be curious to know if you tried doing this. You can use the original separation method and then strengthen the cut with OBBT (it may no longer be the most violated cut, but that is fine). I do not think that this would be particularly necessary for the NeurIPS publication, but if you have some spare time to include this experiment (probably in the appendix), it would be a very nice improvement to your contribution to the community.

7. A work that may be relevant to cite is: Tjandraatmadja, C., Anderson, R., Huchette, J., Ma, W., Patel, K. and Vielma, J.P., "The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification", since this work describes the convex hull of a ReLU for a box input without binary variables.


Writing issues and other notes:

8. Line 76 states "Note that the second equation is not necessary to model y". Can you clarify in the paper what this second equation refers to? I am confused because all four equalities and inequalities in (5) are needed to model y as a disjunction. Or do you mean (3)?

9. Line 79: $LB^a$, $UB^a$, $LB^b$, and $UB^b$ are not defined.

10. In (12), should $y \leq 0$ be $y \geq 0$?

11. Line 147 has a broken reference.

12. Line 147: Could you explicitly mention that the experiments in Section 4 are done with respect to the lifted formulation? In my first read, I incorrectly interpreted that the projected formulation is used for the computational results. I think the Appendix A.5 results are a minor contribution that could be highlighted a bit more in the main text, since the opposite is true for the full extended formulation given the large number of variables.

13. Line 186: Is this sentence "The partitions ... constraints:" meant to be here?

14. Line 277: Typo: "verfication".

15. I have some difficulty fully understanding the left plot in Figure 2 and it could use some more contextualization. Could you define what "cut frequency" is? Does a frequency of k means that cuts are generated every 1/k nodes? What is the baseline (i.e. no cuts, your version), and does a low cut frequency mean that cuts are still generated at the root? How many rounds of cuts are applied per node? Could you also clarify in the text that the setup is that you start with your partition-based formulation and apply cuts?

16. Could you clarify that Figure 2 is without OBBT, if that is the case?

17. In Figure 3, why is it that N = 1 shows different values for non-OBBT? Is this just MIP solver variability?
limitations_and_societal_impact: This is not discussed but also not particularly relevant for this work.
review_title: null

final_score: rating: 7: Good paper, accept
review_content: summary: This paper presents a family of mixed-integer optimization formulations for trained neural networks (or, rather, individual neurons in the network), with primary application to verification and adversarial analysis/training. The family traces out a spectrum between a small, weak formulation (the big-M) and a larger, stronger formulation (the "convex hull"). The family is parameterized by a partition of the multivariate input to a single ReLU neuron. A handful of strategies for doing this partition are presented, along with computational experiments.
main_review: The main originality of the paper is the way in which existing formulation techniques can be combined to produce a family of approaches which attempt to balance between two important computational considerations. As such, there is not a ton of novelty, but the insight is a worthy contribution to the literature.

The paper is reasonably clear to the reader familiar with mixed integer optimization, though I do think that the presentation could be improved (suggestions to follow).

The computational results suggest that the contributions of the paper have merit and are a solid contribution to the verification literature. I do wish the authors left us with a clearer story on how N should be selected (either theoretically or practically, or both), but that may be too much to ask for a single conference paper.

Other comments:
* L14: The acronym "NN" is used without definition.
* L76: What is the "second equation" being referred to?
* L130: The description of the indexing of (20) is confusing. Should I understand that: you consider each nonempty subset of elements of {S_1,...,S_N}, assign it an integer index j, and then construct I_j as the union over all selected elements?
* Proposition 1 looks strikingly similar to the ideal formulation of Anderson et al. In particular, if we take each S_i = {i}, are they not the same, modulo how the LBs and UBs are computed? This connection should be made explicit.
* L147: Broken references
* The typesetting for (22), and similar blocks below, are very confusing. They read like a disjunction, with the "or", but the text uses them in a very different way. Consider other ways to typeset this discussion.
* The discussion of partitioning strategies is brief, with no real attempt at a theoretical justification for the chosen approaches. However, I don't find this a major deficiency. I do wish that the discussion, particularly for the "equal-range partitions", was written more clearly; it is sufficiently hard to parse that I do not believe that I could recreate the authors approach solely from the description in the text.
* Is the time reported in the tables accounting for the time spent on OBBT, or solely for the MIP?
* How does the performance look for the new approaches _without_ OBBT? Put another way: how strongly dependent are the positive computational results on OBBT?
* The values for epsilon reported (5 in Tables 2 and 3) seem quite high. Are the inputs normalized? Does it vary for the differing input sizes of MNIST and CIFAR10?
* Figure 3: Please do not mix two charts with differing y-axes into one! It is very confusing and/or misleading to the reader.
* In the computational results: Is the "average" arithmetic of geometric mean? How do time outs factor into the average time columns? This is a situation where time limits can introduce weird artifacts. For example, method 1 might be very fast on half of the instances and completely unsolvable on the remaining, while method 2 is consistently solvable within the time limit, but slow. Depending on how the time limit is set, the average time of method 1 (computed with time outs included) can be made arbitrarily large.


limitations_and_societal_impact: No concerns.
review_title: null

Meta-review: In this paper, the authors introduce novel mixed-integer programming formulations to optimize the output of a trained ReLU network. This is an important problem that arises, e.g., in verifying robustness of deep neural networks and adversarial training. The approach is based on partitioning node inputs into a number of groups and forming the convex hull over the partitions via disjunctive programming. In particular, this approach recovers the convex hull and Big-M formulations by choosing different partition sizes. The authors show that the proposed formulation provides computational advantages with respect to the baselines in neural network verification. The reviews all agreed that the paper introduces an interesting and effective strategy, only expressed minor concerns and suggestions, and recommended acceptance. Please take into account the updated reviews when preparing the final version to accommodate the requested changes. Thank you for your submission to NeurIPS.
Decision: Accept (Poster)