Towards Scalable Complete Verification of Relu Neural Networks via Dependency-based Branching

1 Introduction

While the accuracy of neural network classifiers has greatly improved in the past few years, concerns about their fragility and opacity have been raised. This hinders the application of machine learning in a variety of applications, including safety-critical systems, where error rates need to be shown to be small before deployment. The area of verification of neural networks has grown rapidly in the past 3 years in response of these concerns and aims to provide methods to verify automatically that a neural network meets its intended specifications. For example, robustness against adversarial attacks [Szegedy et al., 2014], or local robustness, i.e., the invariance of an image classifier against small image perturbations, is a property that is often studied, among others, in this area. Results from the verification step can be used in a process of certification to demonstrate that the classifier is robust; alternatively, if counterexamples are found these can be used to improve the model.

A key difficulty in the area is scalability. Simply put, the present methods, while effective on small models, cannot presently analyse the networks used in vision and other complex tasks. This is particularly evident in complete verification, where, in contrast to incomplete verification, a definite answer to the verification problem needs to be given. The main drawback of complete verification is the state space explosion problem whereby the ReLU space, i.e., the search space generated by the possible states of the ReLU nodes, grows exponentially in the number of ReLU nodes. This challenge is well recognised and constitutes the key objective for further research. This paper makes a contribution in this direction. In particular, we employ a notion of dependency between ReLU nodes as a heuristic to construct a MILPbased, branching approach that divides the original verification problem into a set of sub-problems whose ReLU space is smaller than the original one. In contrast to previous work in complete verification, the branching method that we devise directly aims at the reduction of the ReLU space. As we show in experiments on the ReLU-based fully-connected networks from the first competition for neural network verification (VNN-COMP) [VNN-COMP, 2020], this leads to 145% performance gains over the present state-of-the-art in complete verification.

The rest of the paper is organised as follows. After discussing related work in Section 2, in Section 3 we introduce the basic notions for the verification of neural networks that we use later in the paper. In Section 4 we present a dependency-based branching method for the MILP formulation of the verification problem. In Section 5 we report an experimental comparison of the method to the state-of-the-art in complete verification using the networks from VNN-COMP.

2 RelatedWork

Formal verification of neural networks comprises complete and incomplete methods. Complete methods can in principle return a definite answer as to whether the verification property is satisfied, whereas incomplete methods may be unable to decide whether the property is satisfied. Complete methods are based on MILP formulations [Botoeva et al., 2020; Bastani et al., 2016; Lomuscio and Maganti, 2017; Cheng et al., 2017; Fischetti and Jo, 2018; Tjeng et al., 2019], SMT encodings [Ehlers, 2017; Katz et al., 2017; Katz et al., 2019], and input refinement [Wang et al., 2018; P. Henriksen, 2020]. Incomplete methods are based on duality [Dvijotham et al., 2018; Wong and Kolter, 2018], linear approximations [Tran et al. et al., 2019; Weng et al., 2018; Tjandraatmadja et al., 2020] and semidefinite relaxations [Fazlyab et al., 2020; Dathathri et al., 2020]. While incomplete approaches differ, they all rely on approximations of the ReLU function. This often improves their scalability over complete methods but can also hinder their efficacy to solve the verification problem.

The present contribution uses and extends ideas from MILP encodings [Tjeng et al., 2019; Anderson et al., 2019; Botoeva et al., 2020] towards conquering scalability in complete verification. This is achieved by developing a novel divide-and-conquer method that branches on the states of the ReLU nodes. Branching methods of this kind were previously considered. Reluplex [Katz et al., 2017] implements a Simplex-type method which branches on a ReLU node whenever several pivot operations fail to resolve conflicts in the constraints representing the verification problem. In SATand MILP-based neural network verification [Ehlers, 2017; Cheng et al., 2017; Botoeva et al., 2020], branching is delegated to the underlying SAT and MILP solvers, though MILP-solvers are often instructed to prioritise branching for ReLU nodes in the early layers of the network. Branching is also considered in [Wang et al., 2018; R¨ossig and Petkovic, 2020], where the ReLU node to branch is selected on the basis the nodes' output gradients so as to tighten the output range of the network. A common theme among these works is that they do not target the reduction of the ReLU space, which is the key aim of the present contribution.

