Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 8: Accept
review_content: Summary:
This paper deals with complete formal verification of Neural Network, based on the Branch and Bound framework. The authors focus on branching strategies, which have been shown to be a critical design decision in order to obtain good performance. The tactic employed here is to learn a Graph Neural Network (which allows to transfer the heuristic from small networks to large networks), using supervised training to imitate strong branching. The authors also discuss fallback mechanism to prevent bad failures case, as well as an online fine-tuning strategy that provide better performance.
Experiments are performed on the CIFAR dataset and show convincing improvements compared to the baselines.

Comments:
* "This allows us to harness both the effectiveness of strong branching strategies and the efficiency of GPU computing power". Most other hand crafted heuristics also benefit from GPU computing, as they are based on gradients, or on the K&W dual, which all have GPU implementations.
* The description of the Nodes indicates that all hidden activation have a representative node in the GNN. Does it make sense to have it for non-ambiguous hidden activations?
* "Since intermediate lower and upper bounds of a node xˆi[j] are completely decided by the layers prior to it" -> That's not necessarily true depending on the Relaxation used. In the context of the full LP relaxation of Ehlers and branching on the ReLUs, constraint on following nodes can have an impact on earlier bounds. The authors make the same point later in the paragraph, so it's just a matter of being precise in the writing.
* "underlying data distribution, features and bounding methods are assumed to be same when the trained model is applied to different networks" -> This is a very reasonable assumption to make. Is there some intuition on which features are the most important? Given the features chosen, a strong relaxation needs to be used to obtain all the required features. Do the authors have any insights or experiments on how looser relaxations, which would lead to less feature available would fare? 
* With regards to the improvement measure (8), I'm slightly confused by the definition. It essentially measures independently and averages the improvement for each of the subdomain resulting of the split. In this case, if we go from one subdomain with a lower bound of -5, to a pair of subdomain with respective lower bounds (0, -5). (essentially we have split across a useless dimension), this metric will grant a certain amount of improvements, while the global lower bounds held by the BaB process will not have changed. Did the authors give a try to other metrics?
* I'm happy to see some discussion of the failures case of following a learned policy, leading to a series of bad decisions, which in my experience is a real problem. Am I correct in understanding the explanation that after a split is done, if it provides poor improvement, the split is undone and a back-up heuristic is applied? Or is it just that for the resulting subdomains of the low improvement split, the back-up heuristic is used?

* I'm wondering if some hand crafted heuristics could be learned by the model? As in, is the model expressible enough that it could encode the heuristics of Bunel, Royo or Wang? This would be an interesting analysis and show that following the learning approach is essentially a "free win". From what I can see, it wouldn't be able to as it is missing some information (the GNN doesn't have access to the bias of the network for example?), but I might be wrong.

* For the upper bound computations, "For the output upper bound, we compute it by directly evaluating the network value at the input provided by the LP solution". Is there some reference on how effective of a scheme that is, compared to more expected things like adversarial attacks?

* I know that they are not directly comparable but Gurobi provides the information about the numbers of branches that it performed internally. This would have been beneficial to obtain for the results of Table 1 and 2

* Am I correct in assuming that MIPplanet is the same method as in Bunel et al., where all intermediates bounds are computed with the method of Ehlers et al.? Given that solving LP on large networks can be quite slow, is this method penalized by using tight but very expensive bounds? Would a MIP with bounds based on the linear relaxation of (1b) be faster and provide a stronger baseline?

* One aspect that is missing from this paper is the discussion of the cost of generation of the training dataset, and of the training of the GNN? How many properties do you need to have to verify for it to make sense to learn a heuristic rather than just using a handcrafted one?
There might also be some more interest if the network was shown to generalize to other settings. We can already observe that there is at least some transfer between architectures and across "hardness of problems", but it would be great to see if it generalizes further (learn a GNN on MNIST, use it to verify CIFAR?)

Opinion:
The paper is quite interesting and outperform its baseline by a significant amount. I have some question about whether the MIP baseline is the best one but even if it could have been improved, I still think there is interest in methods that are more specialized and go beyond trusting a MIP solver.
review_title: Official Blind Review #4

final_score: rating: 6: Weak Accept
review_content: 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.

review_title: Official Blind Review #2

final_score: rating: 8: Accept
review_content: The paper proposes learning a branching heuristic to be used inside a branch-and-bound algorithm used for solving integer programming problems corresponding to neural network verification. The heuristic is parameterized as a neural network and trained to imitate an existing heuristic called Strong Branching which is computationally expensive but produces smaller branch-and-bound trees than other heuristics. A graph neural network architecture is used to take the neural network being verified as input, and a message passing schedule that follows a forward pass and a backward pass along the network being verified is used. An online learning variant is also considered that fine tunes the learned heuristic at test time as a problem instance is being solved. Results for verifying large convolutional neural networks on CIFAR-10 show approximately 2x improvement in average running time of the branch-and-bound algorithm.

Pros:
- Significant reductions in average running time across the various datasets.
- Well-written paper with clear figures (especially figure 2) and explanations. I enjoyed reading it.

Cons:
- Novelty is somewhat low, as it is a straightforward application of existing ideas like Gasse et al. NeurIPS’19 to the problem of verification. The idea of forward and backward message passing schedule is similar to the idea considered in Amizadeh et al., ICLR’19 (https://openreview.net/pdf?id=BJxgz2R9t7).
- It would be useful to present results on other datasets like MNIST. Even if they are not as impressive, it would be good to know when the proposed approach works and when it doesn’t.

Additional comments:
- Reporting average running time and number of branches can be sensitive to outliers. Shifted geometric mean will be less sensitive, please include these metrics.
- It would be good to compare against using a mixed integer program input representation (as done in Gasse et al., NeurIPS’19) of the verification problem to see what the difference in performance is. This can indicate how much benefit is obtained by conditioning on the neural network graph as the input representation and the associated forward-backward message passing schedule.
- How accurate is the learned heuristic in imitating strong branching? Is it necessary to get high accuracy on the imitation task to achieve an improvement in the final solve task?
- As a baseline it would be good to include the results for branch-and-bound using strong branching. Even if this is much slower, it would still help to know how much slower.
- I’m surprised that the reduction in the number of branches closely follows the reduction in the running time. This seems to suggest that the overhead of running graph neural network inference within branch-and-bound is negligible. Is this the case? If so, why -- is it because the LP solve time is much higher than the graph net inference time?

review_title: Official Blind Review #3

Meta-review: The authors develop a strategy to learn branching strategies for branch-and-bound based neural network verification algorithms, based on GNNs that imitate strong branching. This allows the authors to obtain significant speedups in branch and bound based neural network verification algorithms relative to strong baselines considered in prior work.

The reviewers were in consensus and the quality of the paper and minor concerns raised in the initial reviews were adequately addressed in the rebuttal phase. 

Therefore, I strongly recommend acceptance.
Decision: Accept (Talk)