Partition-Based Formulations for Mixed-Integer Optimization of Trained ReLU Neural Networks
Authors: Calvin Tsay
Jan Kronqvist
Alexander Thebelt
Ruth Misener
Venue: NeurIPS 2021 Poster (2021)
Keywords: Mixed-integer programming
Deep learning
Rectified linear activation

Abstract: This paper introduces a class of mixed-integer formulations for trained ReLU neural networks. The approach balances model size and tightness by partitioning node inputs into a number of groups and forming the convex hull over the partitions via disjunctive programming. At one extreme, one partition per input recovers the convex hull of a node, i.e., the tightest possible formulation for each node. For fewer partitions, we develop smaller relaxations that approximate the convex hull, and show that they outperform existing formulations. Specifically, we propose strategies for partitioning variables based on theoretical motivations and validate these strategies using extensive computational experiments. Furthermore, the proposed scheme complements known algorithmic approaches, e.g., optimization-based bound tightening captures dependencies within a partition.

Partition-Based Formulations for Mixed-Integer Optimization of Trained ReLU Neural Networks
Calvin Tsay Department of Computing Imperial College London tttssyiimmeiiie aa..raalll....... ac uk
Jan Kronqvist
Department of Mathematics
KTH Royal Institute of Technology jankr@kth.se se
Alexander Thebelt Department of Computing Imperial College London alexander. thebelt 1hebelt1801mppriall ac. uk
Ruth Misener
Department of Computing
Imperial College London
r mi meiseerimmmerial ac. uk
Abstract
This paper introduces a class of mixed-integer formulations for trained ReL.U neural networks. The approach balances model size and tightness by partitioning node imputs into number of groups and forming the convex hull over the partitions via disjunctive programming. At one extreme, one partition per input recovers the convex hull of node, i.e., the tightest possible formulation for each node. For fewer partitions, we develop smaller relaxations that approximate the convex hull, and show that they outperform existing formulations. Specifically, we propose strategies for partitioning variables based on theoretical motivations and validate these strategies using extensive computational experiments. Furthermore, the proposed scheme complements known algorithmic approaches, e.g.. optimization- based bound tightening captures dependencies within partition.
Introduction
Many applications use mixed-integer linear programming (MILP) to optimize over trained feed- forward ReLU neural networks (NNs) [5]
14 [8|
23
32 36). MILP encoding of ReLU-NN
enables network properties to be rigorously analyzed, e.g., maximizing neural acquisition function
33 or verifying robustness of output (often classification) within restricted input domain 6 MILP encodings of ReLU-NNS have also been used to determine robust perturbation bounds ( compress NNs (28), count linear regions [27). and find adversarial examples (17). The so-called big-
M formulation is the main approach for encoding NNs as MILPs in the above references. Optimizing the resulting MILPs remains challenging for large networks, even with Maate-of-the-art software.
Effectively solving a MILP hinges on the strength of its continuous relaxation 10 weak relaxations render MILPs computationally intractable. For NNs, Anderson et al. 3 showed that the big-M formulation is not tight and presented formulations for the convex hull (i.e., the tightest possible formulation) of individual nodes. However, these formulations require either an exponential (w.r.t inputs) number of constraints or many additional/auxiilary variables. So, despite its weaker continuous relaxation, the big-M formulation be computationally advantageous owing its smaller size.
Given these challenges, we present a novel class of MILP formulations for ReLU-NNs. The formulations hicrarchical: their relaxations start big-M equivalent and converge to the convex hull. Intermediate formulations can closely approximate the convex hull with many fewer variables/coostraints. The formulations constructed by viewing each ReLU node two-part
35th Conference on Neural Information Processing Systems (NcurIPS 2021).

---

disjunction. Kronqvist et al. [2] proposed hierarchical relaxations for general disjunctive programs. This work develops similar hierarchy to construct strong and efficient MILP formulations specific to ReIJUNNNs. In particular, we partition the inputs of each node into groups and formulate the convex hull over the resulting groups. With fewer groups than inputs, this approach results in MILPs that are smaller than convex-hull formulations, yet have stronger relaxations than big-M.
Three optimization tasks evaluate the new formulations: optimal adversarial examples, robust verification, and l mmminimallly distorted adversaries. Extensive computation, including with convex- hull-based cuts, shows that our formulations outperform the standard big-M approach with 25% more problems solved within a Ih time limit (average 2.2X speedups for solved problems).
Related work. Techniques for obtaining strong relaxations of ReLU-NNs include linear program-
Lagrangian decomposition (7), combined al. [31] derived the tightest possible convex relaxation for a single ReL.U node by considering its multivariate input space. These relaxation techniques do not exactly represent ReLU-NNs, but rather derive valid bounds for the network in general. These techniques might fail to verify some properties, due to their non-exactness, but they can be much faster than MILP-based techniques. Strong MILP encoding of ReLU-NNs was also studied by Anderson et al. [3, and related dual algorithm was later presented by De Palma al. [33. Our approach is fundamentallyy different, as constructs computationally cheaper formulations that approximate the convex hull, and we start by deriving a stronger relaxation instead of strengthening the relaxation via cutting planes. Furthermore, our formulation enables input node dependencies to easily be incorporated.
ming 16
34 35
semidefinite programming 12 25
relaxations 30 and relaxations multiple nodes 29 Recently, Tjandraatmadja
Contributions of this paper. We present a new class of strong, yet compact, MILP formulations for feed-forward ReLU-NNs in 3 Section [31 observes how, in conjunction with optimization- based bound tightening, partitioning input variables can efficiently incorporate dependencies into MILP formulations. Section 3.2 builds on the observations of Kronqvist et al. [21] to prove the hierarchical nature of the proposed ReLUUspecific formulations, with relaxations spanning between big-M M and convex-hu formulations. Sections 3.4 show that formulation tightness depends on the specific choice of variable partitions, and we present efficient partitioning strategies based on both theoretical and computational motivations. The advantages of the new formulations are demonstrated via extensive computational experiments in Section 4
2 Background
2.1 Feed-forward Neural Networks
A feed-forward neural network (NN) is directed acyclic graph with nodes structured into l layers. Layer l receives the outputs of nodes in the preceding layer - 1 as its inputs (layer represents inputs to the NN). Each node in a layer computes weighted sum of its inputs (known as the preactivation), and applies an activation function. This work considers the ReLU activation function:
y = max(0. wn + b)
where æ E R and y E [0, oo) are, respectively, the inputs and output of a node (w b termed the preactivation). Parameters w E Io' and b E R are the node weights and bias, respectively.
2.2 ReLU Optimization Formulations
In contrast to the training of NNs (where parameters w and are optimized), optimization over a NN seeks extreme cases for a trained model. Therefore, model parameters (w. b) are fixed, and the inputs/outputs of nodes the network (ær, y) are optimization variables instead.
Big-M Formulation, The ReLU function
is commonly modeled
y 2 (w² T x + 6) y S (w x + 6) (1 0) LB
(2)
(3)
y S O
(4)

---

where [0, oo) is the node output and a E {0, is a binary variable corresponding to the on-off state of the neuron. The formulation requires the bounds (big-M coefficients) LB,, UB E R. which should be as tight as possible, such that (w x + b) E [LB", UB").
Disjunctive Programming
We observe that can be modeled as disjunctive program:
y= ]v w u po"+bbso
(5)
w x
The extended formulation for disjunctive programs introduces auxiliary variables for each disjunction. Instead of directly applying the standard extended formulation, we first define 2 == w x and assume is bounded. The auxiliary variables =" RR and d² E R can then be introduced to model (5):
w a 2z +
(6)
+ ob 00 0
(7)
+ (1-o)b
(8)
y= 24 + +1--a))
(9)
LL 2 S UB"
(10)
(1 (1-6)LB" < S (1 (1-o) UB
(11)
where again y E (0, and a {0, 1). Bounds LB", UB" L.B UB E R are required for this formulation, such that E ooLB" UB"] and 2² E (L-o)LLB*, UB Note that the inequalities in (5) may cause the domains of 2 and 2 to differ. The summation in (6) can be used to eliminate either or zh; therefore, in practice, only one auxiliary variable is introduced by formulation (6) II].
Importance of relaxation strength. MILP is often solved with wranch-and-bounde strategy that bounds the objective function between the best feasible point and its tightest optimal relaxation. The integral search space is explored by "branching" until the gap between bounds falls below given tolerance. A tighter, or stronger, relaxation can reduce this search tree considerably.
Disaggregated Disjunctions: Between Big-M and the Convex Hull
Our proposed formulations split the sum w x into partitions: will show these formulations have tighter continuous relaxations than (6) TT). In particular, we partition the set {l,.... n into
subsets S₁ U S2 U..... ... U SN = {I, .... m Sn ns 0 Vn + n'. An auxiliary variable is then introduced for each partition, i.c., 2n Eies, Wax, Replacing a w x with Σ 2n. the disjunction (5) becomes:
- Σ 2n +
1 v (
v
Σ m y 9
2n +
(12)
Assuming now that each on is bounded, the extended formulation variables of and = for each 2n. Eliminating z via the summation 2n = zu + 2 results in our proposed formulation (complete derivation in appendix A.1):
be expressed using auxiliary
Σ
bb W Zn
+ +ab 50
(13)
VES
2 + (1 o)b 20
(14)
Σ 2 + (1 - a)b
(15)
n
LB
WaT; 2/2 SU..
Vn 1, 1,,., N
(16)
seS
(1 - 1) < Fm < - <1-o)BBB, UB
Vn I...,N N
(17)
where y E [0, oo) and a E (0, We observe that 13
exactly represents the ReLU node (given that the partitions 2n are bounded in the original disjunction): the sum 2n Eies, waz, is
3

---

substituted in the extended convex hull formulation 4 of disjunction (12). Note that, compared to the
general case presented by Kronqvist et al. (2, both sides of disjunction (12) can be modeled using the same partitions, resulting in fewer auxiliary variables. We further note that domains [I.B%, UB. and [LB" n2
U may not be equivalent, owing to inequalities in (12).
3.1 Obtaining and Tightening Bounds
The big-M formulation
2 requires valid bounds (w x + b) [LB", UB%. Given bounds for E Ir F.]. interval arithmetic gives valid bounds:
each input variable, T2
LB
(r, wy) + 3,min(O, w,)) + b
(18)
UB Σ (f,max(0, wx) + min(( ws)) + b
(19)
But (18)-19) do not provide the tightest valid bounds in general, as dependencies between the input nodes are ignored. Propagating the resulting over-approximated bounds from layer to layer leads to increasingly large over-approximaaions, i.e., propagating weak bounds through layers results in a significantly weakened model. These bounds remain in the proposed formulation (3 17 in the form of bounds on both the output y and the original variables æ (i.c., outputs of the previous layer).
[9)
05
65
65
83
F3
F3
20
83
13
Figure I: Hierarchical relaxations from N = 1 (equiv. big-M) to N = 20 (convex hull of each node over box domain) for two-input (x)) NN trained on scaled Ackley function, with output fxx) Top row: 2 bounds obtained using interval arithmetic; Bottom row: 2 bounds obtained by optimization-bant based bound tightening. The partitions are formed using the equal size strategy.
Optimization-Basee Bound Tightening (OBBT) or progressive bounds tightening [32), tightens variable bounds and constraints [13]. For example, solving the optimization problem with the objective set to minimize/maximize (w x + b) gives bounds: min( (w" x + b) I w x + b < max(w" x + b). To simplify these problems, OBBT can be performed using the relaxed model (i.e.. E J0. 1] rather than a E {0. 1)), resulting in a linear program (LP). In contrast to (18) (9). bounds from OBBT incorporate variable dependencies. We apply OBBT by solving one LP per bound.
The partitioned formulation (3 17 requires bounds such that = E [LB. UB%] 2 E (1 I)LB
n2 UB*]]. In other words, LLB UB*] is a valid domain for 2 when the node is inactive
(a = 1) and vice versa. These bounds can also be obtained via OBBT: min(E W;2x)) S 2 <
max w;xr);; w x + b < O. The constraint on the right-hand side of disjunction 12 can
be similarly enforced in OBBT problems for 2 In our framework, OBBT additionally captures dependencies within each partition Sn, Specifically, we observe that the partitioned OBBT problems effectively form the convex hull over a given polyhedron of the input variables, in contrast to the convex hull formulation, which only considers the box domain defined by the min/max of each input node B Since Eies, W,Y, 2, + 2 and 24 0, the bounds Imin tes., wyz,),
max maxxE, w.:::]] are valid for both = and 2b These bounds can from 18 19 or by solving two OBBT problems for each partition (2N LPs total). This simplification uses equivalent bounds for
Fn and 2/, but tighter bounds can potentially be found by performing OBBT for 2 and 2 separately
(4N LPs total).

