Neural Network Branching for Neural Network Verification 
Authors: Jingyue Lu
M. Pawan Kumar
Venue:  (2020)
Keywords: Neural Network Verification
Branch and Bound
Graph Neural Network
Learning to branch

Abstract: Formal verification of neural networks is essential for their deployment in safety-critical 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.

NEURAL NETWORK BRANCHING FOR NEURAL NETWORK VERIFICATION
Jingyue Lu University of Oxford jingyue 1u0 ww.
M. Pawan Kumar
University of Oxford
pawan@robots ox. aaaauu.u .uk
ABSTRACT
Formal verification of neural networks is essential for their deployment in safety- critical areas. Many available formal verification methods have been shown 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 be- haviour. Our framework differs from previous methods for learning 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 re- quired for verification on various convolutional networks when compared 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 diffi- culty levels. Vertically, the model trained on small neural networks achieves simi- lar performance on large neural networks. Code for all experiments available lattps:// com/ oval carollggoou//aae GNN branching
the
INTRODUCTION
Despite their outstanding performances on various tasks, neural networks are found to be vulner- able to adversarial examples (Goodfellow et al. 2015) Szegedy et al. 2013). The brittleness of neural networks can have costly consequences in areas such as autonomous driving, finance and healthcare. When one requires robustness to adversarial examples, traditional model evaluation ap- proaches, which test the trained model on hold-out set, do not suffice. Instead, formal verification of properties such as adversarial robustness becomes necessary. For instance, to ensure self-driving cars make consistent correct decisions even when the input image slightly perturbed, the required property verify is that the underlying neural network outputs the same correct prediction for all points within a norm ball whose radius is determined by the maximum perturbation allowed.
Several methods have been proposed for verifying properties neural networks (NN), Bunel et al. (2018) showed that many of the available methods can be viewed as instances a unified BaB framework. A BaB algorithm consists of two key components: branching strategies and bounding methods. Branching strategies decide how the search space is recursively split into smaller spaces. Bounding methods compute bounds of each subspace tighten the bounds of the final objective function over the whole search space. In this work, we focus on improving the branching strategies. By directly working with a general framework, our identified algorithmic improvements can be combined with any bounding method, leading to potential performance improvement for BaB based verification algorithms.
Branching strategies have significant impacts on the overall problem-solving process, as it directly decides the total number steps, and consequently the total time, required to solve the problem at hand. The quality of branching strategy is even more important when NN verification problems are considered, which generally have a very large search space. Each input dimension or each activation unit can be a potential branching option and neural networks of interest often have high dimensional inputs and thousands of hidden activation units. With such a large search space, an effective branching strategy could mean large reduction of the total number of branches required, and consequently of the time required to solve a problem. Developing an effective strategy is thus of significant importance to the success of BaB based NN verification.
So far, to the best of our knowledge, branching rules adopted by BaB based verification methods are either random selection (Katz et al. 2017 Ehlers 2017) hand-designed heuristics (Wang al.

---

2018b
Bunel et al., 2018 Royo et al. 2019 Bunel et al. 2019). Random selection is generally in- efficient as the distribution of the best branching decision is rarely uniform. In practice, this strategy often results in exhaustive search to make verification decision. On the other hand, hand designed heuristics often involve a trade-off between effectiveness and computational cost. For instance, strong branching is generally one of the best performing heuristics for BaB methods in terms of the number of branches, but it is computationally prohibitive as each branching decision requires an ex- pensive exhaustive search over all possible options. The heuristics that are currently used in practice are either inspired by the corresponding dual problem when verification is formulated as an opti- mization problem (Bunel et al. 2018: Royo al. 2019) or incorporating the gradient information of the neural network (Wang et al. 2018b). These heuristics normally have better computational effi- cieney. However, given the complex nature of the search space, it is unlikely that any hand-designed heuristic is able to fully exploit the structure of the problem and the data distribution encountered in practice. As mentioned earlier, for large size NN verification problems, a slight reduction in the quality of the branching strategy could lead to substantial increase in the total number of branches required to solve the problem. A computationally cheap but high quality branching strategy is thus much needed.
In order to exploit the inherent structure of the problem and the data, we propose a novel machine learning framework for designing a branching strategy. Our framework is both computationally efficient and effective, giving branching decisions that are of a similar quality to that of strong branching. Specifically, we make the following contributions:
We use a graph neural network (GNN) to exploit the structure of the neural network we want to verify. The embedding vectors of the GNN are updated by novel schedule, which is both computationally cheap and memory efficient. In detail, we mimic the forward and backward passes of the neural network update the embedding vectors. In addition, the proposed GNN allows a customised schedule to update embedding vectors via shared parameters. That means, once training is done, the trained GNN model is applicable to various verification properties on different neural network structures.
We train GNNs via supervised learning. We provide ways to generate training data cheaply but inclusive enough to represent branching problems at different stages of a BaB process for various verification properties. With the ability to exploit the neural network structure and comprehen- sive training data set, our GNN is easy to train and converges fast.
Our learned GNN also enjoys transfcrability both horizontally and vertically. Horizontally, al- though trained with easy properties, the learned GNN gives similar performance on medium and difficult level properties. More importantly, vertically, given that all other parts of BaB algorithms remain the same, the GNN trained on small networks performs well on large networks. Since the network size determines the total cost for generating training data and is positively correlated with the difficulty of learning, this vertical transferability allows our framework to be readily applicable to large scale problems.
We further enhance our framework via online learning. For a learned branching strategy, it is expected that the strategy can fail to output satisfactory branching decisions from time to time. To deal with this issue, we provide an online scheme for fine-tuning the GNN along the BaB process in order to best accommodate the verification property at hand.
Finally, we supply a dataset on convolutional NN verification problems, covering problems at different difficulty levels over neural networks of different sizes. We hope that by providing large problem dataset it could allow easy comparisons among existing methods and additionally encourage the development of better methods.
Since most verification methods available work on ReLU-based deep neural networks, we focus on neural networks with ReLU activation units in this paper. However, we point out that our framework is applicable to any neural network architecture.
2 RELATED WORKS
Learning has already been used in solving combinatorial optimization problems (Bello et al. 2016 Dai et al. (017) and mixed integer linear programs (MILP) (Khalil et al.) 2016 Alvarez et al.
2017 Hansknecht et al. 20188) Gasse et al. 2019). In these areas, instances of the same underlying structure are solved multiple times with different data values, which opens the door for learning. Among them, Khalil et al. (016)). Alvarez et al. (217)), Hansknecht et al. (2018), and Gasse et al.)
2019) proposed learned branching strategies for solving MILP with BaB algorithms. These meth-
2

---

ods imitate the strong branching strategy. Specifically, Khalil et al. (2016) and Hansknecht et al. (2018) learn a ranking function to rank potential branching decisions while Alvarez et al. (2017) uses regression to assign branching score to each potential branching choice. Apart from imita- tion, Anderson et al. (2019) proposed utilizing Bayesian optimization to learn verification policies. There are two main issues with these methods. Firstly, they rely heavily on hand-designed features or priors and secondly, they use a generic learning structure which is unable to exploit the neural network architecture.
The approach most relevant to ours is the concurrent work by Gasse et al. 2019). They managed to reduce feature reliance by exploiting the bipartite structure of an MILP through GNN. The bipartite graph is capable of capturing the network architecture, but cannot exploit it effectively. Specifically, it treats all the constraints the same and updates them simultaneously using the same set of parameters. This limited expressiveness can result in difficulty in learning and hence in a high generalization error for NN verification problems. Our proposed framework specifically designed for NN verification problems. By exploiting the neural network structure, and designing customized schedule for embedding updates, our framework is able to scale elegantly both in terms of computation and memory. Finally, mention that the recently proposed verification methods (Katz et al. 2019] Siighh et al.] [2188] (Anderson et al.] 2019) are not explicitly formulated as BaBs. Since our focus is on branching, we mainly use the methods in Bunel al. (2019) for comparison.
BACKGROUND
Formal verification of neural networks refers to the problem of proving or disproving a property over bounded input domain. Properties are functions of neural network outputs. When a property can be expressed as a Boolean expression over linear forms, we can modify the neural network in suitable way so that the property can be simplified to checking the sign of the neural network output (Bunel et al., 2018). Note that all the properties studied in previous works satisfy this form, thereby allowing neural network f. bounded input domain C, formal verification examines the truthfulness of the following statement:
use the aforementioned simplification. Mathematically, given the modified
VE E C. If the above statement is true, the property holds. Otherwise, the property does not hold.
f(x) 2 0.
3.1 BRANCH AND BOUND
Verification tasks often treated as global optimization problem. We want to find the minimum of (xx over C in order to compare it with the threshold O. Specifically, we consider an I layer feed- forward neural network, f R| + R, with ReLU activation units such that for any σy E C C Rla]
f(x)) &r E R where
L;+1 = Wi+1 x; + b
for = 0,..,, 1, for 1,..=,L,,,,L 1-
(2a)
a;; max ( 0),
(2b)
The terms W and 6' refer to the weights and biases of the i-th layer of the neural network f. Domain C can be an fp norm ball with radius c. Finding the minimum of is challenging task, as the optimization problem is generally NP hard (Katz et al. (017).. To deal with the inherent difficulty of the optimization problem itself, BaB (Bunel et al. 2018 is generally adopted. In detail, BaB based methods divide into sub-domains, each of which defines a new sub-problem (branching). They then compute relaxed lower bound of the minimum on each sub-problen (bounding). The minimum of the lower bounds all the generated sub-domains constitutes a valid global lower bound of the global minimum over C. As recursive process, BaB keeps partitioning the sub- domains to tighten the global lower bound. The process terminates when the computed global lower bound above zero (property is true) or when an input with a negative output is found (property is false). A detailed description of the BaB is provided in the appendices. In what follows, we provide a brief description of the two components, bounding methods and branching strategies, that is necessary for the understanding of our novel learning framework.
3.2 BOUNDING
For NN verification problems, bounding consists of finding upper and lower bounds for the final output, the minimum of f(x) over C. An effective technique to compute a lower bound is to trans- form the original optimization problem into linear program (LP) by introducing convex relaxations over ReLU activation units. As we can see in Eq. (2). ReLU activation units do not define a convex feasible set, and hence, relaxations are needed. Denote the j-th element of the vector æ; xmf)
3

