ScalingUpExactNeuralNetworkCompressionbyReLU Stability SupplementaryMaterial A1 DescriptionofMILPformulationforaReLUactivation

Theconstraintsareasfollows: wli xl 1+bli =yli (13) yli =xli χli (14) xli Mlizli (15) χli µli(1 zli) (16) xli 0 (17) χli 0 (18) zli {0,1} (19) Constraint (13) matches the layer inputxl 1 with the neuron preactivation outputyli. We then use the binary variablezli to match yli with the neuron output with eitherxli or 0. Whenzli = 1, constraints (16) and (18) imply thatχli = 0, and thus xli = yli due to constraint(14). We avoid explicitly enforcing that variablespli and qli are binary by leveraging thatzli is binary. Let us initially consider a formulation in whichPl = Ql = {1,...,nl} l L and then respectively remove from those sets each neuroni for whichpli = 1 and qli = 1 in any solution obtained. These compression operations are the same as in [79], but performed once per layer instead of once per neuron.