The area of verification of neural networks (NNs) is concerned with the development of methods and tools to establish whether a given NN satisfies a given specification on a given input (Li et al. 2020;Liu et al. 2020). If a NN model is verified to be robust, no adversarial attack exists for the model, input and perturbation under analysis (Goodfellow, Shlens, and Szegedy 2014). NN verification has been used in many areas including safety-critical systems (Tran et al. 2020;Julian and Kochenderfer 2021;Kouvaros et al. 2021;Manzanas Lopez et al. 2021).
One type of NN verification methods is the complete approach which guarantees no false negatives or false positives are generated. Existing complete approaches for NN verification build on mixed-integer linear programming (MILP) (Bastani et al. 2016;Lomuscio and Maganti 2017;Tjeng, Xiao, and Tedrake 2019;Anderson et al. 2020;Botoeva et al. 2020) or satisfiability modulo theories (Ehlers 2017;Katz et al. 2021). These complete verifiers can guarantee to resolve any verification query but often come at a high computational cost, thus not scaling well to large-scale NNs.
Another type of verification methods is the incomplete approach that involves overapproximations of the NN and has a better scalability to larger NNs than the complete approach. The existing incomplete verifiers involve abstraction and approximation via linear approximations (Henriksen and Lomuscio 2020, 2021; Wang et al. 2021;Hashemi, Kouvaros, and Lomuscio 2021) or convex approximation (Xu et al. 2020;Dvijotham et al. 2018;Wong and Kolter 2018;Chen et al. 2021;Raghunathan, Steinhardt, and Liang 2018;Fazlyab, Morari, and Pappas 2022;Batten et al. 2021). Some incomplete verifiers can offer completeness guarantees by combining symbolic interval propagation or convex relaxation with input refinement (e.g., ReluVal (Wang et al. 2018c)) or neuron refinement (e.g., Neurify (Wang et al. 2018a), VeriNet (Henriksen and Lomuscio 2020), DEEPSPLIT (Henriksen and Lomuscio 2021), β-CROWN (Wang et al. 2021) and OSIP (Hashemi, Kouvaros, and Lomuscio 2021)), but requiring a very large numbers of splitting refinements.
This paper focuses on the incomplete approach. The success of incomplete methods hinges on the tightness of the approximations generated by the technique, because a looser approximation leads to more unsolvable verification queries and a lower scalability capability. The triangle relaxation (Ehlers 2017) offers the tightest possible convex approximation for a single Rectified Linear Unit (ReLU) neuron and has been used for faster bound propagations (Weng et al. 2018;Singh et al. 2019a;Tjandraatmadja et al. 2020;Müller et al. 2021). These incomplete methods are based on polynomial-time solvable linear program (LP) problems and can achieve state-of-the-art (SoA) performance. However, their efficacy is fundamentally limited by the tightness of convex relaxations. This is known as the "convex relaxation barrier" indicating that even optimal convex relaxations on a single neuron fail to obtain tight approximation of the overall model (Salman et al. 2019). This problem can be approached in two ways. The first is applying convex relaxations to multiple neurons. The representative methods include DeepPoly (Singh et al. 2019a), kPoly (Singh et al. 2019b), OptC2V (Tjandraatmadja et al. 2020), and PRIMA (Müller et al. 2021). The second is using stronger relaxations, among which the most promising ones achieving tightness and efficiency are based on semidefinite program (SDP) (Raghunathan, Steinhardt, and Liang 2018;Fazlyab, Morari, and Pappas 2022;Batten et al. 2021).
Empirically, the standard SDP relaxation (Raghunathan,
The Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI-23)
Steinhardt, and Liang 2018) is considerably tighter than the standard LP relaxations. However, as illustrated in (Zhang 2020), SDP relaxations become loose for multiple hidden layers. Linear cuts (Batten et al. 2021) or nonconvex cuts (Ma and Sojoudi 2020) were introduced to further tighten SDP relaxations. The standard SDP approaches (Raghunathan, Steinhardt, and Liang 2018;Zhang 2020;Ma and Sojoudi 2020) achieve tighter relaxations than LPs, but incur a considerable extra computational effort, making them not scalable to larger models. To alleviate the computational cost, a memory-efficient first-order algorithm was introduced in (Dathathri et al. 2020). With the same aim, layerwise SDP relaxations were used in (Batten et al. 2021;Newton and Papachristodoulou 2021) by exploiting the cascaded NN structures based on chordal graph decomposition (Zheng, Fantuzzi, and Papachristodoulou 2021). To the best of our knowledge, the LayerSDP method (Batten et al. 2021) achieves the tightest relaxations by combining SDP relaxation with triangle relaxation (Ehlers 2017). Even so, it is observed in (Batten et al. 2021) that the relaxation gap of LayerSDP is still considerable in large networks. This leads to an increased false negative rate as the model size grows and thus limits applicability of the approach.
In this paper, we advance the SDP approach for NN verification with a new relaxation and an efficient algorithm to solve it. The relaxation we propose combines the LayerSDP method (Batten et al. 2021) with a set of valid nonlinear constraints, which gives a provably tighter relaxation than the SoA SDP methods. The inclusion of nonlinear constraints results in a non-convex SDP problem that is generally harder to solve than LayerSDP. We further develop an iterative algorithm to obtain the optimal solution of the non-convex SDP problem. The algorithm initialises from the LayerSDP solution and solves iteratively an auxiliary convex SDP problem. The auxiliary SDP problem is derived from the original non-convex SDP problem and its size is around the same as LayerSDP. Our theoretical analysis shows that the solution sequence produced by the iterative algorithm is tighter than the SoA SDP methods, and can converge to the optimal solution of the non-convex SDP problem. The experiments on various standard benchmarks confirm that the proposed SDP method is considerably tighter than the present SoA, whilst having competitive efficiency. Our previous work (Lan, Zheng, and Lomuscio 2022) constructed effective linear cuts using the linear reformulation technique (RLT) and added them to LayerSDP (Batten et al. 2021) to produce a tighter solution. These RLT-based linear cuts can be directly added to the SDP problems solved in this paper, meaning that the method proposed in this paper always gives a provably tighter solution than the method in (Lan, Zheng, and Lomuscio 2022).
We use the symbol R n to denote the n-dimensional Euclidean space, ∥ • ∥ ∞ to denote the standard ℓ ∞ norm, and I b to denote a sequence of non-zero integers from 0 to b. We use diag(X) to stack the main diagonals of matrix X as a column, and ⊙ to refer to the element-wise product. We use 0 n×m to denote a n × m zero matrix and 1 n to denote a n × 1 vector of ones. We use P i [z] to represent the elements of matrix P i corresponding to the vector or matrix z.
We focus on feed-forward ReLU NNs. A network f : R n0 → R n L+1 with L hidden layers, n 0 inputs and n L+1 outputs is defined as follows:
, where x 0 is the input, f (x 0 ) is the output, xi+1 ∈ R ni+1 is the pre-activation vector, x i+1 ∈ R ni+1 is the post-activation vector, W i ∈ R ni+1×ni is the weight and b i ∈ R ni+1 is the bias. We focus on classification NNs whereby an input x 0 is assigned to the class j ⋆ whose corresponding output has the highest value: j ⋆ = arg max j=1,2,...,n L+1 f (x 0 ) j .
This paper contributes to solving the local robustness verification problem. Given a NN f and a clean input x under the ℓ ∞ -norm perturbation ϵ, the local robustness problem concerns determining whether f is robust on x, i.e., whether f (x 0 ) j ⋆ -f (x 0 ) j > 0 holds for all j = 1, 2, . . . , n L+1 with j ̸ = j ⋆ , and for all x 0 satisfying ∥x 0 -x∥ ∞ ≤ ϵ. This verification problem can be formulated and solved as an optimisation problem (Raghunathan, Steinhardt, and Liang 2018;Batten et al. 2021):
where
and l i+1 and u i+1 are the lower and upper activation vector bounds that can be computed by using bound propagation methods (Henriksen and Lomuscio 2020;Wang et al. 2018b). Without loss of generality, we assume that the considered verification problem is feasible. We solve the problem (1) for every potential adversarial target j = 1, 2, . . . , n L+1 , where j ̸ = j ⋆ , to obtain the optimal objective value γ * . If γ * > 0 in all the cases, the NN is verified to be robust on the input x under the adversarial input x 0 . Since the ReLU constraints in (1a) are nonlinear, the optimisation problem (1) is non-convex and in general hard to solve. A promising direction is converting problem (1) into a convex relaxation problem that can be efficiently solved. Solving the convex relaxation gives an optimal value γ * cvx that is a valid lower bound to γ * , i.e., γ * ≥ γ * cvx . When γ * cvx > 0, then γ * > 0 always holds and the input is robust. Clearly, a tighter convex relaxation (i.e., with a smaller relaxation gap γ * -γ * cvx ) increases the number of verification queries that can be solved. Tightness is thus the key design objective of a convex relaxation method given that its computational cost is acceptable.
The LP relaxation (Ehlers 2017) is a widely used convex relaxation method in the literature. Its key idea is using a triangle relaxation to approximate each ReLU constraint in (1a) with a convex hull:
where
The vectors ûi+1 and li+1 are the upper and lower bounds of the pre-activation vector xi+1 , respectively. Replacing the nonlinear constraint (1a) with the linear constraints in (2) leads to an LP relaxation to the non-convex optimisation problem (1). The LP is relatively easy to solve, but there is usually a large relaxation gap for many NNs, known as the convex relaxation barrier in (Salman et al. 2019). This paper aims to develop a tighter convex relaxation method based on semidefinite program (SDP) (Parrilo 2000;Lasserre 2009).
Non-convex Enhancement
In this section we describe a few SDP relaxations to the nonconvex optimisation problem (1), including the existing SDP methods and our new non-convex SDP relaxation.
Convex SDP Relaxations. The starting point is to observe that the nonlinear ReLU constraints in (1a) can equivalently be replaced by the set of linear and quadratic constraints:
Given a verification instance, we can know the strictly active neurons at each layer. If the j-th neuron, 1 ≤ j ≤ n i+1 , at layer i + 1 is strictly active, then for this neuron the set of constraints in (3) can equivalently be replaced by a single linear equality constraint x i+1 (j) = W i (j, :
The input constraints in ( 1b) and (1c) can also be reformulated as the quadratic constraints:
where l 0 = x -ϵ1 n0 and u 0 = x + ϵ1 n0 .
The techniques of polynomial lifting (Parrilo 2000;Lasserre 2009) can be used to reformulate the quadratic constraints in (3) and (4) as linear constraints in terms of new variables. Specifically, to couple all the ReLU constraints of the network together, we define a single positive semidefinite (PSD) matrix P as:
. By using (5), the constraints (3) and ( 4) can be reformulated as linear constraints of P . This idea was first utilised for NN verification in (Raghunathan, Steinhardt, and Liang 2018). Dropping the rank-one constraint on P results in a global SDP relaxation to the non-convex optimisation problem (1), with a potentially smaller relaxation gap than the LP relaxation, as empirically observed in (Raghunathan, Steinhardt, and Liang 2018). However, the global SDP relaxation is very computationally expensive for large NNs due to high dimensionality of P , thus limiting applicability of the approach.
Thanks to the inherent cascading structure of feedforward NNs, the activation vector of layer i + 1 depends only on its preceding layer i, for all i ≥ 0. We can exploit this cascading structure to derive a layer-based SDP relaxation with a set of PSD matrices that are of smaller sizes than the matrix P . The layer-based PSD matrices are defined as:
with
. By using (6), we reformulate (3) and (4) as a set of linear constraints on the elements of P i :
where xi+1 = [1, x T i+1 ] T . The constraint (7e) ensures inputoutput consistency (Batten et al. 2021) and ( 7f) is equivalent to (6) as shown in (Horn and Johnson 2012).
By replacing ( 3) and ( 4) with ( 7) and dropping the rankone constraint rank(P i ) = 1, the non-convex problem ( 1) is relaxed to a convex layer SDP (Batten et al. 2021): 7b), ( 7c), ( 7d), (7e), (8a)
where (8c) is reformulated from the last inequality in (2) with
As shown in (Batten et al. 2021), the layer SDP relaxation (8) is considerably easier to solve than the global SDP relaxation (Raghunathan, Steinhardt, and Liang 2018) and is also tighter, i.e., γ * GlobalSDP ≤ γ * LayerSDP ≤ γ * , by introducing the linear cut (8c). However, due to dropping the rank-one constraint, the relaxation gap of layer SDP is still considerable in large NNs, thereby limiting the scalability and applicability of the approach.
Non-convex Layer-based SDP Relaxation. A promising way to reduce the SDP relaxation gap is introducing constraints (or cuts) to enforce the rank conditions in (7f). Nonconvex cuts in the form of
are introduced in (Ma and Sojoudi 2020) to tighten the global SDP relaxation (Raghunathan, Steinhardt, and Liang 2018). The resulting non-convex SDP is solved via successively generating large numbers of linear cuts to approximate the nonconvex cuts. This method has limited scalability due to the underlying computationally demanding global SDP and the additional large number of linear cuts.
To alleviate the computational challenge, we take inspirations from recent advances on SDP relaxation for nonconvex QCQP (quadratically constrained quadratic program). In particular, a single nonlinear constraint in the form of c T (P -xx T )c = 0 is used for generic SDP relaxations in (Luo, Bai, and Peng 2019). This constraint must use the same vector c as the objective function, which limits its capability in reducing the relaxation gap (Ma and Sojoudi 2020). The method is thus undesirable for NN verification, because the vector c only has very few non-zero elements associated with the last hidden layer. Regarding the layer SDP relaxation (8), the vector c is only associated with the last PSD matrix P L-1 . A direct adoption of the nonlinear constraint in (Luo, Bai, and Peng 2019) to (8) will then only be able to enforce the rank condition of P L-1 .
We propose a new type of nonlinear constraints that allows using a set of vectors to enforce the rank conditions of all PSD matrices P i , i ∈ I L-1 , by exploiting the NN activation pattern, which will be explained in detail in the next section. In particular, we introduce a nonlinear constraint to each P i in ( 8) and obtain the novel layer SDP relaxation: 8b), ( 8c), (9a)
, are verification instance based constant vectors to be constructed (see Algorithm 1). Hereby we explicitly write the vector x i (referring to the elements in the first column of P i , i.e., P i [x i ]) to ease the analysis.
The introduction of the constraints in (9b) results in a tighter SDP relaxation, as shown in Theorem 1. Theorem 1. Given a feasible verification instance, we have
Intuitively, the relations in Theorem 1 hold because we add the extra valid constraints in (9b) into the layer SDP relaxation (8). Due to the nonlinear constraint (9b), the new layer SDP relaxation (9) is non-convex and harder to solve than the original layer SDP relaxation (8). Our main technical contribution is to circumvent the non-convexity issue by developing an iterative algorithm. This iterative algorithm, detailed in the next section, recursively solves a convex SDP problem of around the same size as (8). The algorithm is able to generate an objective value that initialises from γ * LayerSDP and converges to γ * ncvxSDP for v i constructed in Algorithm 1.
This section describes an iterative algorithm to compute the optimal solution of the non-convex layer SDP relaxation (9) at moderate computational cost. We first formulate an auxiliary convex layer SDP, then use it to develop an iterative algorithm and apply it to the NN verification problem.
Auxiliary SDP Problem. Although the non-convex layer SDP relaxation ( 9) is generally hard to solve, its optimal objective value γ * ncvxSDP is bounded below by γ * LayerSDP , as shown in Theorem 1. This lower bound can be efficiently solved from the convex layer SDP relaxation (8). Hence, we can use γ * LayerSDP as a start point to search for the value of γ * ncvxSDP . This inspires us to generate an objective value sequence {γ (k) iter } by solving an auxiliary convex SDP problem recursively. Our aim is to generate the objective value sequence that is bounded by γ
iter ≤ γ * ncvxSDP and can converge to γ * ncvxSDP . We want to ensure these bounds so that γ (k) iter is always tighter than γ * LayerSDP and remains as a valid lower bound to γ * . By having these properties, the sequence {γ (k) iter } can then be used for NN verification. The above analysis motivates us to consider the auxiliary SDP problem in the form of:
subject to (8a), (8b), (8c), (10a)
where
The weight α is a user-specified positive constant. Its value is set as α > 1 to penalise more on the SDP relaxations of the first L -1 layers. This is useful to obtain a tighter NN output, as it is influenced by the SDP relaxations of the first L -1 layers. δ i , i ∈ I L-2 , are user-given scalars. v i , i ∈ I L-1 , are constant vectors to be constructed in Algorithm 1 and δ L-1 is a constant scalar to be constructed in Algorithm 2. They are constructed such that the constraints in (10b) and (10c) are always satisfied for any feasible solution to the non-convex layer SDP problem (9). It thus enables us to solve the auxiliary SDP problem to obtain a valid lower bound of γ * ncvxSDP . We construct the vector set {v i } L-1 i=0 from Algorithm 1 by using the strictly active neurons of the NN (whose input and output are equal), which generally exist for each test input. By doing so, we know (10b) and v T L-1 x L-1 = c T P L-1 [x L ] are always satisfied. Hence, we can solve the auxiliary SDP (10) to obtain v T L-1 x L-1 and thus the objective value γ iter = v T L-1 x L-1 + c 0 = c T P L-1 [x L ] + c 0 . We further show that solving this auxiliary SDP can obtain γ iter = γ * ncvxSDP , based on Proposition 2. Proposition 2. By constructing the set {v i } L-1 i=0 from Algorithm 1, the optimal objective value of the auxiliary SDP problem (10) has the properties: 1) γ * auxSDP ≥ 0 for any constructed δ L-1 that satisfies (10c). 2) γ * auxSDP = 0 if and only if the optimal solution satisfies v
ncvxSDP , then solving the problem (10) gives the objective value
To achieve this, we propose an algorithm to iteratively update the value of δ L-1 and generate the objective value sequence {γ (k) iter } that converges to γ * ncvxSDP . Iterative Algorithm and Application to NN Verification. The iterative algorithm is based on solving the problem (10) at each iteration with the scalar δ L-1 that is changed with the Algorithm 1: Constructing the set of vectors
for j = 1, 2, . . . , n i+1 do 5:
if li+1 (j) ≥ 0 then 6:
end for 9:
if i ≤ L -2 then 10:
11:
else 12:
13:
end if 14: end for 15: Output:
iterations. The proposed iterative algorithm is summarised in Algorithm 2. The initial value of δ L-1 is set as δ
(1)
LayerSDP -c 0 , where γ * LayerSDP is the optimal objective value of the layer SDP relaxation (8). For each given δ (k) L-1 , the auxiliary SDP problem ( 10) is solved to obtain the objective value γ (k) iter . At each iteration, the obtained optimal objective γ * (k) auxSDP of problem ( 10) is used to update the value of δ L-1 .
The iteration is terminated when γ * (k) auxSDP is smaller than a prescribed tolerance ε ≥ 0. Algorithm 2 outputs the objective value γ (k0) iter for robustness verification of NNs. To apply Algorithm 2 to the problem of robustness verification, we first need to ensure that:
1) γ
iter is always a valid lower bound to γ * . 2) The sequence {γ (k) iter } converges to γ * ncvxSDP . The first item is concerned with soundness of the algorithm, i.e., whether γ (k) iter > 0 implies that γ * > 0 and the input is robust. The second item concerns the tightness of the algorithm, i.e., whether the sequence {γ
auxSDP can be used to check when the sequence {δ (k) L-1 } converges. This confirms the appropriateness of using γ * (k) auxSDP ≤ ε as the stopping criterion in Algorithm 2. We now proceed to analyse the properties of Algorithm 2: Proposed iterative algorithm 1: Input: NN parameters, {δ i } L-2 i=0 , α and ε. 2: Initialise: Construct {v i } L-1 i=0 using Algorithm 1. Solve γ * LayerSDP from (8). Set δ
(1)
auxSDP and x
auxSDP ≤ ε 7: Output: γ L-1 x L-1 under the parameter δ L-1 . Consider Algorithm 2, we know that:
Given the above, we can now state the soundness and tightness of Algorithm 2 in Theorem 5. Theorem 5. Given a feasible verification instance, the objective value sequence {γ Proof. By using Lemma 3 and the first property of Proposition 4, we know that the sequence {γ
iter } is monotonically increasing. By further using the second property of Proposition 4, we know that the sequence {γ
iter ≤ γ * ncvxSDP . By construction and using (10c), we also know that {γ
The convergence proof follows directly from that of Lemma 3 by replacing δ
Theorem 5 shows that Algorithm 2 achieves an objective value sequence {γ (k) iter } that is always a valid lower bound to γ * ncvxSDP and γ * . Also, the objective values at all iterations are not worse than γ * LayerSDP and converge to γ * ncvxSDP in finite iterations. The finite-time convergence has been empirically observed, but how to derive an analytic upper bound for the maximal iterations is still an open question. The above analysis shows that the proposed iterative algorithm is efficient to solve the non-convex layer SDP problem (9), which would otherwise be hard to solve directly. We now show the application of Algorithm 2 to NN verification (see Figure 1). In the picture the output "Verified robust" means that the instance studied is robust against the adversarial input, while the output "Undefined" represents the situation in which robustness cannot be determined. The iteration is executed only when γ * LayerSDP ≤ 0, i.e., the layer SDP is unable to resolve the robustness query. As we show later, this approach reduces the computational cost, as the layer SDP approach can already verify a considerable number of instances. Also, it is clear that the use of our iterative algorithm can increase the number of instances that can be verified. In practice, the iteration is terminated whenever γ
auxSDP ≤ ε is not reached yet. Computational Complexity. The computational cost in the method stems from solving the auxiliary SDP (10). This auxiliary SDP and the existing layer SDP (Batten et al. 2021) and global SDP (Raghunathan, Steinhardt, and Liang 2018) are all solved using the solver MOSEK (Andersen and Andersen 2000) which implements an interior-point algorithm. Before calling MOSEK, the SDP problem is reformulated as the widely-used conic optimisation form where inequality constraints are converted into equalities (Sturm 1999). As shown in (Nesterov 2003), solving a standard SDP at each iteration of the interior-point algorithm requires O(n 3 m + n 2 m 2 + m 3 ) time and O(n 2 + m 2 ) memory, where n is the size of the largest semidefinite constraint and m is the number of equality constraints. For the global SDP, n = 1 + L-1 i=0 n i which is the sum of all layer dimensions. For the layer SDP and the auxiliary SDP (10), n = 1 + max i=0,...,L-1 (n i + n i+1 ) which is the largest size of P i and it can be significantly smaller than that in the global SDP. As demonstrated in (Batten et al. 2021, Proposition 2), it is always beneficial to remove the dead neurons in any verification instance before formulating the SDP. The layer SDP and the auxiliary SDP can increase the number of equality constraints and may offset the benefits of smaller semidefinite constraints; see (Batten et al. 2021, Remark 1).
Settings. We conducted experiments on a Linux machine with an AMD Ryzen Threadripper 3970X 32-Core CPU, 256 GB RAM and a RTX 3090 GPU. The optimisation problems were modelled using the toolbox YALMIP (Lofberg 2004) and solved using the SDP solver MOSEK. We used δ i = 1, i ∈ I L-2 , α = 1.0e5 and ε = 0 to run Algorithm 2.
Networks. We evaluated on several feed-forward ReLU NNs trained on the MNIST dataset (LeCun 1998) and CI- Results. All experiments were run on the first 100 images of the datasets. We received the permission to run VeriNet (Henriksen and Lomuscio 2020) for obtaining the activation bounds of all benchmarks. We report the verified robustness (percentage of images verified to be robust) and runtime (average solver time for verifying an image) for each method.
Figure 2 shows the results of MLP-3 × 50 under various ϵ and methods IterSDP, LP, SDP-IP and LayerSDP. Our method IterSDP outperforms the baselines across all ϵ, confirming the statement in Theorem 5. Notably, IterSDP improves the verified robustness up to the PGD bounds for several ϵ. IterSDP requires more runtime (about twice) when compared to LayerSDP, but it is still faster than SDP-IP. This is expected since Algorithm 2 uses LayerSDP to initialise and solves the auxiliary SDP (10) whose size is similar to LayerSDP.
Table 1 shows the comparative results for the standard benchmarks. The breakdown of the time cost of our method IterSDP is also reported. IterSDP is more precise than the baselines for all the networks, except MLP-LP, MLP-SDP and MLP-9 × 100. For MLP-LP and MLP-SDP, both IterSDP and LayerSDP reach the PGD upper bounds, while for MLP-9×100, IterSDP is only less precise than β-CROWN. Remarkably, for most the networks, IterSDP achieved the verified accuracy that is close to or same as the PGD upper bound. It is also shown in (Dathathri et al. 2020;Li et al. 2020) that the complete method MILP verifies 69% robust cases for MLP-SDP, 67% for MLP-8×1024-0.1 and 7% for MLP-8 × 1024-0.3, lower than 84%, 86% and 33% by our method respectively.
As expected, IterSDP needs more runtime than LayerSDP across all the networks, but is faster than SDP-IP. Neither SDP-IP nor SDP-FO could verify the large models MLP-8×1024-0.1 and MLP-8×1024-0.3. The results reported in (Batten et al. 2021) showed that compared to LayerSDP, SDP-FO has a runtime that is much larger for MLP-Adv and MLP-LP, but smaller for MLP-SDP. Also, SDP-FO fails to verify MLP-6×100, MLP-9×100 and MLP-6×200. These results confirm that our proposed IterSDP improves the verification precision, whilst retaining a competitive computational efficiency.
Relaxation methods that provide tight approximations are required to be able to verify large NNs used in applications. SDP-based methods have been proposed in the literature to accomplish this goal; yet, the relaxation gap in the present SoA is still considerable when applying them to deep and large networks, resulting in SoA tools not being able to establish the result for many verification queries. Here we proposed a novel SDP relaxation to narrow the relaxation gaps and enable efficient NN verification. The method improves the tightness by integrating a nonlinear constraint to the present SoA layer SDP method. Our approach is computationally effective because, unlike previous approaches, the resulting non-convex SDP problem is solved by computing the solutions of auxiliary convex layer SDP problems in an iterative manner. As shown, the method always yields tighter relaxations than the layer SDP and the solution sequence iteratively converges to the optimal solution of the non-convex SDP relaxation. The experiments showed that the method results in SoA performance on all benchmarks commonly used in the area.