---

Possible convex relaxations for a hidden node 2i(]] that have been introduced far shown in Figure [ We replace ReLU with the shaded green area. The tighter the convex relaxation intro- duced, the more computational expensive it is to compute bound but the tighter the bound is going to be. From Figure || we note that in order to introduce a convex relaxation, we need intermediate bounds 44]]] and Wuyy]- Thus intermediate bounds
required for building the LP for the final out- put lower bound. Given their purpose and the large number of intermediate bound computations, rough estimations are mainly used. On the other hand, the final output lower bound is directly used in making the pruning decision and hence tighter lower bound is preferred as it avoids further unnecessary splits on the sub-proe sub-problem.
2 [
b
-0 Ebbl
4b
[U,
(a) Naive relaxation
(b) Linear bounds relaxation
(c) Planet relaxation (Ehlers 2017
Figure 1: Different convex relaxations introduced. For each plot, the black line shows the output of ReLU
activation unit for any input value between 4gj and Magy] and the green shaded area shows the convex relax- ation introduced. Naive relaxation (a) is the loosest relaxation. Linear bounds relaxation (b) is tighter and is introduced in Weng et al. (2018). Finally, Planet relaxation (c) is the tightest linear relaxation among the three considered (Ehlers 2017). Among them. (a) and (b) have closed form solutions which allow fast computations while (c) requires an iterative procedure to obtain an optimal solution.
3.3 BRANCHING
Branching is of equal importance as bounding in the BaB framework. Especially for large scale networks f. each branching step has a large number of putative choices. In these cases, the effec- tiveness of branching strategy directly determines the possibility of verifying properties over these networks within a given time limit. On neural networks, two types of branching decisions are used: input domain split and hidden activation unit split.
Assume we want to split a parent domain D. Input domain split selects an input dimension and then makes a cut on the selected dimension while the rest of the dimensions remain the same. The common choice is to cut the selected dimension in half and the dimension to cut is decided by the branching strategy used. Available input domain split strategies are [unell et al. (2018) and Royo et al. (2019). Royo et al. (2019)*s 's is based on sensitivity test of the LP on D while Bunel et al. (2018) use the formula provided in Wong & Kolter (018) to estimate final output bounds for sub-domain after splitting on each input dimension and selects the dimension that results in the highest output lower bound estimates.
In our setting, we refer to a ReLU activation unit T.G) = max(f;))) 0) as ambiguous over 'D if the upper bound Ud[ and the lower bound 4nj for žgbs have different signs. Activation unit split chooses among ambiguous activation units and then divides the original problem into cases of different activation phase of the chosen activation unit. If a branching decision is made on Embs] we divide the ambiguous case into two determinable cases: {zi(}) = 0, 0,44 S 4:p] S 0} and (M+() = ..pl], 0 S 6.6)) S ]. After the split, the originally introduced convex relaxation is re- moved, since the above sets are themselves convex. We expect large improvements on the output lower bounds of the newly generated sub-problems if good branching decision is made. Apart from random selection, employed in Ehlers (2117) and Katz et al. (2017), available ReLU split heuris- tics are Wang et al. (2)18a) and Bunel et al. 2019). Wang et al. (2018a) compute scores based on gradient information to prioritise ambiguous ReLU nodes. Similarly. Bunel et al.) (2019) use scores to rank ReI.U nodes but scores are computed with formula developed on the estimation equations in WWong& & Kolter (2018). We note that for both branching strategies, after the split, intermediate bounds are updated accordingly on each new sub-problem. For NN verification problems, either domain split or ReLU split can be used at each branching step. When compared with each other, ReLU split is more effective choice for large scale networks, as shown in Bunel et al. 2019).
All the aforementioned existing branching strategies use hand-designed heuristics. In contrast, we propose new framework for branching strategies by utilizing GNN to learn to imitate strong branching heuristics. This allows us to harness the effectiveness of strong branching strategies while retaining the efficiency of GPU computing power.
4

---

4 GNN FRAMEWORK
Overview We begin with brief overview of our overall framework, followed by a detailed de- scription of each of its components. a set of nodes V and a set of edges E, such that G (V, E). Each node and each edge has its set of features. A GNN uses the graph structure and node and edge features to learn representation vector (embedding vector) for each node v E V. The GNN is key component of our framework, which we treat the neural network / as a graph G₁. A GNN takes Gy as an input and initializes an embedding vector for each node in V. The GNN updates each node's 's embedding vector by ag- gregating its own node features and all its neighbours' embedding vectors. After several rounds of updates, we obtain learned representation (an updated embedding vector) of each node. To make a branching decision, we treat the updated embedding vectors as inputs to a score function, which assigns score for each node that constitutes potential branching option. branching decision is made based on the scores of potential branching decision nodes. Our framework is visualised in Figure We now describe each component in detail.
graph neural network G represented by two components:
Neural Network
Graph Neural Network
Forward Update
Onbokdagg
Risl Branching
e Uptra
Embedding Vectors
Backward Update
Figure 2: Illustration of our proposed GNN framework. An all zeros embedding network mimicking the neural network is initialised. Embedding vectors updated via several rounds of forward backward passes using updating Eqs. 33 We obtain the final branching decision by calling score function ga over all embedding vectors of the potential branching decision nodes.
Nodes Given neural network f, V consists of all input nodes [o[]]. all hidden activation nodes Mayl and an output node vt. In our framework, we combine every pre-activation variable and its associated post-activation variable and treat them as a single node. Pre- and post-activation nodes together contain the information about the amount of convex relaxation introduced at this particular activation unit, so dealing with the combined node simplifies the learning process. terms of the Eq. let واا denote the combined node of &.G) and z-t]]- The nodes tops] M|[]] and are thus in one-to-one correspondence with Tool "L1 and Fr. We note that V is larger than the set of all potential branching decisions as includes unambiguous activation nodes and output nodes.
Node features Different types of nodes have different sets of features. In particular, input node features contain the corresponding domain lower and upper bounds and the primal solution. For activation nodes, the node features consist of associated intermediate lower and upper bounds, the layer bias, primal and dual solutions and new terms computed using previous features. Finally, the output node has features including the associated output lower and upper bounds, the layer bias and the primal solution. Other types of features could be used and some features could be excluded if they are expensive to compute. We denote input node features as Zojz], activation node features as zi0] and output node features as z1. Our framework uses simple node features and does not rely on extensive feature engineering. Nonetheless. by relying on the powerful GNN framework, it provides highly accurate branching decisions.
Edges E consists of all edges connecting nodes in V, which are exactly the connecting edges in f. Edges are characterized by the weight matrices that define the parameters of the network ʃ such that for an edge e'k connecting [/] and 1141 we assign e/j W jk-
Embeddings We associate a p-dimensional embedding vector μu for each node e e V. All embedding vectors are initialised as zero vectors.
5

---

Forward and Backward embedding updates In general, graph neural network learns signals from graph by acting as function of two inputs: a feature matrix X' E RIVXx,, where each row the embedding vector Py for a node v E V. and an adjaceney matrix A representing the graph structure. Under this formulation, all node embedding vectors are updated at the same time and there is no particular order between nodes, In this work, instead, we propose an update scheme where only the nodes corresponding to the same layer of the network f are updated at the same way.
time, so embedding vector updates are carried out in a layer-by-layer
We argue that the forward-backwart updating scheme is natural fit for our problem. In more detail, for a given problem D, each branching decision (an input node or an ambiguous activation node) will generate two sub-problems 81 and $2, with each sub-domain having an output lower bound 2 and 1/2 respectively, equal to or higher than 1/ the lower bound that of DD Strong branching heuristic uses a predetermined function to measure the combined improvement of 1 and t over L/ and makes the final branching decision by selecting the node that gives the largest improvement. Thus, to maximise the performance of a graph neural network, we want a node embedding vector to maximally capture all information related to the computation of 1 and 12, For estimating 14, Lh of splitting on a potential branching decision node v, we note that these values are closely related to two factors. The first factor is the amount of convex relaxations introduced node v, when u corresponds to an ambiguous activation node. The second factor considers that the impact that splitting node o will have on the convex relaxations introduced nodes on layers after that of u. Recall that, if there are no ambiguous activation nodes, the neural network f is simply a linear operator, whose minimum value can be easily obtained. When ambiguous activation nodes are present, the total amount of relaxation introduced determines the tightness of the lower bound to f- We thus treat embedding vectors as a measure of local convex relaxation and its contribution to other nodes' convex relaxation.
branching decision
As shown in Figure 1. at each ambiguous activation node "'Dl" the area of convex relaxation intro- duced is determined by the lower and upper bounds of the pre-activate node R.p)). We observe that intermediate lower and upper bounds of node f.g) are significantly affected by the layers prior to it and have to be computed a layer-by-layer fashion. Based on the observation, we utilise a forward layer-by-layer update on node embedding vectors. This should allow these embedding vectors to capture the local relaxation information. In terms of the impact of local relaxation change to that of other nodes, we note that by splitting an ambiguous node into two fixed cases, all intermediate bounds of nodes on later layers will be affected, leading to relaxation changes at those nodes. We thus employ a backward layer-by-layer update to account for the impact the local change has over other nodes. Theoretically, by fixing an ambiguous ReLU node, intermediate bounds of nodes at previous layers and on the same layer might change as well. For a naturally trained neural network, the changes for these nodes should be relatively small compared to nodes the later layers. To updates.
account for these changes, we rely on multiple rounds of henward-and-backwee
In summary, during the forward update, for 1, .., L 1. we have, for all possible j.
MoD -- Pimp 0o), if pops = 0,
(3)
[a - Fact(2e (ZiLi) 14-1, e c²:01)) 01),
(4) pr. - (zu |T,- e,
(5)
During the backward update, for i = b....,,,. we have
Pg <- Buct (Zilg)) Met1, et1, 0s),
(6)
Mop] f- Bingl [o[]) M1, 0a).
Update functions F and B take the form of multi-layered fully-connected networks with ReLUU acti- vation functions or composites of these simple update networks. The terms 0, denote the parameters of the networks. A detailed description of update functions is provided in the appendices.
We point out that our howaadd-bacwward update scheme does not depend on the underlying neural network structure and thus should be generalizable to network architectures that differ from the one we use for training. However, does rely on the information used to compute convex relaxations, so underlying data distribution, features and bounding methods are assumed to be the same when the trained model is applied to different networks. Furthermore, our forward-backwant update is memory efficient, as we are dealing with one layer at a time and only the updated embedding vectors of the layer are used to update the embedding vectors in the next (forward- pass) and the previous (backward-pase passs) layer. This makes it readily applicable to large networks.