---

Figure I compares the proposed formulation with bounds from interval arithmetic (top row) vs OBBT (bottom row). The true model outputs (blue), and minimum (orange) and maximum (green) outputs of the relaxed model are shown over the input domain. The NNs comprise two inputs, three hidden layers with 20 nodes each, and one output. As expected, OBBT greatly improves relaxation tightness.
3.2 Tightness of the Proposed Formulation
Proposition 1.
13
has the equivalent non-lifted (i.e., without auxiliary (eriiales))
wiat + +lbb +
Σ
UB:)
LB(), + (a 1) KEZ,
Vj = -1,.., 2
(20)
VEI
2 w" b
(21)
5 UB
(22)
where UB; and LB; denote the upper and lower bounds of weys. The set I denotes the inpul indices {1.... ?}, and the subset I denotes the indices contained by the union of the j-th combination of partitions in Sy.
Proof. Formulation
introduces N auxiliary variables =/, which can be projected out using Fourier-Motzkin elimination (appendix A.2), resulting in combinations IJ, 2
Remark. When N < 7, the family of constraints in 20 represent subset the inequalities used to define the convex hull by Anderson et al. (33, where UB and LB; would obtained using interval arithmetic. Therefore, though lifted formulation is proposed in this work, the proposed formulations have non-lifted relaxations equivalent to pre-selecting a subset of the convex hull inequalities.
Proposition 2. Formulation
13
is equivalent to the big-M M formulation
when N 1.
Proof. When Conversely, big-M can be seen the convex hull over single aggregated En Zn 21 "variable," w² x.
follows that & = (1,... n). Therefore, 21
Ei= Wer w x and
Proposition 3. Formulation 13 bounded, for the case of N
represents the convex hull of given the inputs a
Proof. When N = 7/ it follows that S, = [n]: Vn = 1,.., and, consequently. 2n = wn Since Zn are linear transformations of each zn. (as are their respective bounds), forming the convex hull over recovers the convex hull over æ. An extended proof is provided in appendix A.3.
Proposition 4. A formulation with N partitions is strictly tighter than any formulation with (N 1) partitions that is derived by combining two partitions in the former.
Proof. When combining two partitions, i.e., S == S USN, constraints in (20) where S/y S
I, are also obtained by - Sy} S Iz. In contrast, those obtained by N VSN S I, cannot be modeled by S N Since each constraint in (20) is facet-defining 3 and distinct from each other, omissions result in a less tight formulation.
The convex hull can be formulated with 1j auxiliary variables using 13 or 2n constraints using (20.. While these formulations have tighter relaxations, they perform subproblems. Our proposed
Remark.
for N =
worse than big-M due to having more difficult branch-and-bour formulation balances this tradeoff by introducing hierarchy of relaxations with increasing tightness and size. The convex hull is created over partitions Zn, n. = =1,.., N. rather than the input variables In, 1,....J. Therefore, only N auxiliary variables are introduced, with N S n. The results in this work are obtained using this lifted formulation (13) (1);; Appendix A.5 compares the computational performance of equivalent non- non-lifted formulations, i.e. involving N constraints.
Figure I shows a hierarchy of increasingly tight formulations from N = (equiv. big-M) to N = 20 (convex hull of each node over a box input domain). The intermediate formulations approximate the convex-hull (N 20) formulation well, but need fewer auxiliary variables/constraint..
5

---

3.3 Effect of Input Partitioning Choice
Formulation 13 creates the convex hull over 2n Eieg Wiz,, n I...,NN. The hyperpa- rameter N dictates model size, and the choice of subsets, $1, .... Sy, can strongly impact the strength of its relaxation. By Proposition 4, (I3) (I7) can fact give multiple hierarchies of formulations. While all hierarchies eventually converge to the convex hull, we are primarily interested in those with tight relaxations for small N.
Bounds and Bounds Tightening, Bounds on the partitions play a key role in the proposed for- mulation. For example, consider when a node inactive: bounds o LL I Lies, w;Z; S oU... Intuitively, the proposed formulation represents the convex hull over the auxiliary variables, 2n = Exes, W,Z,, and their bounds play key role in model tightness. We hypothesize these bounds are most effective when partitions Sn are selected such that w,z4, vi E Sn, are of similar orders of magnitude. Consider for instance the case of w 1,,, 100) and 2; E [0, 1], = 1, ...., 4. As all weights are positive, interval arithmetic gives 0 S Σ 3,W;; S Σ Wy With two partitions, the choices of $ [1,2] vs S1 (1.3) give:
1, =h. 0. and (I6) gives the
T + D2 S 02
21 + 100rg S o101
I3 I4 S o2
vs.
22 100x
o101
(23)
where a is a binary variable. The constraints on the right closely approximate the 17- n-partition (i.c., convex hull) bounds: 23 S a and x4 S a. But 21 and I2 are relatively unaffected by a perturbation = 1- 5 (when a is relaxed). Whereas the formulation on the left constrains the four variables equivalently. If the behavior of the node is dominated by a few inputs, the formulation on the right strong, as it approximates the convex hull over those inputs (2) ~ Z3 and 2g ~ xz in this case). For the practical case of N << 1) there are likely fewer partitions than dominating variables.
The size of the partitions can also be selected to be uneven:
T1 00 L2 + 1002z + 100x4 S 201
33 S 01
(24)
21
+ D2 + 100za S d102
Similar tradeoffs are seen here: the first formulation provides the tightest bound for 21, but 22 is effectively unconstrained and T3, Z4 approach "equal treatment." The second formulation provides the tightest bound for æ3, and a tight bound for T4, but Ø1, I2 are effectively unbounded for fractional a. The above analyses also apply to the case of OBBT. For the above example, solving relaxed model for max(#1 + 222) obtains bound that affects the two variables equivalently, while the same procedure for max(x; + 100xg) obtains bound that is much stronger for 23 than for 2 Similarly, max(x1 + x2) captures dependency between the two variables, while max(x11 + 100xa) Rs max(1100ra).
Relaxation Tightness. The partitions (and their bounds) also directly affect the tightness of the relaxation for the output variable y. The equivalent non- non-lifted realization (20) reveals the tightness of the above simple example. With two partitions, the choices of S₁ = {1. vs S1 = (1 result in the equivalent non -ifted constraints:
y S x + 100r3 + ob + 101)
y S + 22 + (b + 200)
]
y 5 + 100z4 + abb 101)
VS.
y S 100 + 100., + (b - 2)
(25)
Note that combinations Z, = 0 and Z, = 21, 3. to the big -partition the tightest formulation and (in addition to all possible 2- 2-partition constraints) includes:
in 20 are not analyzed here, as they correspond big-M/l-partition model and are unaffected by choice of partitions. The 4-partition model is
S x, + (b + 201), i = 1,2
(26)
y 100 + ab + 102), 3,4
(27)
The unbalanced 2-partition, i.c., the left of (5). closely approximates two of the 4-partition (i.c., convex hull) constraints (27) Analogous to the tradeoff's in terms of bound tightness, we that this formulation essentially neglects the dependence of on Ø1, 22 and instead creates the convex hull over 21 z1 100m: 23 and 22 Zz.. For this simple example, the behavior of y is dominated by 2a and 24,, and this turns out to be a relatively strong formulation. However, when N << 17, we expect neglecting the dependence of y on some input variables to weaken the model.
The alternative formulation, i.e., the right of (25). handles the four variables similarly and creates
the convex hull in two new directions: 21 21 + Z2 and 22 = 100(z3 I1). While this does not