To accomplish this, our method exploits the structure of the networks on the basis of a notion of dependency between the ReLU nodes. Whilst the dependency analysis methods are extended from [Botoeva et al., 2020], the latter work delegates branching to the MILP solver, thereby offering no mechanism for selecting the ReLU node to branch, which is a key consideration of the present method. Also, whereas the efficacy of the cited method in reducing the ReLU space relies on the analysis of callback cuts by the underlying MILP solver, our method directly aims at the construction of simpler MILP encodings by "eliminating" some of the binary variables. As we experimentally show this is often more effective.

The dependency-based branching methods that we develop are also related to conflict analysis in MILP [Achterberg, 2007], which generalises SAT infeasibility analysis, and look-ahead based SAT solvers, which prioritise branching for variables that optimise a heuristic value [Biere et al., 2009]. However, these approaches are domain independent with no specificity in neural network verification. In particular, as we experimentally show by comparing with the state-of-the-art MILP-based verification tools, generic methods do not fully exploit the highly structured nature of neural networks and suffer frommarkedly lower scalability due to this fact.

3 Background

The paper extends previous work in MILP formulations [Anderson et al., 2019; Lomuscio and Maganti, 2017] and dependency analysis [Botoeva et al., 2020] for the formal verification of neural networks. This section summarises basic concepts and fixes the notation used later in the paper.

Feed-forward ReLU networks. A feed-forward neural network (FFNN) is a vector-valued function f : Rs0 → RsL that composes a sequence of L ≥ 1 layers, f (1) : Rs0 → Rs1 , . . . , f (L) : RsL-1 → RsL . Each layer f (i) is the composition of an affine transformation and a non-linear activation function. That is, f (i) (x(i-1) ) ≜ act(i) (W(i)x(i-1) +b(i) ), where: x(0) is the input to the network; x(i-1) is the output of the (i - 1)-th layer; act(i) is the activation function of the ith layer; z(i) = W(i)x(i-1) + b(i) is the affine transformation, also called pre-activation, of the i-the layer for a weight matrix W(i) ∈ Rsi×si-1 and a bias vector b(i) ∈ Rsi . A ReLU FFNN is a FFNN that contains only the Rectified Linear Unit (ReLU) activation function. The ReLU function is ReLU(z(i) ) ≜ max(0, z(i) ) where the maximum function is applied element-wise on z(i) . Each j-th element of layer f (i) is said to be the j-th ReLU node, or simply the j-th node, of the i-th layer; we sometimes write n (i) j to refer to the node. A node n (i) j is said to be in the active state if z(i) j ≥ 0 and in the inactive state if z(i) j < 0.

Verificationproblem. Given a FFNN f , a set of inputsX ⊂ Rs0 and a set of outputs Y ⊂ RsL , the verification problem is to answer whether

We write (f,X, Y) to denote an instance of the verification problem. Typically, X and Y are finite sets of polyhedra [Anderson et al., 2019; Wang et al., 2018; Katz et al., 2019; Tjeng et al., 2019]. In particular, in this work X is a box given by lower and upper bounds on the inputs nodes, i.e., X = {x(0) | l(0) j ≤ x(0) j ≤ u(0) j , 1 ≤ j ≤ s0, l(0) j ≤ u(0) j ∈ R}, and Y is a linear constraint on the network's outputs, i.e., Y = {x(L) | cT x(L) +c0 > 0}. Among the various instantiations of the verification problem, the local adversarial robustness problem is one of the most well studied. The problem is to establish whether all images within a norm-ball of a given image are classified equivalently by the network. We here consider the l∞ norm-ball. For a network f , an image x with class label c and a perturbation (norm-ball) radius ϵ, the local adversarial robustness problem can be solved by solving a verification problem (f,X, Yj) for each j with 1 ≤ j ≤ sL, j ̸= c, X = {x(0) | x - ϵ ≤ x(0) ≤ x + ϵ} and Yj = {x(L) | x(L) c -x(L) j > 0}. The answer to the problem is positive iff every (f , X , Yj) has a positive answer.

Bounds. Given a verification problem, we hereafter assume a lower bound l(i) j and an upper bound u(i) j for the pre-activation z(i) j of each node n (i) j . The bounds can be computed from X via bound propagation methods, see, e.g., [Singh et al., 2019; Wang et al., 2018; P. Henriksen, 2020]. A node n (i) j is said to be strictly active if l(i) j ≥ 0 and strictly inactive if u(i) j ≤ 0. A stable node is a node that is either strictly active or strictly inactive. An unstable node is a node that is neither strictly active nor strictly inactive.