---

Scores At the end of the barkwrdd updates, embedding vectors for potential branching decision nodes (all input nodes and ambiguous activation nodes) are gathered and treated as inputs of a score function (.;:0s) Rº + R. which takes the form of a fully-connected network with parameters 05- It assigns a scalar score for each input embedding vector. The final branching decision is determined by picking the node with the largest score.
PARAMETER ESTIMATION
Training We train a GNN via supervised learning. To estimate θ = (0,, 01, 02 01. 0s), we propose new hinge rank loss function that is specifically designed for our framework. Before we give details of the loss, we introduce a relative improvement measure m first. Given a domain D, for each branching decision node v, the two generated sub-problems have output lower bounds 1 and - We measure the relative improvement of splitting the node over the output lower bound 1/ as follows
myg == (min((,) 0) + min(t",. 0) - -,, 2-15//(22115)
Intuitively, m (0 S m I 1) measures the average relative sub- hubb-roblem lower bound improvement to the maximum improvement possible, that is -1g. Any potential branching decision node v can be compared and ranked via its relative improvement value m4. Since we are only interested in branching nodes with large improvement measures, ranking loss is a natural choice. A direct pair- wise rank loss might be difficult to learn for NN verification problems, given the large number of branching decision nodes on each domain D. In addition, many branching decisions may give sim- ilar performance, so it is redundant and potentially harmful to the learning process if we learn a ranking among these similar nodes. To deal with these issues, we develop our loss by first dividing all potential branching nodes into M classes (M is much smaller than the total number of branching decision nodes) through the improvement value my of a node. We denote the class label as Y, for node Labels assigned in ascending order such that Y. >= Yor if my my. We then compute the pairwise hinge-rank loss on these newly assigned labels as
N
N
loss ( K
6(g. (1y; θ) go (1u: θ)) 1y,,y,),
(9)
where (bz) = (1 2) the hinge fuhction, N is the total number of branching decision nodes and K is the total number of pairs where Y, > Y; for any branching decision nodes v,, Vj. The loss measures the average hinge loss on score difference (go(1t;; )) Ia ( θ)) for all pairs of branching decision nodes U2 b/y such that Y, Y, Finally, we evaluate @ by solving the following optimization problem:
A 9 and n is the number of training samples.
1 -
+ arg min 2 1012
losSD, (O),
(10)
YI
where the losSD, the one introduced Eq.
Fail-safe Strategy We introduce fail-safe strategy employed by our framework to ensure that consistent high-quality branching decisions are made throughout BaB process. The proposed framework uses a GNN to imitate the behavior of the strong branching heuristic. Although com- putationally cheap, in some cases, the output decision by the learned graph neural network might be suboptimal. When this happens, could lead to considerably deteriorated performance for two reasons. Firstly, we observed that for certain problems, which requires multiple splits reach conclusion on this problem, if a few low-quality branching decisions are made at the beginning or the middle stage of the branching process, the total number of splits required might increase substan- tially. The total BaB path is thus, to some extent, sensitive to the quality of each branching decision apart from those made near the end of the BaB process. Secondly, once a low-quality decision is made on a given problem, a decision of similar quality is likely to be made on the two newly gen- erated sub-problems leading to exponential decrease in performance. Features for newly generated sub- cebb-rrobles are normally similar to those of the parent problem, especially in the cases where the branching decision of the parent problem made on the later layers and loose intermediate bounds are used. Thus, it is reasonable to expect the GNN fails again on the resulting sub- nub-problems.
To deal with this issue, we keep track of the output lower bound improvement for each branch- ing decision, as introduced in Eq. (8). We then set a pre-determined threshold parameter. If the improvement below the threshold, computationally cheap heuristic called to make a branch- ing decision. Generally, the back-up heuristic is able to give an above-threshold improvement and generate problems sufficiently different from the parent problem to allow the learned GNN to recover from the next step onwards.
7

---

Online Learning Online learning is strategy to fine-tune the network for particular property after we have learnt O It can be seen as an extension of the fail-safe strategy employed. Every time a heuristic branching decision node UA is used instead of the node Ugan chosen by the GNN, we can use th and ''gan to update the GNN accordingly. Since a correct GNN model should output an embedding vector 14, resulting in higher score 9s (s +) for the heuristic decision, loss can be developed based on the two scores 9s (1h; )) and 9s (Mgnn )) to generate optiiization signals for correcting the GNN behaviour. For example, the loss used in our experimental setting is:
losSontine (+) 9s (2 +) go ( )) + ((m; Mgnn) > t).
(11)
The last term is used to amplify (7 > 0) the loss if the relative improvement made by the heuristic decision is more than & percent higher than that by the GNN. We update @ of the GNN by taking one gradient step with small learning rate of the following minimization problem.
A 1|0112 + lo88entine (e)
+ = arg min
(12)
@ 2
Online learning is property specific: it uses the decisions made by heuristics to fine tune the GNN model so it can best accommodate the property at hand. As will be shown in our experiments, a small but significant improvement in performance is achieved when online learning is used.
6 EXPERIMENTS
We now validate the effectiveness of our proposed framework through comparative experiments against other available NN verification methods. A comprehensive study of NN verification methods has been done in Bunel et al. 2019). We thus design our experiments based on the results presented in Bunel al. (0119).
6.1 SETUP
We are interested in verifying properties on large network architectures with convolutional layers. In Bunel et al. (2019), existing NN methods are compared on a robustly trained convolutional net- work on MNIST. We adopt similar network structure but using a more challenging dataset, namely CIFAR-10, for an increased difficulty level. We compare against the following two methods: (i) MIPplanet, a mixed integer solver backed by the commercial solver Gurobi; and (ii) BaBSR, a BaB based method utilising ReLU-spli heuristic. Our choice is motivated by their superior performance over other methods for MNIST verification problems in the previous work (Bunel et al. 2019).
We provide the detailed experimental setup through four perspectives: bounding methods, branching strategies, network structures, and verification properties tested. (Bounding methods) We compute intermediate bounds using linear bounds relaxations (Figure [b)) For the output lower bound, we use Planet relaxation (Figure and solve the corresponding L.P with Gurobi. For the output upper bound, we compute it by directly evaluating the network value at the input provided by the LP so- lution. (Branching strategy) We focus on ReLU split only in our experiments. As shown in Bunel al.) (2019), domain split only outperforms ReLU split on low input dimensional and small scale networks. Also, since one of the Baseline method BaBSR employs ReLU-split heuristic, we con- sider ReLU split only for a fair comparison. However, we emphasize that our framework readily applicable to work with a combined domain and ReLU split strategy. (Network structures) Three neural network structures will be studied. The base one is of the similar structure and size to the one used in Bunel et al. (2019). It has two convolutional layers, followed by two fully connected layers and is trained robustly using the method provided in Wong & Kolter (2018). This particular choice of network size is made because the time required for solving each LP increases substan- tially with the size of the network. To best evaluate the performance of the branching strategy, we have work with medium sized network so that within the given timeout, a sufficient amount of branching decisions can be made to allow effective comparisons. When testing the transfcrability of the framework, two larger networks will be tested but their sizes are still restricted by the LP bottle- neck. A detailed description of the network architecture is provided in the appendices. (Verification properties) Finally, we consider the following verification properties. Given an image x for which the model correctly predicted the label ye, we randomly choose a label yer such that for given we want to prove (ele) - elc')T f'(x") > 0, Ya' s.t ||æ - x' 2'1|>0 S Here, f' is the original neural network, e(e) and e!d') one-hot encoding vectors for labels ye and yer We want to verify that for a given e, the trained network will not make a mistake by labelling the image as yer Since BaBSR is claimed to be the best performing method on convolutional networks, we use it determine the
8

---

values, which govern the difficulty level of verification properties. Small values mean that most ReLU activation units are fixed so their associated verification properties are easy to prove while large values could lead to easy detection of counter-cxamples, The most challenging e values are those at which a large number of activation units are ambiguous. We use binary search with BaBSR method to find suitable e values. We only consider e values that result in true properties and timed out properties. Binary search process is simplified by our choice of robustly trained models. Since these models are trained to be robust over ball, the predetermined value can be used starting value for binary search.
6.2 TRAINING DATASET
In order to generate training data, we firstly pick 565 random images and for each image, we ran- domly select an incorrect class. For each property, the e value is determined by running binary search with BaBSR and 800 seconds timeout, so the final set of properties consists of mainly easily solvable properties and a limited number of timed out properties.
We collect training data along BaB process for solving verification property. each given domain, given the large number of potential branching decisions, we perform the strong branching heuristic on a selected subset of all potential branching decisions. The subset consists of branching decisions that are estimated to be of high quality by the BaBSR heuristic and randomly selected ones, which ensure a minimum 5% coverage on each layer.
To construct training dataset that is representative enough of the whole problem space, need to cover a large number of properties. In addition, within a BaB framework, it is important to include training data at different stages of BaB process. However, running complete BaB process with the strong branching heuristic for hundreds of properties is computationally expensive and considerably time consuming. We thus propose the following procedure for generating training dataset to guarantee a wide coverage both in terms of the verification properties and BaB stages. For generated verification properties, we randomly select 25% of non-timeout property to conduct a complete BaB process with the strong branching heuristic. For the rest of the properties, we try to generate at least B- 20 training data for each verification property. Given the maximum number of branches g = 10 and an effective and computationally cheap heuristic, we first generate a random integer & from [0, z]. Then, we run a BaB process with the selected cheap heuristic for steps. Finally, we call the strong branching heuristic to generate training sample. We repeat the process until B training samples are generated or the BaB process terminated. A detailed algorithm is provided in the appendices.
6.3 BASE MODEL
We test our learned model on the same model structure but on properties of three different difficulty levels. Testing verification properties generated by binary search with BaBSR and 3600s timeout. We categorise verification properties solved within 800s as easy, which is consistent with training data generated, between 800s and 2400s as medium and more than 2400s as hard. In total, we generated 467 easy properties, 773 medium properties and 426 hard properties.
Results are given in the Table [ Methods compared in three perspectives: the average time over all properties, average number of branches required over the properties that are solved by all methods (we exclude timed out properties) and also the ratio of timed out properties. Since the properties are generated based on BaBSR, the timed out ratios of BaBSR on easy and medium properties are not comparable with that of other methods. All other numbers should give fair evaluation of the effectiveness of our branching strategy. BaBSR, GNN and GNN-online only differ in the branching strategy used.
On all three sets of properties, we see that our learned branching strategy has led to more than 50% reduction in the total average number of branches required for a property. As a direct re- sult, the average time required achieves at least 50% reduction as well. Our framework is thus an effective scheme and enjoys horizontal transferability. A further performance improvement is obtained through instance-specific online learning. Among all 1666 tested verification properties, GNN with online-learning solves 61.52% of properties with fewer number of branches and 60.20% of properties in less time when compared to the standard GNN.
We also provide a time cactus plot (Figure Baj for all properties on the Base model. Time cactus plots for each category of properties can be found in the appendices. All these time cactus plots look

---

Table I: Methods' Performance on the Base model. For easy, medium and difficult level verification properties. we compare methods' average solving time, average number of branches required and the percentage of timed out properties. GNN-Online outperforms other methods in all aspects.
Facy
Medium
Hard
Method
time(s)
branches
% Timenut
time(s)
branches
% Timenut
timets)
bmnchhs
% Timeout
BABSR
545,457
578.828
0.0
1370.395
1405.301
0.0
3127.985
2493,870
0,413
MIPELANET
1499,375
0.165
2240,980
0.430
2250.623
0.462
GNN
272.6M5
285.682
0.002
592.118
583,210
0.004
1577.156
995.437
GNN ONLINE
208.821
252.807
0.002
556.163
501,595
0.001
1369,326
813.502
0,183
Table 2: Methods' Performance on Large Models. For verification properties Wide large model and Deep large model, we compare methods' average solving time, average number of branches required and the per- centage of timed out properties. GNN-Online outperforms other methods in all aspects.
Wide
Deep
Method
time
branches
%Tmmecut
time
branches
%Timeou
BABSR
4137,467
843.476
0.0
4016.336
416.824
0.0
MIPPLANET
5855,059
0.743
5426.160
0.608
GNN
2367.693
387.403
0.127
2308.612
208.760
0.048
GNN-ONLINE
2179.306
353,879
0.095
2220.351
199.032
0.040
similar. Although BaBSR performs better than the commercial solver encoded method MIPplanet overall, MIPplanne wins on a subset of properties. The learned model GNN, however, is capable of giving consistent high quality performance over all properties tested.
6.4 TRANSFERABILITY: LARGER MODELS
We also robustly trained two larger networks. One has the same layer structure as the Base model but has more hidden units on each layer, which we refer to as the Wide model. The other has a similar number of hidden units on each layer but more layers. We refer to it as the Deep model. The detailed network architecture is provided in the appendices. Apart from the network structure, everything else is kept the same as for the Base model experiments. We use BaBSR and a timeout of 7200s to generate 300 properties for the Wide model and 250 properties for the Deep model. For these two models, each LP called for solving a sub-profe sub-problem output lower bound is much more time consuming, especially for the Deep model. This is reason that the average number of branches considered is much fewer that those of the Base model within the given time limit.
The model learned on the Base network is tested verification properties of large networks. Exper- imental results are given in the Table and time cactus plots (Figures 3bb 3c) are also provided. All results are similar to what we observed on the Base model, which show that our framework enjoys vertical transferability.
GMN
GVA
3MR
VPPcanee SaBSk
VPPdanet SaBSA
Vippaant SaBSS Del
Our CVd
Corp-iittete 1ime (.
Compureionn Corp.torooommmeee....
Compunicon Site 21.1
(c) Deep large model Figure 3: Cactus plots for the Base model (left), Wide large model (middle) and Deep large model (right). For each model, we plot the percentage of properties solved in terms of time for each method. Consistent performances are observed on all three models. BaBSR beats MIPplanet on the majority properties. GNN consistently outperforms BaBSR and MIPplanet. Further small improvements can be achieved through online- learning.
(a) Base model
(b) Wide large model
7 DISCUSSION
The key observation of our work is that the neural network we wish verify can be used to design GNN to improve branching strategies. This observation can be used in enhancing the performances of other aspects of BaB. Possible future works include employing GNNs to find fast-converging starting values for solving LPs on neural network and utilising GNNs to develop lazy verifier, that only solves the corresponding LP on a domain when it could lead pruning.
LEDNOWLEDGMENTS
This work is supported by Clarendon Fund Scholarship. We thank Rudy Bunel for useful discus- sions. We thank Florian Jaeckle for proofreading the article.
10

---

REFERENCES
Alejandro Marcos Alvarez, Quentin Louveaux, and Louis Wehenkel. A machine learning- -ased approximation of strong branching. INFORMS Journal on Computing, 19 2017.
Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat. Chaudhuri. Optimization and abstraction: synergistic approach for analyzing neural network robustness. ACM SIGPLAN Conference Programming Language Design and Implementation, 2019.
Irwan Bello, Hieu Pham, Quoc V Le, Mohammad Norouzi, and Samy Bengio. Neural combinatorial optimization with reinforcement learning. arXiv preprint arX1v.1611.09940 2016.
Rudy Bunel, Ilker Turkaslan, Philip H.S Torr, Pushmeet Kohli, and M. Pawan Kumar. A unified view of piecewise linear neural network verification. Advances in Neural Information Processing Systems, pp. 4790-4799, 2018.
Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H.S Torr, Pushmeet Kohli, and M. Pawan Ku- mar. Branch and bound for piecewise linear neural network verification. arXiv preprint arXiv: 1909.0089, 2019.
Hanjun Dai, Elias B. Khalil, Yuyu Zhang. Bistra Dilkina, and Le Song. Learning combinatorial optimization algorithms over graphs. Conference on Neural Information Processing Systems, 2017.
Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. Automated Technology for Verification and Analysis, 2017.
Maxime Gasse, Didier Chételat, Nicola Ferroni, Laurent Charlin, and Andrea Lodi. Exact combina- torial optimization with graph convolutional neural networks. arXiv preprint (00600/90000699 2019.
Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. The International Conference on Learning Representations, 2015.
Christoph Hansknecht, Imke Joormann, and Sebastian Stiller. Cuts, primal heuristics, and learning to branch for the time-dependent traveling salesman problem. arXiv preprint arXiv: vrxXiv:805.0/44 1805001415, 2018.
Guy Katz, Clark Barrett, David Dill. Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. International Conference on Computer Aided Verification, 2017.
Guy Katz, Derek Huang, Duligur lbeling, Kyle Julian, Christopher Lazarus, Rachel Lim, and Parth et al. Shah. The marabou framework for verification and analysis of deep neural networks. International Conference on Computer Aided Verification, 2019.
Elias Boutros Khalil, Pierre Le Bodic, Le Song, George Nemhauser, and Bistra Dilkina. Learning to branch in mixed integer programming. Thirtieth AAAI Conference Artificial Intelligence, 2016.
Vicenc Rubies Royo, Roberto Calandra, Dusan M Stipanovic, and Claire Tomlin. Fast neural net- work verification via shadow prices. arXiv preprint 1rXiv:1902.072441 2019.
Gagandeep Singh, Timon Gehr, Markus Pschel, and Martin. Vechev. Boosting robustness certifica- tion of neural networks. International Conference Learning Representations, 2018.
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 2013.
Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. International Conference on Learning Representations, 2019.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. Conference on Neural Information Processing Systems, 2018 8a..

---

Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. 27th {USENIX) Security Symposium ( (UUSENIX) Security 18), pp. 1599-1614, 2018b.
Tsui- Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Duane Boning, Inderjit Dhillon, and Luca Daniel. Towards fast computation of certified robustness for relu networks. International Conference Machine Learning, 2018.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. International Conference on Machine Learning, 2018.
APPENDIX A. BRANCH AND BOUND ALGORITHM
The following generic Branch and Bound Algorithm is provided in Bunel et al. (2019). Given neural network net and a verification property problem wish verify, the BaB procedure examines the truthfulness of the property through an iterative procedure. During each step of BaB, first use the pick_out function (line 6) to choose problem prob to branch The split function (line 7) determines the branching strategy and splits the chosen problem prob into sub-problems. We compute output upper and lower bounds each sub-problem with functions compute.. _BB and compute LB respectively. Newly computed output upper bounds are used to tighten the global upper bound, which allows more sub- sub-problems bound is greater than or equal to the global upper bound, so the smaller the global upper bound the better is. Newly calculated output lower bounds are used to tighten the global lower bound, which is defined as the minimum of the output lower bounds of all remained sub sub-problems after pruning. We consider the BaB procedure converges when the difference between the global upper bound and the global lower bound is smaller than
be pruned. We prune sub-problem if its output lower
our case, our interested verification problem Eq. T is a satisfiability problem. We thus can simplify the BaB procedure by initialising the global upper bound global_ub 0. As a result, prune all sub-problems whose output lower bounds are above addition. the BaB procedure is terminated early when a below 0 output upper bound of sub-problem is obtained, which means counterexample exits.
Algorithm Branch and Bound
I: function (net problem,
global_11 <- compute LB(net, problem)
3: global_ub ub <- compute UB (nete problem)
4: probs <- [[globallbbbbbbpca problem)
5: while global.ut global.lbb>>> de
(-.prob) - wwcpppcccouuoooo pickoot(pross)
7: [subprob.1.... subprob..j + split(prob)
8:
for i 1... do
9:
sub_lb + Bemputt__[(nettsubbll
10:
aub compute UB(net, subprab i) sub ub global ub then global ub <- sub ub prume.probs(probs, srrobbpproob..gobal..ub end
12:
13:
14:
15:
if sub_lb global.ub then
16:
arobs.append( subprob.ik end end for global 1b min(1b] (1b, prob) proba)
17:
18:
19:
20:
end while
21:
return global.uu
22:
end function
12

---

APPENDIX B. IMPLEMENTATION OF FORWARD AND BACKWARD PASSES
We give implementation details of forward and backward updates for embedding vectors for the model used in the experiments section. Choices of forward and backward update functions based on the bounding methods used. In our experiments, we used linear bound relaxations for computing intermediate bounds and Planet relaxation for computing the final output lower bound. We start with a graph neural network mimicking the structure of the network we want to verify. We denote domain lower and upper bounds as to and ue respectively. Similarly, we denote the intermediate bounds (pre-activation) for layers called for the final output lower bound, we have primal values for all nodes of V and dual values for all ambiguous nodes of V. Finally, let W ...... W be the layer weights and b' ...., b be the layer biases of the network f. which we wish to verify.
1, 1,.... I. - 1 as L and u, Since an LP solver
B.I FORWARD PASS
Unless otherwise stated, all functions F, are 2-layer fully connected network with ReLU activation units,
B. INPUT NODES
We update the embedding vectors of input nodes only during the first round of forward pass. That is update (a[;] when it zero for all j. After that, input nodes embedding vectors updated only in backward pass. For each input node, we form the feature vector 2o[i] as a vector of [o]5]. Mojj] and its associated primal solution. The input node embedding vectors are computed
Pogy = Fimp [Fo[s]: 0o)
(13)
1.2 ACTIVATION NODES
The update function Faet can be broken down into three parts: 1) compute information from local features 2) compute information from neighbourhood embedding vectors and 3) combine informa- tion from 1) and 2) to update current layer's 's embedding vectors.
Information from local features Since compute the final lower bound with the Planet laxation (Figure [c)), we introduce a new feature related to the relaxation: the intercept of the relaxation triangle, shown in Figure We denote intercept as and compute
-431 "bbl
But
(14)
U.(]] 4p
The intercept of a relaxation triangle can be used as a measure of the amount of relaxation introduced the current ambiguous node.
Therefore, the local feature vector 2i()] of an ambiguous node dby consists of 45)= "[[]), Pip). its associated layer bias value, primal values (one for pre-activation variable and one for post-activation variable) and dual values. We obtain information from local features via
Fact Fact-if 11 (z;b)) 0 if %/p) is ambiguous,
R
(15)
0
otherwise.
where Rapl E IRP.
Information from neighbourhood embedding vectors During the forward pass, we focus on embedding vectors of the previous layer only. To update an embedding vector on layer i, we first combine embedding vectors of the previous layer with edge weights via
Egil Σ &
W WWy (i-1(A)
(16)
To compute the information from neighbourhood embedding vectors to an arbitrary activation node Eig consider each activation unit as gate. We observe that the amount of the information
13

---

[4
Figure 4: Red line represents the intercept of the convex relaxation. It is treated as measure of the shaded green
100
(a) Ambiguous Node
(b) Complete Blocking
(c) Complete Passing
Figure 5: Depending on the value of Lis and u.s.), relaxed activation function can take three forms. The left figure shows the where [ays and Mgy of different signs. In this case, for any input value between 4pp and Mggz] the maximum output achievable is indicated by the line. The middle figure shows the case where both 41s) and wn[l are no greater than zero. In this case, the activation function completely blocks all input information by outputting zero for any input value. The right figure shows the case where 4D] and üرزs] are greater equal zero. In this case, the activation function allows complete information passing by outputting value equal the input value.
from neighbourhood embedding vectors that remains after passing through gate is dependent on the its lower bound 4[jj] and upper bound Utiy]. When bts) and Utiy] are of different signs, 44ty an ambiguous node. With relaxation, for any input value between 41 and u,y]), the maximum output
achievable after passing an activation unit is shown by the red slope in Figure 5la). The red slope s([]] is computed as
Sapl (Ba1g))
E0l + Bupl
(17)
401
Thus, the amount of information from neighbourhood embedding vectors that remains after passing through an ambiguous gate is related to the ratio a = - When Uziy] is no greater than zero, the activation node ='13 completely blocks all information. For any input value, the output value is zero after passing the activation unit, as shown by the red line in Figure 5(b). We have a 0 in this case. Finally, when 4[g] is no less than 0, the activation node ='t allows a complete passing of information and 1. It is shown by the red line in Figure (lc). We incorporate these observations into our evaluations and compute the information from neighbourhood embedding vectors as
4eld
Nabs = fact-nb Eng, a' -Epr):
(18)
where a' a when < a < and a' otherwise. Here, we use (a, bj denote the concate- nation of two vectors a, b E RD into vector of R2 We introduce a' to be more informative. We do not consider the information that relate to the intercept 3.g in the ambiguous case for the sake of simplicity. Improved performance could be expected if the Big related information is incorporated as well.
Combine previous information Finally, combine the information from local features and the information from neighbourhood embedding vectors to update the embedding vectors of activation nodes. Specifically,
Mip Fact-com ([111))) Napll: 07).
(19)
14

