Neural Network Verification

Neural Network Verification (NNV) via MILP is proposed in [Cheng17,Tjeng19] as the problem of verifying the robustness of a fixed, trained neural network on a given input example: is there an input within a prescribed distance of the example on which the network outputs a class other than the correct one? If no such input exists, the network is robust (verified) on that example.

The instances come from the Neural Network Verification dataset of [Nair20] (DeepMind neural_mip_solving), provided by DeepMind and built with the MILP formulation of [Tjeng19] as used in [Gowal18]. Each instance verifies the “small” convolutional network of [Gowal18] (trained on MNIST) on one MNIST image, against \(\ell_\infty\) perturbations of radius \(\epsilon=0.1\). Rather than minimizing the perturbation, each instance maximizes the worst-case margin by which an incorrect class can beat the true class inside the \(\epsilon\)-ball; the network is robust on the example if and only if the optimal value is negative.

Inputs. A trained ReLU network; an image \(x^0\in[0,1]^{784}\) with true label \(y\); the \(\ell_\infty\) radius \(\epsilon\); interval bounds \([l_i,u_i]\) on every pre-activation, precomputed by bound propagation (used as big-M constants).

Network. Conv 16 filters \(4\times 4\), stride 2 (\(28\times28\to13\times13\times16\), 2704 neurons) \(\to\) ReLU \(\to\) Conv 32 filters \(4\times4\), stride 1 (\(10\times10\times32\), 3200 neurons) \(\to\) ReLU \(\to\) fully connected 100 \(\to\) ReLU \(\to\) fully connected 10 (logits).

Notation.

• \(\mathcal{I}\): input pixels (784); \(\mathcal{H}_1,\mathcal{H}_2,\mathcal{H}_3\): neurons of the two convolutional layers and the dense hidden layer; \(\mathcal{C}=\{0,\dots,9\}\): output classes; \(W^{(k)},b^{(k)}\): weights and biases of layer \(k\) (layer 4 is the output layer).
• For each hidden neuron \(i\) with pre-activation bounds \([l_i,u_i]\): \(i\) is stably inactive if \(u_i\le 0\) (its ReLU output is 0 and it is dropped), stably active if \(l_i\ge 0\) (its ReLU output equals the pre-activation), and unstable otherwise; \(\mathcal{U}_k\subseteq\mathcal{H}_k\) denotes the unstable neurons of layer \(k\).
• \(\mathcal{K}\subseteq\mathcal{C}\setminus\{y\}\): candidate adversarial classes (\(|\mathcal{K}|\) varies by instance, from 1 to 8 in the instances inspected and about 3 on average; the remaining classes were removed when the instance was generated); \([L_c,U_c]\): bounds on the margin of class \(c\).
• Variables: \(x_j\) input pixels; \(\hat z^{(k)}_i\) (free) pre-activations of layer \(k=1,\dots,4\); \(z^{(k)}_i\ge 0\) and \(\delta^{(k)}_i\in\{0,1\}\) for unstable neurons (\(\delta=1\) means the ReLU is active); \(\mu_c\) margin of class \(c\in\mathcal{K}\); \(m_1,\dots,m_{|\mathcal{K}|-1}\) pairwise maxima with binaries \(\beta_1,\dots,\beta_{|\mathcal{K}|-1}\).
• The input to layer \(k+1\) from neuron \(i\) of layer \(k\) is \(a^{(k)}_i=\hat z^{(k)}_i\) if \(i\) is stably active, \(a^{(k)}_i=z^{(k)}_i\) if \(i\in\mathcal{U}_k\), and \(a^{(k)}_i=0\) if \(i\) is stably inactive; \(a^{(0)}=x\).

Formulation. Let \(K=|\mathcal{K}|\). The maximum of the margins is built from \(K-1\) pairwise maxima \(m_r=\max(A_r,B_r)\) arranged in a balanced binary tree: the leaves are the margins \(\mu_c\), \(c\in\mathcal{K}\), each node's arguments \(A_r,B_r\) are two margins or two lower nodes, and the root \(m_{K-1}\) is the final maximum (for example, for \(\mathcal{K}=\{1,3,4,5,6,7,8,9\}\) the root is \(\max(\max(\max(\mu_1,\mu_3),\max(\mu_4,\mu_5)),\max(\max(\mu_6,\mu_7),\max(\mu_8,\mu_9)))\)). When \(K=1\) the objective is just \(\mu_{c}\) and there are no \(m_r\) or \(\beta_r\).