MILP formulation of the verification problem. The verification problem can be recast into a mixed integer linear program (MILP). A MILP is an optimisation problem whereby a linear objective function over real-valued and integer variables is sought to be minimised subject to a set of linear constraints on its variables, see, e.g., [Papadimitriou and Steiglitz, 1998]. The MILP formulation of a verification problem (f,X, Y) is the following:

where 1 ≤ i ≤ L, 1 ≤ j ≤ si. The constraints (1c) model the ReLU function. In particular, each δ(i) j is a binary variable such that δ(i) j = 0 iff node n (i) j is inactive and δ(i) j = 1 iff node n (i) j is active. We say that a MILP is satisfied if its optimal value is above zero. The verification problem has a positive answer iff its associated MILP is satisfied.

ReLU space. We focus on the branch-and-bound (B&B) method [Land and Doig, 2010] to solve the MILP (1). A key step of B&B is the recursive splitting of the feasible region, i.e., the set of admissible solutions, of a MILP into smaller regions by branching on the values of the binary variables until a feasible solution is found; see, e.g., [Morrison et al., 2016] for a thorough description of B&B. The efficacy of B&B is therefore linked to the size of the search space generated by the binary variables. We refer to this space as the ReLU space; it is formally defined as the Cartesian product {0, 1}|∆| of the ground terms of all the binary variables ∆ ≜ {δ(i) j }i,j . The ReLU space induced by the MILP formulation (1) can be reduced by replacing the ReLU constraints for a node n (i) j with x(i) j = z(i) j if the node is strictly active and with x(i) j = 0 if the node is strictly inactive [Tjeng et al., 2019].

Dependency analysis. Dependency analysis [Botoeva et al., 2020] is a method to further reduce the ReLU space that needs to be considered during B&B. In dependency analysis, the state s (s ∈ {active, inactive}) of a node n (i) j depends on the state s′ (s′ ∈ {active, inactive}) of another node n (q) r if whenever (i.e., for any network input in X) the state of n (q) r is s′ , the state of n (i) j has to be s. The cited work identifies these dependencies during B&B, expresses them as MILP constraints and adds them to the MILP program being solved via callback cuts. Intuitively, each constraint determines the value of the binary variable associated with n (i) j whenever n (q) r is in state s′ (as per its binary variable), thereby reducing the ReLU space.

4 Dependency-based Branching

This section introduces a dependency-based branching procedure for the MILP formulation of the verification problem defined above. The procedure recursively divides the verification problem into pairs of sub-problems. The two subproblems are verification problems resulting from an originally unstable node being split and stabilised into the active and inactive state. Intuitively, the MILP formulations of the sub-problems are easier to solve as they contain fewer integrality constraints. Clearly, branching of this kind can be carried out exhaustively to generate sub-problems whose MILP formulations are linear programs that are generally easier to solve. However, the number of sub-problems grows exponentially in the number of unstable nodes, thereby rendering the exhaustive exploration of the ReLU space intractable for even small networks. In the light of this we develop a procedure that is parameterised on the branching depth, i.e., the depth of the tree obtained by recursively dividing the original problem. Once this depth is reached, all of the generated subproblems are solved. Since the sub-problems are obtained via branching on the states of the ReLU nodes, the original problem is satisfied iff all of the sub-problems are satisfied. At the heart of the procedure is the selection of the ReLU node to branch. The key idea of this work is to exploit the dependency relations of the network to determine the ReLU node that will bring about the most significant reduction of the ReLU space. In particular, at each branching step, the ReLU node with the most nodes depended on it is selected for branching. Accounting for these dependencies, not only the ReLU node selected for branching is stabilised but also the nodes that depend on it. This leads to a linear encoding of the nodes, which in turn leads to a reduced ReLU space.

4.1 Branching Procedure

The overall verification method is outlined in Algorithm 1. The method relies on the branching procedure to divide the given verification problem into a set of sub-problems. It then encodes the sub-problems into MILPs which can be solved in parallel. Finally, it answers yes to the original verification problem iff all the MILPs are satisfied.

The branching procedure comprises three steps. In the first step, a dependency graph for the network in question is built. The graph expresses which node depends on which node. In the second step, the ReLU node that has the most depended nodes is identified and selected for branching. In the third step, the verification problem is divided into two sub-problems: one where the selected node is stabilised into the active state and one where it is stabilised into the inactive state. In each sub-problem, all the nodes that depend on the branching node are stabilised into the state prescribed by the corresponding dependency. The procedure recursively carries out these steps until the required branching depth is reached.