---

B.1.3 OUTPUT NODE
Embedding vectors of output nodes are updated in a similar fashion to that of activation nodes. We first compute information from local features.
Rıj = (f 09)
(20)
For output nodes, the vector of local features 2 consists of output lower bound, output upper bound, primal solution and layer bias. Fout-If is one-layer fully-connected network with ReLU activation units. We then compute information from neighbourhood embedding vectors. Since the
output node does not have activation unit associated with it, we directly compute the information of neighbourhood embedding vectors as
EbOl Σ Why P
(21)
Finally, we update the embedding vector of the output node
PLj Fout-com
([Rr1)) ca Ergy] 0%).
(22)
B.2 BACKWARD PASS
During backward message passing, for = L 1,..., 1, we update embedding vectors for activation nodes and input node. Again, all functions B, are 2-layer fully-comnected networks unless specified otherwise.
B.2.1 ACTIVATION NODES
Similar updates of embedding vectors carried out for activation nodes in forward pass, we update embedding vectors of activation nodes using the same three steps in the backward pass, but with minor modifications.
Information from local features We use the same feature 21(}] as the one used in the forward pass and compute the information from local features as
Baa is (Zzy); 03)
if [gg is ambiguous,
R -
(23)
otherwise.
We recall that dual value indicates how the final objective function is affected if its associated constraint is relaxed by a unit. To better measure the importance of each relaxation to the final objective function, we further update the information from local features by
Bant- 1/s ([dktz) @ Riy Rig 0%) if R #0
R
10
(24)
otherwise.
Here, day is the vector of dual values corresponding the activation node "Bps-- We use @ mean that we multiply Ripj by each element value of di(;) and concatenate them as singe vector.
Information from neighbourhood embedding vectors During the backward pass, we focus on embedding vectors the next layer only. In order to update an embedding vector on layer we compute the neighbourhood embedding vectors as
F
Σ Wit 1*+1(B)-
(25)
We point out that there might be an issue with computing Egg if the layer i + 1 a convolutional layer in the backward pass. For convolutional layer, depending on the padding number, stride number and dilation number, each node [bp]] may connect to different number of nodes on the layer + 1. Thus, to obtain a consistent measure of Eig) we divide Egj]] by the number of connecting node on the layer 1, denoted as 1 and use the averaged 1 instead. Let
Eb 10l
if layer i+1 convolutional,
Ebx
(26)
Ebb [
otherwise.
15

---

The following steps the same as the forward pass. We first evaluate
N [i Bact-no(le E a' E 03)
(27)
and the update embedding vectors as
Miyy com (R Nohh Minl:: 03)
(28)
B.2.2 INPUT NODES
Finally, update the input nodes. We use the feature vector zie which consists of domain upper bound and domain lower bound. Information from local features is evaluated as
Roj 1 0?).
(29)
We compute the information from neighbourhood embedding vectors in the same manner as we do for activation nodes in backward pass, shown Eq (26). Denote the computed information as Bogl The embedding vectors of input nodes are updated by
Mois = Binp- (1+ L 01).
(30)
APPENDIX C. ALGORITHM FOR GENERATING TRAINING DATASET
Algorithm 2 outlines the procedure for generating the training dataset. The algorithm ensures the generated training date have a wide coverage both terms of the verification properties and BaB stages while at the same time is computationally efficient. Specifically, we randomly pick 25% of all properties that not time out and run a complete BaB procedure on each of them with the strong branching heuristic to generate training samples (line 3-5). For the remaining properties, we attempt to generate training samples for each of them. To cover different stages of a BaB process of property, we use computationally cheap heuristic together with the strong branching heuristic. Given a property, we first use the cheap heuristic for l steps (line 10-15) to reach a new stage of the BaB procedure and then call the strong branching heuristic to generate training sample (line 16). We repeat the process until B training samples are generated or the BaB processs terminates.
Algorithm 2 Generating Training Dataset
1: Provided: total P properties; minimum B training data for each property; maximum branches between strong branching decisions
2: for I,.., P do:
3: a <- random number from [0, 1]
4: if not timed out property and S 0.25 then
5:
Running a complete BaB process with the Strong Branching Hcuristic
6:
else
7:
b=0
8:
while < B do
9:
t: t- random integer from[o, g]
while 0 do
11:
Call a computationally cheap heuristic if BaB process terminates then return
13:
end if
1: 1:
15:
end while
16:
Call the strong branching heuristic and generate training sample if BaB process terminates then return
17:
18:
end
19:
b = b++
20:
end while
21:
end if
22:
end for
16

---

APPENDIX D. EXPERIMENT DETAILS
All the hyper-parameters used in the experiments are determined by testing a small set of numbers over the validation set. Due the limited number of tests, we believe better sets of could be found.
D.1 TRAINING DETAILS
Training dataset To generate training dataset, 565 random images are selected. Binary serach with BaBSR and 800 seconds timeout are used to determine с on the Base model. Among 565 430 properties to generate 17958 training samples and verification properties determined, validation samples. Training samples and validation samples the rest of properties to generate 5923 are generated using Algorithm with B 20 and q 10.
For a typical epsilon value, each sub-domain generally contains 1300 ambiguous ReLU nodes. Among them, approximately 140 ReLU nodes are chosen for strong branching heuristies, which leads to roughly 200 seconds for generating training sample. We point out that the total amount of time required for generating a training sample equals the 2* LP solve "ime)e of am- biguous ReLUU nodes chosen). Although both the second and the third terms increase with the size of the model used for generating training dataset, the vertical transferability of our GNN enables us to efficiently generate training dataset by working with small substitute of the model interested in. our case, we trained on the Base model and generalised to Wide and Deep model.
Training We initialise GNN by assigning each node a 64-dimensional zero embedding vector. GNN updates embedding vectors through two rounds of forward and backward updates. To train the GNN, we use hinge rank loss (Eq. (9)) with M = 10. Parameters @ are computed and updated through Adam optimizer with weight decay rate À 1e-4 and learning rate 1e-4, If the validation loss does not decrease for 10 consecutive epochs, we decrease the learning rate by a factor of 5. the validation loss does not decrease for 20 consecutive epochs, we terminate the learning procedure. The batch size is set to 2. In our experiments, each training epoch took less than 400 seconds and the GNN converges within 60 epochs.
In terms of the training accuracy, we first evaluate each branching decision using the metric defined by Eq. ( Since there are several branching choices that give similar performance at each subdo- main, we considered all branching choices that have m. above 0.9 as correct decisions. Under this assumption, our trained GNN achieves 85.8% accuracy on the training dataset and 13.1% accuracy on the validation dataset.
D.2 VERIFICATION EXPERIMENT DETAILS
We ran all verification experiments in parallel on 16 CPU cores, with one property being verified on one CPU core. We observed that although we specifically set the thread number to be one for MIPplanet (backed by the commercial solver Gurobi), the time required for solving a property depends on the total number of CPUs used. For a machine with 20 epu cores, MIPplanet requires fewer (say 4) CPU cores in
much less time on average for proving the same set of properties parallel than on many (say 16) CPU cores in parallel (the rest of CPU cores remain idle). Since BaBSR, GNN and GNN-online all use Gurobi for the bounding problems, similar time variations, depending on the number of CPU cores used, are observed. We ran each method in the same setting and on 16 CPUs in parallel, so our reported results and time are comparable. However, we remind readers to take the time variation into consideration when replicating our experiments or using our results for comparison.
Fail-safe strategy Since, to the best of our knowledge, the branching heurisite of BaBSR is the best performing one on convolutional neural networks so far, we choose it for our fail-safe strategy. The threshold is set to be 0.2. Every time when the relative improvement mynn of GNN branching decision U gnn is less than 0.2, we call the heuristic to make new branching decision Uh. We solve
we have tried various other metrics, including picking the minimum of the two subdomain lower bounds and the maximum of the lower bounds. Among these metrics, metric defined by Eq. (8) performs the hest.
17

---

the corresponding LPs for the new branching decision and compute its relative improvement m4- The node with higher relative improvement is chosen to be the final branching decision.
Online learning We take a conservative approach in terms of online learning. We refer to GNN decision as a failed decision if the relative improvement offered by heuristic branching is better than the offered by the GNN. We record all GNN failed decisions and only update the GNN model online when the same failed decision is made at least twice. To update the GNN model, we use Adam optimizer with weight decay rate 1e- and learning rate 1e le- The GNN model is updated with one gradient step only with respect to the optimization problem Eq. (12) where = and 0.1 in the loss function losSontine. defined in Eq. (II.
le
D.3 BASELINES
We decided our baselines based on the experiment results of Bunel et al. (2019). In Bunel et al. (2019) methods including MIPplanet, BaBSK, planet (Fhlers 2017). reluBaB and reluplex (Katz et al. 2017) are compared on small convolutional MNIST network. Among them, BaBSR and MIPplanet significantly outperform other methods. We thus evaluate our methods against these two methods only in the experiments section. In order to strengthen our baseline, compare against two additional methods here.
Neurify (Wang et al., 2018a) Similar to BaBSR, Neurify splits ReLU activation nodes. It makes branching decision by computing gradient scores to prioritise ReLU nodes. Since the updated version of Neurify's 's released code supports verification, we conducted a comparison exper- iment between between Neurify and BaBSR for inclusiveness.
Neurify does not support CIFAR dataset. To evaluate the performance of Neurify, obtained the trained ROBUST MNIST model and corresponding verification properties from Bunel et al. (201)). We ranked all verification properties in terms of the BaBSR solving time and selected the first 200 properties, which are solved by BaBSR within one minute, as our test properties. For a fair comparison, have restricted Neurify use one CPU core only and the timeout limit to be two minutes. Among all test properties, Neurify timed out on 183 out of 200 properties. BaBSR thus outperforms Neurify significantly. Combining with the results of Bunel et al. (2019). BaBSR indeed fairly strong baseline to be compared against.
MIP based algorithm (Tjeng al., 2019) We also compared MIPplanet baseline against new MIP based algorithm (Tjeng et al. 2019), published in ICLR 2019. To test these two methods, randomly selected 100 verification properties from the CIFAR Base experiment with timeout 3600s. In terms of solving time, MIPplanet requires 1732.18 seconds on average while the new MIP algorithm requires 2736.60 seconds. Specifically, MIPplanet outperforms the new MIP algorithm on 78 out of 100 properties. MIPplanet is therefore strong baseline for comparison.
As caveat, we mention that the main difference between MIPplanet and the algorithm of (Tieng et al., 2019) is the intermediate bound computation, which is complementary to our focus. If bet- ter intermediate bounds are shown to help verification, we can still use our approach to get better branching decisions corresponding to those bounds.
D.4 MODEL ARCIITECTURE
We provide the architecture detail of the neural networks verified in the experiments in the following table.
18

---

Network Name
No. of Properties
Network Architecture
Conv2d(3,8,44 stride=2, padding=1)
Easy: 467
Conv2d(8, stride=2, padding=1)
BASE Model
Medium: 773
linear layer of 100 hidden units
Hard: 426
linear layer of 10 hidden units
(Total ReLU activation units: 3172)
Conv2d(3, 16,4, stride=2, padding=1) Conv2d( (6,,2,,4 stride=2, paddlig==1)
WIDE
300
linear layer of 100 hidden units
hidden units (Total ReLU activation units: 6244)
linear layer
Conv2d(3,88 stride=2, padding=1) Conv2d stride=1, packing==)
Conv2d(8,8,8 stride=1, padding=1)
DEEP
Conv2d(8,8, stride=2, padling=1)
linear layer of 100 hidden units linear layer 10 hidden units (Total ReLU activation units: 6756)
Table For each CIFAR experiment, the network architecture used and the number of verification properties tested.
APPENDIX E. ADDITIONAL EXPERIMENT RESULTS
E. FAIL-SAFE HEURISTIC DEPENDENCE
In all our experiments, we have compared against BaBSR, which employs only the fail-safe heuristic for branching. In other words, removing the GNN and using only the fail-safe heuristic is equivalent to BaBSR. The fact that GNN significantly outperforms BaBSR demonstrates that GNN is doing most of the job. To better evaluate the GNN's reliance a fail-safe heuristic, times that GNN branching decision is used for each verification property of a given model. Results listed in Table 4 On all three models, GNN accounts for more than 90% of branching decisions employed on average, ensuring the effectiveness of our GNN framework.
study the ratio of
Table 4: Evaluating GNN's dependence the fail-safe strategy. Given a CIFAR model, we collected the percentage of times GNN branching decision is used and the percentage of times the fail-safe heuristic (BaBSR in our case) is employed for each verification property. We report the average ratio of all verification propertics of the same model. To account for extreme cases, we also list the minimum and maximum usage ratios of the fail-safe heuristic for each model.
Model
GNN(avg)
BaBSR(avg)
BaBSR(min)
BaBSR(maa))
BASE
0.934
0.066
0.0
0.653
0.050
DEEP
0.964
0.036
0.0
0.290
E.2 GNN FEATURE ANALYSIS
We evaluate the importance of different features used in GNN, We note that two types of features are used GNN. The first type (including intermediates bounds, network weights and biases) can be collected at negligible costs. The other type is LP features (primal and dual values) that are acquired by solving a strong LP relaxation, which are expensive to compute but potentially highly informative. To evaluate their effect, we trained new GNN with LP features removed and tested the new GNN on 260 randomly selected verification properties on the Base model. Among the selected properties, 140 categorised as easy, 70 medium and 50 as hard. We denote the model trained on features as GNN and the newly trained model as GNN-R (we use to indicate reduced features).
19

---

Table Measuring importance of features by GNN. For easy, medium and difficult level verification properties, we compare methods' average solving time, average number of branches required and the percentage of timed out properties.
Easy
Hard
time(s)
branches
TTmmeuu
tine(s)
branches
7 %TTeeoul
timee(s)
% Timeoul
BABSR
429.589
641.300
0.0
1622.669
1504.366
0.0
2466.712
1931,98
GNN
268.592
319.386
0.0
724.883
529.070
0.0
1025 826
772.667
0.0
GNN-R
348.482
441.043
0.0
898.011
720.958
0.0
1340.559
967.804
From Table 5 we observe that removing primal and dual information deteriorates the GNN perfor- mance, but GNN-R still outperforms the baseline heuristic BaBSR. We believe cheap features are the most important. Depending the cost of LP, potential users can either remove expensive LP features or train a GNN with a smaller architecture.
E.3 MIPPLANET BRANCHING NUMBER
MIPplanct is implemented with the commercial solver Gurobi. Since Gurobi outputs internal branch number, we recorded MIPplanet branch number for a subset of verification properties for each model. In detail, we randomly selected 120 properties of various difficulty levels for the Base model and properties each for the Wide and Deep model. Results are summarised in Table [
One key observation we made is that Gurobi branch number is not positively related to the solving time. For instance, on timed out properties of the Wide model, MIPplanet branch number varies be- tween and 7479. We suspect Gurobi performs cutting before branching, so time spent on branching varies between properties, leading to inconsistent branch number and solving time. As the result, the MIPplanet branch number is not comparable with that of BaBSR, GNN and GNN-online. This also the reason that we not include MIPplant branch number in Table and Table 2
Table 6: Methods' performance randomly selected properties. We show methods' average solving time, average number of branches required and percentage of timed out properties. We emphasize that MIPplanet branch number is not comparable with those of other methods.
Base
Wide
Deep
Method tmmcts)
branches
% Timeout
time(s)
branches
% Timeout
timets)
branches
%Timcour
BABSR
1472.508
1420.839
0.067
2985,190
918.167
0.111
3811.712
482.165
0.111
1783.800
2949.625
0.556
4566.080
4332.375'
GNN
714.224
817.017
0.017
996.811
268.333
0.074
1893.081
201.500
0.0
GNN-ONLINE
582.738
642.387
0.008
949.694
257.667
0.033
1776.278
192.167
E.4 LP SOLVING TIME AND GNN COMPUTING TIME
We mention that LP solving time the main bottleneck for branch-and and-aound based verification methods. Although both GNN evaluation time and LP solving time increase with the size of network, LP solving time grows at significantly faster speed. For instance, in CIFAR experiments, GNN requires average 0.02, 0.03, 0.08 seconds make a branching decision Base, Wide and Deep model respectively but the corresponding one LP solving time on average are roughly 1.1, 4.9, 9,6 seconds. GNN evaluation almost negligible for large neural networks when compared to LP solving time.
E.5 GROMETRIC MEAN
For all our experiments, we based our analyses on the statistics of average solving time and branch- ing number. To ensure the reported numbers are not biased by potential outliers, we measure meth- ods' performance with the geometric mean as well and summarize results in Table 7 and Table 8 Statistics of geometric mean are consistent with that arithmetic mean, validating the analyses of the main paper.
20

---

Table Methods' Performance on the Base model. For easy, medium and difficult level verification properties, we compare methods' geometric average solving time, geometric average number of branches required and the percentage of timed out properties. GNN-Online outperforms other methods in all aspects.
Easy
Medium
Hard
Method
timets)
branches
% Timcout
timets)
branches
Timcout
timets)
branches
%Timcour
BABSR
471.547
468.117
0.0
1304,032
1236.398
0.0
5094, 794
2271,796
0.413
MIPPLANET
836.049
1401.273
0440
1374.794
GNN
180.638
191,514
0.002
412.880
417,970
0.004
985.142
691.599
0.216
GNN-ONLINE
143,968
180.575
0.002
399.786
380.463
0.001
833.343
605.443
0.183
Table 8: Methods' Performance on Large Models. For verification properties on Wide large model and Deep large model, we compare methods' geometric average solving time, geometric average number of branches required and the percentage of timed properties. CNN-Onllne outperforms other methods in all aspects.
Deep
%TTmooot
branches
%TTmsout
BA BSR
3510.960
699, 826
0.0
3580.469
359.464
0.0
MIPPLANET
4430.098
0.743
4014.469
0.608
GNN
296.821
0.127
1529.542
GNN-ONLINE
1316.455
279.298
0.095
1502.349
155.523
0.040
E.6 ADDITIONAL PLOTS
We provide cactus plots for the Base model on easy, medium and hard difficulty level properties respectively.
GRN
CBR
MiPyanet
M-Paaneet
Nippaanet
Babsh
Compaasin mn
(a) Easy properties
(b) Medium properties
(c) Hard properties
Figure 6: Cactus plots for easy properties (left), medium properties (middle) and hard properties (right) the Base model. For each category, plot the percentage properties solved in terms of time for each method. BaBSR beats MIPplanet on easy medium properties overall. On hard properties, although BaBSR manages to solve more properties, its average performance is worse than MIPplanet terms of time. GNN consistently outperforms BaBSR and MIPplanet on all three levels of properties, demonstrating the horizontal transfcrability of our framework. Again, further small improvments can he achieved through online-lcarning.
APPENDIX F. MNIST DATASET
We replicate the CIFAR experiments the MNIST dataset to test the generalization ability of our GNN framework.
F. MODEL ARCHITECTURE AND VERIFICATION PROPERTIES
We trained three different networks on MNIST with the method provided in Wong & Kolter (0018) The base model is mainly used for generating the training dataset and testing the horizontal gener- alization ability of the trained GNN. The Wide and Deep models are used for evaluating the vertical generalization. Verification properties found via binary search with BaBSR. We set the binary search time limit to 1800 seconds for the Base model and 3600 seconds for the other two models.
21