---

model the individual effect of either I's or 24 on y as closely. it includes dependency between I' and T4. Furthermore, Ji and ø2 are modeled equivalently (i.e., less tightly than individual constraints). Analyzing partitions with unequal size reveals similar tradeoffs. This section shows that the proposed formulation has a relaxation equivalent to selecting subset of constraints from (0) with a tradeoff between modeling the effect of individual variables well vs the effect of many variables weakly.
Deriving Cutting Planes from Convex Hull. The convex-hull constraints (20) not implicitly mod- eled by a partition-based formulation can be viewed as potential tightening constraints, or cuts. Anderson et al. B provide linear-time method for selecting the most violated of the exponentially many constraints (20), which is naturally compatible with our proposed formulation (some constraints will be always satisfied). Note that the computational expense can still be significant for practical instances; Botoeva et al. [5] found adding cuts to <0.025% of branch-am and-bound nodes to balance their expense and tightening, while De Palma et al. 13 proposed adding cuts at the root node only.
Remark. While the above 4-D case may seem favor "unbalanced" partitions. it is difficult to illustrate the case where N << 17. Our experiments confirm "balanced" partitions perform better.
experimten
3.4 Strategies for Selecting Partitions
The above rationale motivates selecting partitions that result in model that treats input variables (approximately) equivalently for the practical case of N << 7/. Specifically, we seek to evenly distribute tradeoffs in model tightness among inputs. Section 3.3 suggests a reasonable approach to select partitions such that weights each are approximately equal (weights are fixed during optimization). We propose two such strategies below, as well as two strategies in red for comparison.
Equal-Size Partitions. One strategy is to create partitions of equal size, i.c., [S1] = [ ... [Sx (note that they may differ by up to one if 1) is not a multiple of N). Indices are then assigned to partitions to keep the weights in each as close as possible. This is accomplished by sorting the weights w and distributing them evenly among partitions (array_split (eplit((rrsoot(a)) N) in Numpy).
Equal-Range Partitions. A second strategy is to partition with equal range, i.e., range(w:)
range(w:). We define thresholds v E N+++1 such that t and u are min(w) and max(w). To iESy
reduce the effect of outliers, we define 22 and uN as the 0.05 and 0.95 quantiles of w, respectively. The remaining elements of are distributed evenly in UN). Indices i E (1...., 77) are then
assigned S, wy E [Mn, #n+1) This strategy requires N 2 3, but, for a symmetrically distributed weight vector, w, two partitions of equal size are also of equal range.
We compare our proposed strategies against the following:
Random Partitions. Input indices {1...., 7 are assigned randomly to partitions S1, Sy. Uneven Magnitudes, Weights are sorted and "dealt" in reverse to partitions in snake-draff order.
4 Experiments
Computational experiments were performed using Gurobi v 9.1 11) and models were implemented and trained using PyTorch (24). The computational set-up, solver settings, and models for MNIST 22
and CIFAR-10 20 are described in appendix A.4.
4.1 Optimal Adversary Results
The optimal adversary problem takes a target image ã. its correct label j. and an adversarial label k. and finds the image within range of perturbations maximizing the difference in predictions. Mathematically, this is formulated as max(f(
E X, where f and fy correspond to the k- and j-th elements of the NN output layer, respectively, and X' defines the domain of perturbations. We consider perturbations defined by the fi-norm (||=: æ||1 S 61 E RR,, which promotes sparse perturbations [8]. For each dataset, we use the first 100 test-datass images and randomly selected adversarial labels (the same 100 instances are used for models trained on the same dataset).
Table gives the optimal adversary results. Perturbations 6 were selected such that some big-M problems were solvable within 3600s (problems become more difficult as E increases). While our
7

---

Table 1: Number of solved (in 3600s) optimal adversary problems and average solve times for big-M vs N = (2. 4} equal-size partitions. Average times computed for problems solved by all formulations. Grey indicates partition formulations strictly outperforming big-M.
Dataset
Model
C1
Big-M
2 Partitions
4 Partitions
solved
avg vig.time(s)
solved
avg.time(s)
solved
avg. (ig.tim(()
MNIST
x 50
100
57.6
100
42.7
100
83.9
2 x 50
10
97
431.8
98
270.4
98
398.4
100
2.5
92
525.2
100
285.1
94
553.9
2 x 100
5
38
1587.4
59
587.8
48
1084.7
CNN1 W
0.25
68
1099.7
86
618.8
87
840.0
CNNI *
0.5
2
2293.2
16
1076.0
11
2161.2
CIFAR-I0
x 100
62
1982.3
69
1083.4
85
752.8
x 100
10
23
2319.0
28
1320.2
34
1318.1
*OBBT performed on all NN nodes
formulations consistently outperform big-M in terms of problems solved and solution times, the best choice of N is problem-dependent. For instance, the 4-partition formulation performs best for the 2 x 100 network trained on CIFAR-10 10; Figure (right) shows the number of problems solved for this case. The 2-partition formulation best for easy problems, but is soon overtaken by larger values of N. Intuitively, simpler problems are solved with fewer branch-ande aannchh-nd-boune nodes and benefit more from smaller subproblems. Performance declines again near N 7, supporting observations that the convex-hull formulation (N 1)) is not always best 3
Honvex-Hull-Baaee Cuts. The cut-generation strategy for big-M by Anderson al. [3] compatible with our formulations (Section 3.3) i.e., we begin with partition-based formulation and apply cuts during optimization. Figure 2 (left) gives results with these cuts added (via Gurobi callbacks) various cut frequencies. Specifically, a cut frequency of 1/k corresponds to adding the most violated (if any) each NN node every & frequencies; however, our formulations consistently outperform even the best cases using big-M with cuts. Moreover, cut generation is not always straightforward to integrate with off- off-the-shelf MILP solvers, and our formulations often perform just as well (if not better) without added cuts. Appendix A.5 gives results with most-violated cuts directly added to the model, as in De Palma al. 13.
nodes. Performance is improved at certain
100
N=1
N=2
N
N=1
N=6
X
N-2
x
N-7
80
80
N=3
N=8
solved (#)
solved (#)
N=10
60
40 x
40
20
0
//
16
10-5 10-4 10-3
10"2
10-1
100
0
10a
10a
cut frequency
time (s)
Figure 2: Number solved vs convex-hull-one frequency/run time for optimal adversary problems
5) for 2 x 100 models, without ОBBT. Left: N (equivalent big-M) performs worst on MNIST (dotted) and CIFAR-10 (solid) models for most cut frequencies. Right: each line shows 100 runs of CIFAR-10 model (no convex-hull cuts). N performs the worst; N performs well for easier problems; and intermediate values of N balance model size and tightness well.
Partitioning Strategies. FigureBsshowe the result of the input partitioning strategies from Section 3.4 on the MNIST with random and uneven partitions (red). With OBBT, big-M (N 1) outperforms parttiinn-based formulations when partitions are selected poorly. Figure again shows that our formulations perform best for some intermediate N: random/uneven partitions worsen with increasing N.
model for varying N. Both proposed strategies (blue) outperform formulations

---

100
Number Solved
Avg Time Solved
60
Eq. Size Range
Randem
10*
Eq. Size
Random
Ueven
Figure 3: Number solved (left) and solution times (right) for optimal adversary problems for MNIST
2 x 100 (e = 5). Each point shows 100 runs, max time of 3600s. Dashed lines show runs with OBBT, The equal range strategy requires N 3. Our proposed (blue) partitioning strategies solve more problems (top) faster (bottom) than random and uneven partitions (red)
Optimization-Bi Based Bounds Tightening. OBBT was implemented by tightening bounds for = We found that adding the bounds from the 1-partition model (i.e., bounds on Σ =/h) improved all models, as they account for dependencies among all inputs. Therefore these bounds were used in all models, resulting in 2N LPs per node (N 2). We limited the OBBT LPs 5s; interval bounds were used if an LP was not solved. Figure showss shows that OBBT greatly improves the optimization performance of formulations. OBBT problems for each layer are independent and could, in practice, be solved in parallel. Therefore, at minimum, OBBT requires the sum of max solution times found each layer (5s layers in this case). This represents an avenue to significantly improve MILP optimization of NNs via parallelization. In contrast, parallelizing branch-and-boun known to be challenging and may have limited benefits [1 26).
Table 2: Number verification problems solved 3600s and average solve times for big-M vs
N {2, 4} equal-size partitions. Average times computed for problems solved by all 3 formulations. OBBT was performed for all problems. Grey indicates formulations strictly outperforming big-M. MM.
Dataset
Model
Eoo
Big-M
2 Partitions
Partitions
sol.(f)
avg. time(s)
sol.(#)
time(s)
sol(#f)
time(s)
MNIST
CNNT
0.050
82
198.5
92
27.3
90
52.4
CNNI
0.075
30
632.5
52
139.6
42
281.6
CNN2
0.075
21
667.1
36
160.7
31
306.0
CNN2
0.100
1
505.3
5
134.7
246.3
CIFAR-10
CNNI
0.007
99
100.6
100
25.9
99
45.4
CNNI
0.010
98
119.1
100
25.7
100
45.0
CNN2
0.007
80
300.5
95
85.1
68
928.6
CNN2
0.010
40
743.6
176.4
35
1041.3
4.2 Verification Results
The verification problem is similar to the optimal adversary problem, but terminates when the sign of the objective function is known (i.c., the lower/upper bounds of the MILP have the same sign). This problem is typically solved for perturbations defined by the &oo -nom (| olooo < Exo E R). Here, problems are difficult for moderate 6 large < mis-classified example (positive objective) is easily found. Several verification tools rely on an underlying big-M formulation, e.g., MIPVerify 332. NSVerify 22, making big-M an especially relevant point of comparison. Owing to the early termination, larger NNs can be tested compared to the optimal adversary problems. We turned off cuts (cuts= 0) for the partition-baa based formulations, as models are relatively tight over box-domain perturbations and do not seem to benefit from additional cuts. On the other hand, removing cuts improved some problems using big-M and worsened others. Results are presented in Table Our formulations again generally outperform big-M (N=1), except for few of the 4-partition problems.

---

Table 3: Number of & fi-minimally distorted adversary problems solved in 3600s and average solve times for big-M vs N = {2, 4] equal-size partitions. Average times and 6 are computed for problems solved by all 3 formulations. OBBT was performed for all problems. Grey indicates partition formulations strictly outperforming big-M.
Dataset
Model
avg(e1)
Big-M
2 Partitions
4 Partitions
solved
avg.time(s)
solved
avg.time($)
solved
avg.time(s)
MNIST
2 x 50
6,51
52
675,0
93
150.9
89
166.6
2 x
4.41
16
547.3
37
310.5
31
424.0
2 x 100
2.73
7
710.8
13
572.9
10
777.9
4.3 Minimally Distorted Adversary Results
In similar vein as Croce and Hein [1 we define the f--minimally distorted adversary problem: given target image and its correct label j. find the smallest perturbation over which the NN predicts an adversarial label k. We formulate this as min 61; 1:ll Øb11 S 61; (x) 2 (z).. The <1.
adversarial label & is selected the accond-likeliess class of the target image. Figure provides examples illustrating that the f-normm promotes sparse perturbations, unlike the -norm. Note that the sizes of perturbations e dependent input dimensionality; it were distributed evenly, would correspond to an -norm perturbation 6oo 2 0.006 for MNIST models.
99
9
Target
61 4
6xc 0.05
Figure 4: Sample f1- vs fog -based minimally distorted adversaries for the MNIST x model. The true label (j) is "9," and the adversarial label (k) is '4.'
Table presents results for the minimally distorted adversary problems. As input domains are unbounded, these problems considerably more difficult than the above optimal adversary problems. Therefore, only smaller MNIST networks were manageable (with OBBT) for all formulations. Again, partition-based formulations consistently outperform big-M, solving more problems and in less time.
5
Conclusions
This work presented MILP formulations for ReLU NNs that balance having a tight relaxation and manageable size. The approach forms the convex hull over partitions of node inputs; we presented theoretical and computational motivations for obtaining good partitions for ReLU nodes. Furthermore, our approach expands the benefits of OBBT, which, unlike conventional MILP tools, can easily be parallelized. Results on three classes of optimization tasks show that the proposed formulations consistently outperform standard MILP encodings. allowing us solve 25% more of the problems (average >2X speedup for solved problems). Implementations of the proposed formulations and partitioning strategies are available at lhttt:://// gggbbb........ com/ caam/cog-iiii irogiimperia/// Partitioned:s armulatioss________..
Acknowledgments
This work was supported by Engineering & Physical Sciences Research Council (EPSRC) Fellowships to CT and RM (grants EP/T001577/1 and (P/P016871/1), an Imperial College Research Fellowship to CT, a Royal Society Newton International Fellowship 1X121191)194) to JK, grant by the Swedish Cultural Foundation in Finland to JK, and PhD studentship funded by BASF to AT.
10

---

References
[1] Tobias Achterberg and Roland Wunderling. Mixed integer programming: Analyzing 12 years of progress. In Facets of Combinatorial Optimization, pages 449 481. Springer, 2013.
[2] Michael Akintunde, Alessio Lomuscio, Lalit Maganti, and Edoardo Pirovano. Reachability analysis for neural agent-environment systems. In International Conference on Principles of Knowledge Representation and Reasoning. pages 184-193, 2018.
[3] Ross Anderson, Jocy Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming, pages 1-37, 2020.
[4] Egon Balas. Disjunctive Programming. Springer International Publishing, 2018. doi: 10.1007/ 978- 778-3-030-00148-3.
[5] Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient verification of ReLU-based neural networks via dependency analysis. Proceedings of the AAAI Conference Artificial Intelligence, volume 34, pages 3291-3299 2020.
[6] Rudy Bunel, Ilker Turkaslan, Philip HS Torr. Pushmeet Kohli, and M Pawan Kumar. unified view of piecewise linear neural network verification. arXiv preprint arXiv: 100455, 2017.
[7] Rudy Bunel, Alessandro De Palma, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip Torr, and M Pawan Kumar. Lagrangian decomposition for neural network verification. In Conference on Uncertainty in Artificial Intelligence, pages 370-379, PMLR. 2020.
[8] Pin- Yu Chen, Yash Sharma, Huan Zhang. Jinfeng Yi, and Cho-Jui Hsich. Ead: elastic- attacks to deep neural networks via adversarial examples. Proceedings of the AAAI Conference on Artificial Intelligence, volume 32, 2018.
[9] Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In International Symposium on Automated Technology for Verification and Analysis, pages 251 2568 Springer, 2017.
[10] Michele Conforti, Gérard Cornuéjols, and Giacomo Zambelli. Integer Programming, volume 271 of Graduate Texts in Mathematics, 2014.
[11] Francesco Croce and Matthias Hein. Minimally distorted adversarial examples with a fast adaptive boundary attack. In International Conference Machine Learning, pages 2196-2205. PMLR, 2020.
[12] Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy Liang, al. Enabling certification of verification-agnostii networks via memory effficient semidefinite programming. arXiv preprint arXiv:2010.11645, 2020.
memory-efficient
[13] Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip HS Torr, and M Pawan Kumar. Scaling the convex barrier with sparse dual algorithms. International Conference on Learning Representations, 2021.
[14] Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan. and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium, pages 121-138. Springer. 2018.
[15] Krishnamurthy Dvijotham. Robert Stanforth, Sven Gowal, Timothy A Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. In UAI, volume 1, page 3, 2018.
[16] Ruediger Ehlers. Formal verification of piece-wise linear feed-forwand neural networks. In International Symposium on Automated Technology for Verification and Analysis, pages 269- 286. Springer, 2017.
11

---

[17] Matteo Fischetti and Jason Jo. Deep neural networks and mixed integer linear optimization. Constraints, 23(3):296-309 2018.
[18] Bjame Grimstad and Henrik Andersson. ReLU networks surrogate models in mixed-integer linear programs, Computers & Chemical Engineering, 131:106580, 2019.
[19] Gurobi Optimization, LLC. Gurobi optimizer reference manual, 2020. URL http://wwr gurobi com
[20] Alex Krizhevsky. Learning multiple layers of features from tiny images. Master's thesis, The University of Toronto, 2009.
[21] Jan Kronqvist, Ruth Misener, and Calvin Tsay, Between steps: Intermediate relaxations between big-M and convex hull formulations, In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 299-314. Springer, 2021.
[22] Yann LeCun, Corinna Cortes, and CJ Burges. MNIST handwritten digit database. ATT Labs [Online]. Available: http::/yann.lecum www.:e/wwc..co/ee///iiiiis 2, 2010.
[23]
Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for feed-forward ReLU neural networks. arXiv preprint arXiv: arXiv 1706.0735, 2017.
[24]
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang. Zachary Vetooo, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang. Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems, pages 8024-8035. 2019.
[25] Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems, volume 31, pages 10877-10887, 2018
[26] Ted Ralphs, Yuji Shinano, Timo Berthold, and Thorsten Koch. Parallel solvers for mixed integer linear optimization. In Handbook of Parallel Constraint Reasoning, pages 283-336. Springer, 2018.
[27] Thiago Serra, Christian Tjandraatmadja, and Srikumar Ramalingam. Bounding and counting linear regions of deep neural networks. In International Conference on Machine Learning, pages 4558 4568-4566. PMLR, 2018.
[28] Thiago Serra, Abhinav Kumar, and Srikumar Ramalingam. Lossless compression of deep neural networks. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 417-430. Springer, 2020.
[29] Gagandeep Singh, Rupanshu Ganvir, Markus Plishell, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems, pages 15098-15109, 2019.
[30] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T Vechev. Boosting robustness certification of neural networks. In International Conference on Learning Representations, 2019.
[31] Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, KRUNAL KISHOR PATEL, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. In H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 21675-21686, 2020.
[32] Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv: 2017.
[33] Michael Volpp, Lukas P Fröhlich, Kirsten Fischer, Andreas Doemr Stefan Falkner, Frank Hutter, and Christian Daniel. Meta-learning acquisition functions for transfer learning in bayesian optimization. In International Conference on Learning Representations, 2019.
12

---

[34] Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsich, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLU networks, In International Conference on Machine Learning, pages 5276-5285. PMLR, 2018.
[35] Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pages 5286-5295. PMLR, 2018.
[36] Ga Wu, Buser Say, and Scott Sanner. Scalable planning with deep neural network learned transition models. Journal of Artificial Intelligence Research, 68:571-606, 2020.
13


Reviews:
[{"review_id": "sfYC4N7u3W", "reviewer": "Reviewer_Nod7", "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.", "questions": "", "limitations": "", "rating": 7, "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": "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).\n\nThere 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.\n\nThe 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.\n\nI recommend this paper for acceptance, but I propose a few minor corrections (particularly regarding mathematical formalization) and suggestions below.\n\nMathematical formalization issues:\n\n1. 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.\n\n2. 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).\n\n3. 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.\n\n4. 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.\n\n\nSuggestions for improving connections to previous work:\n\n5. 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).\n\n6. 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.\n\n7. 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.\n\n\nWriting issues and other notes:\n\n8. 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)?\n\n9. Line 79: $LB^a$, $UB^a$, $LB^b$, and $UB^b$ are not defined.\n\n10. In (12), should $y \\leq 0$ be $y \\geq 0$?\n\n11. Line 147 has a broken reference.\n\n12. 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.\n\n13. Line 186: Is this sentence \"The partitions ... constraints:\" meant to be here?\n\n14. Line 277: Typo: \"verfication\".\n\n15. 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?\n\n16. Could you clarify that Figure 2 is without OBBT, if that is the case?\n\n17. In Figure 3, why is it that N = 1 shows different values for non-OBBT? Is this just MIP solver variability?", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "This is not discussed but also not particularly relevant for this work.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "6"}, "extra_text": {}}, {"review_id": "iJPXs0LCVIG", "reviewer": "Reviewer_cKru", "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.", "questions": "", "limitations": "", "rating": 7, "confidence": 1, "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 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.\n\nMany 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.\n\nI did not find English issues.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "5"}, "extra_text": {}}, {"review_id": "hsVDWcvu9sg", "reviewer": "Reviewer_1SxU", "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.", "questions": "", "limitations": "", "rating": 7, "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 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.\n\nThe 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).\n\nThe 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.\n\nOther comments:\n* L14: The acronym \"NN\" is used without definition.\n* L76: What is the \"second equation\" being referred to?\n* 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?\n* 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.\n* L147: Broken references\n* 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.\n* 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.\n* Is the time reported in the tables accounting for the time spent on OBBT, or solely for the MIP?\n* How does the performance look for the new approaches _without_ OBBT? Put another way: how strongly dependent are the positive computational results on OBBT?\n* 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?\n* Figure 3: Please do not mix two charts with differing y-axes into one! It is very confusing and/or misleading to the reader.\n* 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.\n\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "No concerns.", "review_text": "", "extra_scores": {"ethical_concerns": "No concerns.", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "2"}, "extra_text": {}}, {"review_id": "ER1rX9S1uLB", "reviewer": "Reviewer_bEy7", "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. ", "questions": "", "limitations": "", "rating": 7, "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": "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.\n\n1. 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.)  \n2. 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.\n3. The format for the formulations in this paper (including the appendix) should be properly adjusted and aligned. \n4. Line 89, page 3: \"$\\sum_{n}z_n, n=1, \\ldots, N$\" should be \"$\\sum_{n=1}^N z_n$\".\n5. $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.\n6. Second disjunction in equation (12): \"$y \\leq 0$\" should be \"$y \\geq 0$\".\n7. 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. \n8. Line 147: what are (??)?\n9. For those convex hull based cuts, in order to add them, how do you solve the corresponding separation problem?\n10. Equation (52) in Appendix: here the subscript should be $I'_j$. Also, what is the reason for listing inequality (50) and (52) here?\n11. Inequalities (65), (66) in Appendix: you should mention what are these constraints (65), (66) when $w_n=0$.\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "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_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "7"}, "extra_text": {}}]

Author rebuttal:

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)