We now give a detailed description of the steps of the branching procedure. In our presentation, we will use the network from Figure 1 to exemplify each of the steps. We begin with the construction of the dependency graph. This is a directed graph whose vertices represent node-state pairs and whose edges represent dependencies between said pairs.

Definition 1 (Dependency graph). Given a verification problem (f,X, Y) for which f comprises a set of unstable nodes U, the associated dependency graph of (f,X, Y) is a directed graph D = (V, E), where:

• V = U × {a, i} is the set of vertices, where a and i denote "active" and "inactive".
• E ⊆ V × V is the set of edges such that for every (n, s), (n′ , s′ ) ∈ V we have ((n, s), (n′ , s′ )) ∈ E iff

Algorithm 1 The verification procedure.

1: procedure VERIFY((f ,X, Y), bd) 2: Input: verification problem (f , X , Y), branching depth bd 3: Output: yes/no 4: sub-problems ← branch((f , X , Y), bd) 5: for P in sub-problems do 6: milp ← encode(P ) 7: sub-result ←milp solver(milp) 8: if sub-result is not satisfied then return no 9: return yes 10: procedure BRANCH((f ,X, Y), bd) 11: Input: verification problem (f , X , Y), branching depth bd 12: Output: a set of verification sub-problems 13: queue← [(f , 0)], sub-problems ← [] 14: while queue is not empty do 15: h, d ← pop top element of queue 16: if d ≤ bd then 17: D ← dependency graph(h) 18: n ← branching node(D) 19: h1(h2) ← stabilise h as per the active (inactive) dependency tree of n. 20: add (h1, d + 1) ((h2, d + 1)) to queue 21: else 22: add (h, X , Y) to sub-problems 23: return sub-problems

the s′ -state of node n′ depends on the s-state of node n.

Figure 2 shows the dependency graph of the network in the running example.

The construction of the dependency graph relies on the method from [Botoeva et al., 2020] to identify the dependencies between the nodes. The graph is built in time O(L · S2 ) · S2 ), where S is the maximum number of nodes in a layer, L is the number of layers, O(L · S2 ) is the bound on the number of edges in the graph, and O(S2 ) is the cost of identifying a dependency [Botoeva et al., 2020].

With the construction of the dependency graph, the ReLU node with the highest dependency degree is heuristically selected for branching. The dependency degree of a node expresses the total number of nodes that depend on it. Concretely, it equals the sum of the number of vertices in the active and inactive dependency tree of the node, where the active (inactive, respectively) dependency tree of the node is the spanning tree of the vertices reached during depth-firstsearch from the vertex associated with the active (inactive, respectively) state of the node in question. Formally, we have:

Definition 2 (Dependency degree). Given a dependency graph D, the dependency degree of a ReLU node n equals

Figure 2 highlights the active and inactive dependency trees of node n (1) 2 . From these we can compute the dependency degree of the node as 6.

The highest the dependency degree of the node selected for branching, the fewer the required binary variables to encode the resulting sub-problems.

Note that if the active (inactive, respectively) dependency tree of the selected node contains at least one pair of vertices of the form (n, a) and (n, i), then the sub-problem corresponding to the node being active (inactive, respectively) is discarded. This is because the MILP formulation of the sub-problem does not have any feasible solution.

The computation of the size of the dependency trees of the nodes takes time O(L2 · S3 ) via DFS. So, accounting for the O((L·S2 )·S2 ) cost of constructing the dependency graph, the identification of the node to split takes time O(L·S3 ·(L+S)). Therefore, for a branching depth bd, the cost of the branching procedure is O(2bd · L · S3 · (L+S)).

The above concludes the description of the branching procedure. Next, we define the MILP encodings of the subproblems generated by the procedure.

Definition 3 (MILP formulation). Given the dependency trees T1, . . . , Tl of the ReLU nodes so far selected for branching, the MILP formulation of a sub-problem (f , X , Y) is given as formulation (1), but replacing the ReLU constraints (1c) of each node n (i) j with either one of the following:

• (i) if either l(i) j ≥ 0 or (n (i) j , a) is a vertex of some dependency tree, then x(i) j = z(i) j .
• (ii) if either ˆubranch n (i ) j ≤ 0 or (n (i) j , i) is a non-root vertex of some dependency tree, then x(i) j = 0.