---

Network Name
No. of Properties
Network Architecture
Conv2d(1,4,4 stride=2, padding=1l
Conv2d(4,8,44 stride=2, padding=1)
BASE
100
linear layer of 50 hidden units
linear layer of 10 hidden units
(Total ReLU activation units: 1 1226)
Conv2d(1 1,,,4, stride=2, padding=11) Conv2d 26,,2,4, stride=2, paddlng==1)
WIDE
100
linear layer of 100 hidden units
hidden units (Total ReLUU activation units: 4804)
linear layer
Conv2d(1, ,88,4 stride=2, padding=1) Conv2d stride=1, packing==) Conv2d(8,88) stride=1, padding=1) Conv2d(8,8 stride=2, padling=1) linear layer of 100 hidden units linear layer 10 hidden units (Total ReLU activation units: 5196)
DEEP
100
Table For each MNIST experiment, the network architecture used and the number of verification properties tested.
F.2 TRAINING DETAILS
Training dataset Training dataset is generated on the Base model. We point out that we explicitly choose a Base model of small network size for efficient and fast training data generation.
To generate a training dataset, 538 random MNIST images are selected. Binary serach with BaBSR and 600 seconds timcout are used to determine on the Base model. Among 538 verification proper- ties determined, we use 403 properties to generate 18231 training samples and the rest of properties generate 5921 validation samples. Training samples and validation samples are generated using Algorithm
2 with B = 20 and = 10. For a typical epsilon value, each sub-domain generally contains 480 ambiguous ReLU nodes. Among them, approximately ReLU nodes are chosen for strong branching heuristics, which leads to roughly 45 seconds for generating training sample.
Training The same set of parameters and training procedure are used for training GNN for MNIST dataset. The GNN converges in 70 epochs with each epoch took less than 400 seconds. The trained GNN reached 86.5% accuracy on the training dataset and 83.1% 1% accuracy on the validation dataset.
F.3 EXPERIMENT RESULTS
We first note that we use verification properties with timeout 1800 seconds on the Base model to allow for an integrated evaluation of GNN on both its performance and its horizontal transferability. Vertical transferability is tested on the Wide and Deep model.
We observe that MIPplanet outperforss model. Given that the network size of the Base model is particularly small (1226 hidden units only), we believe that MIP algorithms backed by commercial solvers could be the most effective tool on verification problems of small size. Our conjecture is further confirmed by the fact that MIPplanet timed out on almost all properties of both the Wide and Deep models. On all three models, GNN consistently outperforms BaBSR, demonstrating the transferability of our framework. Finally, when online learning is considered, we found effective in fine- tuning the trained GNN and enabling further performance improvements, especially the Wide model.
BaB based methods on verification properties of the Base
22

