Formal verification of neural networks is essential for their deployment in safetycritical areas. Many available formal verification methods have been shown to be instances of a unified Branch and Bound (BaB) formulation. We propose a novel framework for designing an effective branching strategy for BaB. Specifically, we learn a graph neural network (GNN) to imitate the strong branching heuristic behaviour. Our framework differs from previous methods for learning to branch in two main aspects. Firstly, our framework directly treats the neural network we want to verify as a graph input for the GNN. Secondly, we develop an intuitive forward and backward embedding update schedule. Empirically, our framework achieves roughly 50% reduction in both the number of branches and the time required for verification on various convolutional networks when compared to the best available hand-designed branching strategy. In addition, we show that our GNN model enjoys both horizontal and vertical transferability. Horizontally, the model trained on easy properties performs well on properties of increased difficulty levels. Vertically, the model trained on small neural networks achieves similar performance on large neural networks.
This paper proposes to use graph neural networks (GNNs) to replace the
splitting heuristic in branch and bound (BaB) based neural network verification
algorithms. The paper follows the general BaB framework by Bunel et al., but
considers only splitting ReLU neurons, not input domains. The GNN is built by
replacing each neuron in network to be verified as a vertex, and the
connections between neurons as edges. Each vertex has a feature vector combining
information like pre-activation bounds and primal/dual LP solutions.  A
specialized GNN training procedure is developed to exploit the structure of the
problem, and the weights of GNN are updated in a forward and backward manner.
Overall the paper proposes a novel idea of using GNN for accelerating
verification and it is demonstrated to be effective on one MNIST network as
well as its wider and deeper variants.  I feel the main weakness is that the
empirical evidence provided are not thorough and sufficient (only 1 base model
on 1 dataset). Since this paper is 10-page, I evaluate it at a higher standard
and expect more convincing empirical results.
Questions and suggestions for improvements:
1. How much time does it take to generate training examples? It seems to me
that it is a very costly process because obtaining the relative improvement (8)
of splitting at each node can be quite expensive - basically, we need to split
almost every ambiguous neuron to get their improvement values, and in normal
BaB we only need to split one each time. The paper mentioned it "minimum 5%
coverage per layer" but does not provide more details. 
2. Also how much time does it take for training the GNN? It seems the GNN has
many vertices - the same number as the number of neurons in a network, which
can be quite large.  If the dataset generation and training time are much
longer comparing to the BaB time, the usefulness of the proposed method can be
limited especially it does not necessarily generalize to foreign networks
(networks with significantly different structure, or trained using different
methods).
3, An ablation study for the fail-safe strategy is needed. Without the
fail-safe strategy, is the GNN learned split better than other strong
heuristics? If the fail-safe strategy is too strong, the improvement we see can
probably come from the fail-safe strategy mostly, and GNN might not do too much
useful things. This is an important study that should be part of this paper.
4. It seems all networks in this work are trained using a single training
method, Wong & Kolter, 2018.  Does the split heuristic learned by GNN works for
networks trained using a different training strategy?  For example, interval
bound propagation (IBP) based methods [1][2] which achieve the state-of-the-art
results.  Also, adversarial training with L1 regularization is also verifiable,
as demonstrated in [3]. Running a few pretrained models by these methods should
be an easy experiment to add.
5. There have been a few strong baselines in this field that the authors do not
discuss and compare against, including [4][5][6]. They solve similar problems 
as in this paper and also provide promising results. At least, the authors should
discuss them in related works, and it is strongly encouraged to add at least one 
of them as a stronger baseline.
6. This paper claims that Neurify is theoretically incorrect (in Appendix D.2,
page 17). I am quite surprised and not sure if this claim is true. I am not
aware of any firm evidence that Neurify is theoretically incorrect.  It is
better to communicate with the authors of Wang et al., 2018 and make sure this
paper is making a correct claim.
Given that the idea proposed by this paper is novel and interesting, I tend to
accept this paper *under the condition* that the authors can conduct an
ablation study of the fail-safe strategy, provide generalization results on
models trained using different robust training strategies, and provide results
on at least one more dataset (like ACAS Xu, or CIFAR). Adding at least one more
baseline is also strongly encouraged.
** After author discussion, I have increased my score based on the new results
provided. The authors should make sure to include the ablation study results, and
a detailed discussion on training data generation time and training time in the
final version of the paper.
[1] Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. "On the effectiveness of interval bound propagation for training verifiably robust models." arXiv preprint arXiv:1810.12715 (2018).
[2] Huan Zhang, Hongge Chen, Chaowei Xiao, Bo Li, Duane Boning, and Cho-Jui Hsieh, "Towards Stable and Efficient Training of Verifiably Robust Neural Networks" (https://arxiv.org/abs/1906.06316)
[3] Xiao, K. Y., Tjeng, V., Shafiullah, N. M., & Madry, A. (2018). Training for faster adversarial robustness verification via inducing relu stability. arXiv preprint arXiv:1809.03008.
[4] Katz, Guy, et al. "The marabou framework for verification and analysis of deep neural networks." International Conference on Computer Aided Verification. Springer, Cham, 2019.
[5] Singh, G., Gehr, T., Püschel, M., & Vechev, M. (2018). Boosting Robustness Certification of Neural Networks.
[6] Anderson, G., Pailoor, S., Dillig, I., & Chaudhuri, S. (2019, June). Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 731-744). ACM.