Clause (i) corresponds to the node being active, either because the lower bound of the node is above zero or because this is entailed by a dependency constraint. Analogously, clauses (ii) and (iii) correspond to the node being inactive. The two clauses distinguish between vertex (n (i) j , i) being a root of a dependency tree and not. In the former case, the formulation includes the constraint z(i) j ≤ 0 so as to disallow for spurious solutions whereby z(i) j > 0 and x(i) j = 0. In the latter case, said constraint is not required since (n (i) j , i) is in the dependency tree of a node selected for branching; therefore, the pre-activation of n (i) j is guaranteed to be below zero. Finally, clause (iv) corresponds to the standard MILP formulation for unstable nodes (see Section 3).

The above concludes the description of the verification procedure. The procedure is sound, i.e., it assesses a given network to be safe only when the network is safe. The procedure is also complete, i.e., it can in principle (given enough time) assess the safety of all networks that are safe.

Theorem 1 (Soundness and completeness). Given a verification problem (f,X, Y), the procedure VERIFY((f,X, Y)) from Algorithm 1 returns yes iff ∀x ∈ X : f (x) ∈ Y.

Proof. The proof is by straightforward induction on the branching depth.

4.2 Optimisations

It is known that verifying neural networks is NPcomplete [Katz et al., 2017]. Constructing the dependency graph has only quadratic complexity. However, to improve the scalability of the approach, we devise two further optimisation methods.

Iterative branching. To reduce the overhead of the branching procedure, we consider a variant of the procedure where several splits are executed on the basis of the same dependency graph, as opposed to building a dependency graph for each split. Once there are no nodes suitable for branching (i.e., they have no dependencies with other nodes), the procedure re-computes the bounds for the nodes by taking into account the new bounds for the stabilised nodes. On the basis of these bounds it builds a new dependency graph which it uses to further divide the verification problem. While iterative branching does not guarantee that the ReLU node with the highest dependency degree is always selected for branching, it enhances the performance of the overall verification method as we experimentally show in Section 5.

Branch monitor. Whilst dependency-based branching improves the overall verification times (see Section 5), dependency-based branching for MILPs that are already easy to solve using B&B may be disadvantageous to solving the original problem without any (dependency-based) branching. A commonly used indicator of the hardness of MILP programs is the node throughput in B&B [Klotz and Newman, 2013]. In view of this, our verification procedure formulates the original verification problem as a MILP and uses the node throughput to determine whether to initiate branching or not. In particular, the procedure is parameterised with a threshold on the number of B&B nodes, i.e, the nodes in the B&B tree, to be explored by B&B before the branching procedure is initiated (from the root B&B node). The threshold takes high values for MILPs whose B&B nodes are easy to analyse and low values for MILPs whose B&B nodes are hard to analyse.

5 Evaluation

We evaluate the verification procedure introduced above and present a comparison with the state-of-the-art in complete methods. The procedure is implemented in Venus2 1 , a Python toolkit that is based on Venus [Botoeva et al., 2020]. The experimental comparisons focus on the leading and publicly available complete verification tools: Eran (deeppoly) [Singh et al., 2019], Marabou [Katz et al., 2019], MIPVerify [Tjeng et al., 2019], Neurify [Wang et al., 2018], Nnenum [S. Bak et al., 2020], Verinet [P. Henriksen, 2020] and Venus [Botoeva et al., 2020]. The comparisons are drawn on all of the benchmarks for fully connected ReLU FFNNs from VNN-COMP:

• ACASXU [Julian et al., 2016] is a collection of 45 ReLU FFNNs which were developed as part of an airborne collision avoidance system to advise horizontal steering decisions for unmanned aircraft. Each network has 5 inputs, 300 ReLU nodes arranged in 6 layers with 50 neurons each and 5 outputs. We verify the networks against the safety specifications from [Katz et al., 2017]. These include four properties that are checked on all of the 45 networks and 6 properties that are checked on a single network. We therefore consider a total of 186 verification problems.
• MNIST [LeCun et al., 1998] is a dataset comprising images of hand-written digits 0-9, each formatted as 28x28x1-pixel grayscale image. We use three fully connected ReLU FFNNs trained on the dataset: MNIST2, MNIST4 and MNIST6. The networks comprise 2, 4 and 6 layers, respectively. Each layer of each of the networks has 256 ReLU nodes. We verify the networks against the local adversarial robustness property w.r.t 25 correctly classified images and perturbation radii of 0.02 and 0.05. We therefore consider a total of 150 verification problems.

All the experiments were carried out on an Intel Core i77700K (4 cores) equipped with 16GB RAM, running Linux kernel 4.15; the ablation experiment on the branching depth (see below) was carried out on an Intel Core i9-9900X (20 cores) equipped with 125GB RAM, running Linux kernel 5.3.