---

Table 10: Methods' Performance on different models. the Base, Deep model, we compare methods' average solving time, average number of branches required and the percentage of timed out properties respectively. MIPplanet performs the best on the Base model while GNN-Online outperforms other methods on the Wide and the Deep model.
Base
Wide
Deep
Mothod
timots)
branches
% Timcout
time(s)
branches
Timcout
timets)
branches
% Timcoou
BABSR
878.226
2659.276
0.0
1888.084
399.571
0.0
1895.032
211.644
0.0
MIPELANET
411.167
0.0
3567.109
0.990
3437.918
0.833
GNN
623.291
1549.867
1526.381
322.510
0.040
1189.271
144.238
0.010
GNN-ONLINE
$47.102
1363,057
0.009
1133.429
283.673
0.010
1121.066
139.980
0.0
BaRSs
BaRSk
BaRSR
Can Crlins
Ovll
Compuriion Time
Computatenire (ire)
Cimp-balinn (D1e)
(a) Base model
(b) Wide large model
(c) Deep large model
Figure 7: Cactus plots for Base model (left), Wide large model (middle) and Deep large model (right). For each model, we plot the percentage of properties solved in terms of time for each method. MIPplanet outperforms all BaB based method on the Base model. However, once model size get larger, MIPplanet's performance deteriorates quickly. ON the Wide and Deep model, MIPplanet timed and outperformed by BaBSR. GNN consistently outperforms BaBSR all three models, demonstrating the transferability of our framework. Again, further small improvements can be achieved through online-learning.
most properties
F.4 FAIL-SAFE HEURISTIC DEPENDENCE
Results of Table ensure that the trained GNN is indeed account for the most branching decisions.
Table 11: Evaluating GNN's dependence the fail-safe strategy. Given MNIST model, collected the
percentage of times GNN branching decision is used and the percentage of times the fail-safe heuristic (BaBSR our case) employed for each verification property. report the average ratio all verification properties of the same model. To account for extreme cases, we also list the minimum and maximum usage ratios of the fail-safe heuristic for each model.
Model GNN(avg)
BaBSR(avg)
BaBSR(min)
BaBSR(max)
WIDE
0.884
0.116
0.0
0.376
DEEP
0,938
0.062
0.0
0.407
F.5 GEOMETRIC MEAN
The consistency between the results of Table 12 and Table 10 confirm that our analyses based on arithmetic mean are not biased by outliers.
Methods' Performance on different models. For the Base, Wide and Deep model, compare methods' geometric average solving time, geometric average number of branches required and the percent- age timed out properties respectively, MIPplanet performs the best on the Base model while GNN-Online outperforms other methods on the Wide and the Deep model.
Table 12:
Base
Wide
Deep
Method
lime(fs)
brunches
% TTmmoout
limefs)
branches
% Timeoout
timets)
brunches
% Timeout
BABSR
740.740
2210.248
0.0
1683.816
362,171
0.0
1694.55 555
187.723
0.0
MIPELANET
330.455
3506.400
0.990
3356.780
GNN
501.966
1268.780 780
0.019
1267.736
284.452
0.040
1022.466
131.171
0.010
GNN-ONLINE
450.053
1123.867
0.009
973.015
254.641
0.0
991,552
128.115
0.0
23