\begin{align} \max\ & m_{K-1}\\ \text{s.t. } & \max(0,x^0_j-\epsilon)\le x_j\le \min(1,x^0_j+\epsilon), && \forall j\in\mathcal{I}\\ & \hat z^{(k)}_i=\sum_{j} W^{(k)}_{ij}\,a^{(k-1)}_j+b^{(k)}_i, && \forall k\in\{1,2,3\},\ i\in\mathcal{H}_k\\ & \hat z^{(4)}_c=\sum_{j} W^{(4)}_{cj}\,a^{(3)}_j+b^{(4)}_c, && \forall c\in\mathcal{C}\\ & z^{(k)}_i\ge \hat z^{(k)}_i,\quad z^{(k)}_i\le \hat z^{(k)}_i-l_i\big(1-\delta^{(k)}_i\big),\quad z^{(k)}_i\le u_i\,\delta^{(k)}_i,\quad z^{(k)}_i\ge 0, && \forall k\in\{1,2,3\},\ i\in\mathcal{U}_k\\ & \mu_c=\hat z^{(4)}_c-\hat z^{(4)}_y,\quad L_c\le\mu_c\le U_c, && \forall c\in\mathcal{K}\\ & m_r\ge A_r,\quad m_r\ge B_r, && r=1,\dots,K-1\\ & m_r\le B_r+\big(U(A_r)-L(B_r)\big)\beta_r,\quad m_r\le A_r+\big(U(B_r)-L(A_r)\big)(1-\beta_r), && r=1,\dots,K-1\\ & \delta^{(k)}_i\in\{0,1\},\quad \beta_r\in\{0,1\}, \end{align}

where \([L(\cdot),U(\cdot)]\) are the bounds of a margin or node (for \(\mu_c\), \([L_c,U_c]\); for \(m_r\), the maxima of the bounds of its two arguments). The constraints for \(m_r\) encode \(m_r=\max(A_r,B_r)\), so \(m_{K-1}=\max_{c\in\mathcal{K}}\big(\hat z^{(4)}_c-\hat z^{(4)}_y\big)\). The ReLU constraints are the big-M encoding of [Tjeng19]: \(\delta=0\) forces \(z=0\) and \(\hat z\le 0\), and \(\delta=1\) forces \(z=\hat z\ge 0\).

The number of binary variables equals the number of unstable ReLUs plus \(K-1\) (about 171 on average), which varies across examples; all pre-activation variables of the 6014 neurons and 784 inputs are present in every instance.

@misc{huang2024distributional,
      title={Distributional MIPLIB: a Multi-Domain Library for Advancing ML-Guided MILP Methods}, 
      author={Weimin Huang and Taoan Huang and Aaron M Ferber and Bistra Dilkina},
      year={2024},
      eprint={2406.06954},
      archivePrefix={arXiv},
      primaryClass={cs.LG}
}

@inproceedings{cheng2017maximum,
  title={Maximum resilience of artificial neural networks},
  author={Cheng, Chih-Hong and N{\"u}hrenberg, Georg and Ruess, Harald},
  booktitle={Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3--6, 2017, Proceedings 15},
  pages={251--268},
  year={2017},
  organization={Springer}
}

@article{tjeng2017evaluating,
  title={Evaluating Robustness of Neural Networks with Mixed Integer Programming},
  author={Tjeng, Vincent and Xiao, Kai and Tedrake, Russ},
  journal={arXiv preprint arXiv:1711.07356},
  year={2017}
}

@article{nair2020solving,
  title={Solving mixed integer programs using neural networks},
  author={Nair, Vinod and Bartunov, Sergey and Gimeno, Felix and Von Glehn, Ingrid and Lichocki, Pawel and Lobov, Ivan and O'Donoghue, Brendan and Sonnerat, Nicolas and Tjandraatmadja, Christian and Wang, Pengming and others},
  journal={arXiv preprint arXiv:2012.13349},
  year={2020}
}