1 Venus2 is available at https://github.com/vas-group-imperial/ venus2.

Each verification problem was run for a timeout of 30 minutes. All MILP-based tools (Venus2, Eran, MIPVerify, Venus) rely on Gurobi 9.2 for the MILP backend. Venus2 was run with the branching depth set to 4 for MNIST2 and MNIST4 and to 7 for ACASXU and MNIST6. The B&B node threshold was set to 500 for ACASXU and MNIST6, to 5000 for MNIST4 and to 10000 for MNIST2.

Table 1 reports the experimental results 2 . Venus2 outperformed all of the tools by verifying more problems and by being faster on average. In particular, Venus2 solved 13% more problems and had a 145% faster average solve time than the second best performing tool Nnenum.

Venus2 was only outperformed on the ACASXU benchmark only by Nnenum. Also, as can be observed from Figure 3, Nnenum and Verinet were able to solve more MNIST verification problems under 100 seconds than Venus2 was able to solve within the same time. The latter two observations indicate an overhead in the construction of the dependency graphs and the MILP encodings for verification problems that the current state-of-the-art can solve in under 100 seconds. For harder problems Venus2 consistently outperforms all of the tools. This is particularly evident in MNIST4 and MNIST6 and the more challenging perturbation radius of 0.05. For these benchmarks significant branching on the ReLU nodes is required to solve the verification problems, as opposed to the 0.02 perturbation radius where the tighter bounds for the nodes can often be used to solve the verification problem without any branching.

2 Note that the comparative performance of the tools is not always in agreement with the one reported in VNN-COMP. This is because the participants in the competition used different machines with different specifications for the execution of the experiments.

We now proceed to evaluate the parameters and optimisations of Venus2 by documenting the variability of the tool's performance under different operational settings.

We begin with benchmarking Venus2 with iterative branching turned off. Table 2 reports the results obtained on the MNIST models and the 0.05 perturbation radius. Whilst iterative branching does not always select the ReLU node with the highest dependency degree for branching, the results show that the gains obtained from reducing the number of dependency graphs constructed outweigh the occasional nonoptimal selection of the node to branch.

Still, the dependency-based branching heuristic is crucial to Venus2's performance: as Table 2 shows, the heuristic is consistently superior to random branching, e.g., it is 82.49% faster for the MNIST6 model and the 0.05 radius.

Also, whilst parallelisation definitely contributes to Venus2's performance, the simplified MILP encodings from dependency-based branching is an additional contributing factor. In particular, even though Venus2's performance degrades to half its speed when run on a single thread (see Table 2), it still outperforms the baseline tool Venus when run on multiple threads by verifying markedly more images.

Finally, we evaluate the sensitivity of Venus2 to the B&B node threshold and the branching depth parameters. For the study of the former, we use the MNIST6 model and the 0.02 radius since the benchmark contains a mixture of easy and hard verification problems. For the study of the latter, we use the MNIST4 model and the 0.05 radius since the benchmark mainly comprises hard problems for which Venus2 initiates dependency-based branching.

Figure 4 summarises the results. We observe that Venus2

performs best for intermediate values of the B&B node threshold. Intuitively, the branch monitor aims at initiating dependency-based branching only for problems that are hard to solve via B&B. Under this light, low values for the parameter are problematic as they induce the overhead of dependency-based branching for problems that can easily be solved via B&B. Analogously, high values are also problematic as they delay the execution of dependency-based branching for problems that are harder to solve.

We similarly observe that Venus2 performs best for intermediate values of the branching depth parameter. Intuitively, intermediate values for the parameter are more effective as dependency-based branching is executed w.r.t ReLU nodes with high dependency degrees, as opposed to lower values which debilitate the effective execution of dependency-based branching and larger values which encourage branching on nodes with lower dependency degrees.

6 Conclusions

In this paper we introduced a novel verification method for ReLU-based neural networks. The key idea upon which the method is developed is that branching on nodes whose stabilisation forces the stabilisation of other nodes enables the analysis of the verification problem under stronger MILP formulations. Doing this requires the analysis of the dependency relations of the ReLU nodes, so that the nodes whose splitting induces the greatest reduction of the ReLU space can be heuristically determined. The experimental results showed 145% performance gains for the fully connected networks from the first competition for neural network verification, thereby indicating a step towards more scalable complete neural network verification.

Acknowledgements

This work is partly funded by DARPA under the Assured Autonomy programme (FA8750-18-C-0095). A. Lomuscio is supported by a Royal Academy of Engineering Chair in Emerging Technologies.