---

F.6 TRANSFERABILITY BETWEEN DATASETS
To evaluate whether our framework can generalize further to support transferring between datasets, tested CIFAR trained GNN MNIST verification properties. In detail, have tested the GNN on 20 randomly picked verification properties of MNIST Base model. We found that BABSR outperforms CIFAR trained GNN on all properties, so the CIFAR trained GNN model does not transfer to MNIST dataset. This is expected as MNIST and CIFAR images differ significantly from each other.
24


Reviews:
[{"review_id": "rJxXbtWRFH", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "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.\n\nPros:\n- Significant reductions in average running time across the various datasets.\n- Well-written paper with clear figures (especially figure 2) and explanations. I enjoyed reading it.\n\nCons:\n- 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).\n- 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.\n\nAdditional comments:\n- Reporting average running time and number of branches can be sensitive to outliers. Shifted geometric mean will be less sensitive, please include these metrics.\n- 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.\n- 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?\n- 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.\n- 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?\n", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "HJetcZYmqB", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Summary:\nThis 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.\nExperiments are performed on the CIFAR dataset and show convincing improvements compared to the baselines.\n\nComments:\n* \"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.\n* 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?\n* \"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.\n* \"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? \n* 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?\n* 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?\n\n* 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.\n\n* 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?\n\n* 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\n\n* 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?\n\n* 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?\nThere 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?)\n\nOpinion:\nThe 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.", "extra_scores": {"experience_assessment": "I have published in this field for several years.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I carefully checked the derivations and theory."}, "extra_text": {}}, {"review_id": "H1eFFHskqS", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper proposes to use graph neural networks (GNNs) to replace the\nsplitting heuristic in branch and bound (BaB) based neural network verification\nalgorithms. The paper follows the general BaB framework by Bunel et al., but\nconsiders only splitting ReLU neurons, not input domains. The GNN is built by\nreplacing each neuron in network to be verified as a vertex, and the\nconnections between neurons as edges. Each vertex has a feature vector combining\ninformation like pre-activation bounds and primal/dual LP solutions.  A\nspecialized GNN training procedure is developed to exploit the structure of the\nproblem, and the weights of GNN are updated in a forward and backward manner.\n\nOverall the paper proposes a novel idea of using GNN for accelerating\nverification and it is demonstrated to be effective on one MNIST network as\nwell as its wider and deeper variants.  I feel the main weakness is that the\nempirical evidence provided are not thorough and sufficient (only 1 base model\non 1 dataset). Since this paper is 10-page, I evaluate it at a higher standard\nand expect more convincing empirical results.\n\nQuestions and suggestions for improvements:\n\n1. How much time does it take to generate training examples? It seems to me\nthat it is a very costly process because obtaining the relative improvement (8)\nof splitting at each node can be quite expensive - basically, we need to split\nalmost every ambiguous neuron to get their improvement values, and in normal\nBaB we only need to split one each time. The paper mentioned it \"minimum 5%\ncoverage per layer\" but does not provide more details. \n\n2. Also how much time does it take for training the GNN? It seems the GNN has\nmany vertices - the same number as the number of neurons in a network, which\ncan be quite large.  If the dataset generation and training time are much\nlonger comparing to the BaB time, the usefulness of the proposed method can be\nlimited especially it does not necessarily generalize to foreign networks\n(networks with significantly different structure, or trained using different\nmethods).\n\n3, An ablation study for the fail-safe strategy is needed. Without the\nfail-safe strategy, is the GNN learned split better than other strong\nheuristics? If the fail-safe strategy is too strong, the improvement we see can\nprobably come from the fail-safe strategy mostly, and GNN might not do too much\nuseful things. This is an important study that should be part of this paper.\n\n4. It seems all networks in this work are trained using a single training\nmethod, Wong & Kolter, 2018.  Does the split heuristic learned by GNN works for\nnetworks trained using a different training strategy?  For example, interval\nbound propagation (IBP) based methods [1][2] which achieve the state-of-the-art\nresults.  Also, adversarial training with L1 regularization is also verifiable,\nas demonstrated in [3]. Running a few pretrained models by these methods should\nbe an easy experiment to add.\n\n5. There have been a few strong baselines in this field that the authors do not\ndiscuss and compare against, including [4][5][6]. They solve similar problems \nas in this paper and also provide promising results. At least, the authors should\ndiscuss them in related works, and it is strongly encouraged to add at least one \nof them as a stronger baseline.\n\n6. This paper claims that Neurify is theoretically incorrect (in Appendix D.2,\npage 17). I am quite surprised and not sure if this claim is true. I am not\naware of any firm evidence that Neurify is theoretically incorrect.  It is\nbetter to communicate with the authors of Wang et al., 2018 and make sure this\npaper is making a correct claim.\n\nGiven that the idea proposed by this paper is novel and interesting, I tend to\naccept this paper *under the condition* that the authors can conduct an\nablation study of the fail-safe strategy, provide generalization results on\nmodels trained using different robust training strategies, and provide results\non at least one more dataset (like ACAS Xu, or CIFAR). Adding at least one more\nbaseline is also strongly encouraged.\n\n** After author discussion, I have increased my score based on the new results\nprovided. The authors should make sure to include the ablation study results, and\na detailed discussion on training data generation time and training time in the\nfinal version of the paper.\n\n\n\n[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).\n\n[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)\n\n[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.\n\n[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.\n\n[5] Singh, G., Gehr, T., Püschel, M., & Vechev, M. (2018). Boosting Robustness Certification of Neural Networks.\n\n[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.\n", "extra_scores": {"experience_assessment": "I have published in this field for several years.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I carefully checked the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

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)