In the last few decades, the employment of machine learning (ML) models has been increasingly common in the Artificial Intelligence community, with a particular focus on neural networks (NNs). However, even though they are widely adopted, the lack of formal guarantees on their behavior still restrain their use in safety-critical applications, such as avionics and self-driving vehicles. Formal Verification has been proposed to tackle the reliability issues of NNs, but its complexity and the sheer size of the models of interest have been proven to be hard challenges. In this paper we present an enhancement of our verification algorithm based on counter-example guided abstraction refinement (CEGAR) and show how it performs with respect to other approximate star-based methods.
Adoption and successful application of deep neural networks (DNNs) in various domains across
computer science have made them one of the most popular machine-learned models to date —
see, e.g., [
As witnessed by an extensive survey [
Our tool NeVer2 finds itself at the intersection of the issues explained above, and aims
to bridge the gap between learning and verification of DNNs. NeVer2 borrows its design
philosophy from NeVer [
The remainder of the paper is structured as follows: after an overview of the main concepts in
Section 2, we introduce the abstraction definitions and algorithms in Section 3. Our contribution,
i.e., the refinement step for the CEGAR [
Neural networks. Given a finite number of functions 1 : R → R1 , . . . , : R− 1 → R — also called layers — we define a feed forward neural network as a function : R → R obtained through the compositions of the layers, i.e., () = (− 1(. . . 1() . . .)). The layer 1 is called input layer, the layer is called output layer, and the remaining layers are called hidden. For ∈ R, we consider only two types of layers: • () = + with ∈ R× and ∈ R is an afine layer implementing the linear mapping : R → R; • () = ( 1(1), . . . , ()) is a functional layer : R → R consisting of activation functions — also called neurons; usually = for all ∈ [1, ], i.e., the function is applied componentwise to the vector .
We consider the most common activation function : R → R: the ReLU function defined as () = (0, ). For a neural network : R → R, the task of classification is about assigning to every input vector ∈ R one out of labels: an input is assigned to a class when () > () for all ∈ [1, ] and ̸= ; the task of regression is about approximating a functional mapping from R to R. In this regard, neural networks consisting of afine layers coupled with ReLU layers ofer universal approximation capabilities [29].
Verification task. Given a neural network : R → R we wish to verify algorithmically that it complies to stated post-conditions on the output as long as it satisfies pre-conditions on the input. Without loss of generality1, we assume that the input domain of is a bounded set ⊂ R, i.e., there exists ∈ R, > 0 such that ∀, ∈ we have (, ) < where is the Euclidean norm (, ) = || − ||. Therefore, the corresponding output domain is also a bounded set ⊂ R because () afine transformations of bounded sets are still bounded sets and () ReLU is a piecewise afine transformation of its input. We require that the logic formulas defining pre- and post-conditions are interpretable as finite unions of bounded sets in the input and output domains. Formally, given bounded sets 1, . . . , in such that Π = ⋃︀ =1 , we wish to prove =1 and bounded sets 1, . . . , in such that Σ = ⋃︀ that
∀ ∈ Π → () ∈ Σ. (1)
While this query cannot express some problems regarding neural networks, e.g., invertibility or
equivalence [
^
To enable algorithmic verification of neural networks, we consider a subclass of generalized star sets, introduced in [30] and defined as follows — the notation is adapted from [31]. Definition 1. (Generalized star set) Given a basis matrix ∈ R× obtained arranging a set of basis vectors {1, . . . } in columns, a point ∈ R called center and a predicate : R → {⊤, ⊥}, a generalized star set is a tuple Θ = (, , ). The set of points represented by the generalized star set is given by [[Θ]] ≡ { ∈ R | = + such that (1, . . . , ) = ⊤} (2)
In the following we denote [[Θ]] also as Θ. We consider only star sets such that () := ≤ , where ∈ R× and ∈ R for ≥ 1, i.e., is a conjunction of linear constraints; we further require that the set = { ∈ R | ≤ } is bounded. In order to ensure the convexity, we consider input sets which are either already convex or approximated by one. In this case such sets are polytopes in R whose set we represent as ⟨R⟩. 1Input domains must be bounded to enable implementation of neural networks on digital hardware; therefore, also data from physical processes, which are potentially ubounded, are normalized within small ranges in practical applications.
Algorithm 1 Abstraction of the ReLU activation function.
1: function compute_layer(input = [Θ1, . . . , Θ ], refine = [1, . . . , ]) 2: output = [ ] 3: for = 1 : do 4: stars = [Θ] 5: for = 1 : do stars = compute_relu(stars, , refine [], ) 6: append(output, stars) 7: return output Definition 2. (Abstract afine mapping) Given a star set Θ = (, , ) and an afine mapping : → with = + , the abstract afine mapping ˜ : ⟨⟩ → ⟨⟩ of is defined as ˜ (Θ) = (^, ^ , ) where ^ = + ^ =
Intuitively, the center and the basis vectors of the input star Θ are afected by the transformation of , while the predicates remain the same.
Algorithm 1 defines the abstract mapping of a functional layer with ReLU activation functions. The function compute_layer takes as input an indexed list of stars Θ1, . . . , Θ and an indexed list of positive integers called refinement levels . For each neuron, the refinement level tunes the grain of the abstraction: level 0 corresponds to the coarsest abstraction that we consider — the greater the level, the finer the abstraction grain. In the case of ReLUs, all non-zero levels map to the same (precise) refinement, i.e., a piecewise afine mapping. The ReLU function
ReLU
ReLU Over-Approximation
ReLU Over-Approximation 3.0 2.5 2.0 1.5 yj 1.0 0.5 0.0 0.5 1.0 3 output of function compute_layer is still an indexed list of stars, that can be obtained by independently processing the stars in the input list. For this reason, the for loop starting at line 3 can be parallelized to speed up actual implementations. Given a single input star Θ ∈ ⟨⟩, each of the dimensions is processed in turn by the for loop starting at line 5 and involing the function compute_relu. Notice that the stars obtained processing the -th dimension are feeded again to compute_relu in order to process the + 1-th dimension. For each star given as input, the function compute_relu first computes the lower and upper bounds of the star along the -th dimension by solving two linear-programming problems — function get_bounds at line 11. Independently from the abstraction level, if ≥ 0 then the ReLU acts as an identity function (line 13), whereas if ≤ 0 then the -th dimension is zeroed (line 14). The * operator takes a matrix , a star Γ = (, , ) and returns the star ( , , ). In this case, is composed of the standard orthonormal basis in Rn arranged in columns, with the exception of the -th dimension which is zeroed.
When < 0 and > 0 we consider the refinement level. For any non-zero level, the input star is “split” into two new stars, one considering all the points < 0 (Θ) and the other considering points ≥ 0 (Θ) along dimension . Both Θ and Θ are obtained by adding to the input star input[k] the appropriate constraints. Notice that, if the analysis at lines 17–18 is applied throughout the network, and the input abstraction is precise, then the abstract output range will also be precise, i.e., it will coincide with the concrete one: we call complete the analysis of NeVer2 in this case. The number of resulting stars is worst-case exponential, therefore the complete analysis may result computationally infeasible.
If the refinement level is 0, then the ReLU is abstracted using the over-approximation proposed in [31] and depicted in Figure 1. This approach is much less conservative than others, i.e., based on zonotopes or abstract domains, and provides a tighter abstraction. The computation of the resulting star is carried out from line 21 to line 25. Intuitively, given the predicates of the input star ≤ , the matrix and the vector are modified to constrain the output star within the points inside the triangle defining the abstraction, given the points of the input star. If this analysis is carried out throughout the network, then the output star will be a (sound) over-approximation of the concrete output range: we call over-approximate the analysis of NeVer2 in this case. The number of star remains the same throughout the analysis, but at the cost of a new predicate variable for each neuron which, in turn, increases the complexity of the linear program required by get_bounds.
In [
Our algorithm can be used to compute the complete or over-approximate reachable set of the neural network of interest. Once the reachable set has been computed, the property of interest can be verified by computing the intersection between the negation of such property and the reachable set (which we call reachable counter set). If such intersection is the empty set, then the network is compliant with the property of interest; otherwise, if the reachable set is complete, we have shown that the network is unsafe. However, if the reachable set is over-approximated, the concrete network may satisfy the property, and the over-approximation may be too coarse. In both cases in which the reachable counter set is not the empty set, we are interested in extracting concrete input points corresponding to the output contained in the reachable counter set. In particular, when we have a complete counter reachable set we can leverage the following theorem: Theorem 1. Let be a feed-forward neural network, Θ = (, , ) be a star input set, (Θ) = ⋃︀
=1 Θ, Θ = (, , ) be the reachable set of the neural network and S be a safety specification. Denote Θ = Θ ∩ ¬S = (, , ), = 1, ..., . The neural network is safe if and only if = 0 for all i. If the neural network violates its safety property then the complete counter input set containing all possible inputs in the input set that lead the neural network to unsafe states is C = ⋃︀
=1(, , ), ̸= 0.
For the proof of Theorem 1 we refer to [32]. Using Theorem 1 we can easily compute the complete counter input set, so the problem of extracting concrete input points becomes the problem of extracting points from a star-set which in itself can be considered as extracting points from a single star. To do this, we consider the problem of extracting points from the predicate of the star, which, under our pre-conditions, is always a polytope. We will then apply to the points of the predicate ( ) the afine transformation = + to obtain a corresponding point of the star of interest. To extract the point from the polytope defined by the predicate, we leverage the hit and run sampler [33]. It should be noted that while the hit and run algorithm produces an approximation of a uniform distribution for the of the predicate, the application of the afine transformation needed for the transformation to the point of the star skews such distribution. A possible solution to this issue is to transform the predicate to its V-representation, apply the afine transformation directly to the polytope, return to the H-representation and apply the hit and run sampler. However, for our aims, the skew of the distribution is not that relevant. Therefore, at least at this time, we do not need to transform between the two representations, which is computationally expensive.
The problem is diferent when we are working with the over-approximate reachable counter set: in this case, we do not have a way to compute the counter input set since the addition of the new variables needed for the over-approximation to the predicate of the star invalidates Theorem 1. Therefore an alternative solution is needed to compute inputs that allegedly are not compliant with the property of interest. We define the abstract counter output set (ACOS) as the intersection between the abstract reachable set and the negation of the property . Our algorithm extracts a point from the ACOS using hit and run sampling and then searches for the corresponding input point. Formally the search problem of the corresponding input point can be defined as: Definition 3. Given a reference output point ^, a starting input point and a feed forward neural network we can define the search problem for the point ^ which satisfies (^) = ^ as the following minimization problem:
^ = min ||^ − ()||2
However, the non-convexity and non-linearity of the function make the minimization problem not easily solvable: the non-convexity and the presence of local minima make it extremely dificult to apply gradient descent. Consequently, we developed a simple search-by-sampling algorithm which, given a starting point in the input space, generates a “cloud" of points using a normal distribution with the starting point as center and a given variance. Such points are then compared, and the one whose corresponding output is nearest to the desired one is selected as the center for another step of the algorithm. The search terminates when the euclidean distance between the output found and the one we are searching for is less than a given threshold or when a given number of steps is exceeded. If the algorithm finds an input point in the concrete input set and whose corresponding output is in the ACOS, we have found a concrete counter-example, and the network is proven unsafe. Otherwise, the point found is a point whose corresponding output is reasonably close to the ACOS and can be leveraged for our refinement.
Once an adequate sample is found, we can use it to guide our refinement. The idea behind the refinement algorithm is to rank the approximation error for each neuron by computing the triangle areas of the approximate method — see, Section 3 — and enhance it with a measure of the relevance of the neurons with respect to the sample found. To compute the relevance, we leveraged the layer-wise relevance propagation algorithm [34] which, while traditionally used by the explainability community for classification models, can provide an adequate relevance measure even for regression tasks. It should be noted that our implementation of the algorithm support, at present, only fully-connected layers and ReLU activation functions. For more details on layer-wise relevance propagation we refer to [35].
The refinement procedure is detailed in Algorithm 2. As the first thing, it needs to apply our verification methodology in its over-approximate form (line 2) to compute the over-approximate reachable counter set and the triangle areas. If the network is proven to be safe (line 3) then the verification algorithm terminates (line 4), otherwise we can search the counter-example as shown before (line 5 and 6). If we found a concrete counter-example then the network is proven to be unsafe and the procedure terminates (line 7 and 8), otherwise we use the spurious Algorithm 2 CEGAR Algorithm.
1: function cegar_verification(input_set, unsafe_zone, network) 2: ref_levels = [0, ..., 0] 3: , , = starset_ver(input_set, unsafe_zone, network, ref_levels) 4: if is_empty(ACOS) then 5: return , , 6: 7: 8: 9: 10: 11: 12: _ = get_sample(ACOS) _ = input_search(network, output_counter) if _ ∈ _ then
return , , _ = compute_rel(input_counter, network) _ = compute_ref_levels(neuron_relevances, areas) return starset_ver(input_set, unsafe_zone, network, ref_levels) counter-example to find the relevances of the neurons of the network (line 9). At this point, the relevances and the triangle areas can be used to evaluate the significance of each ReLU neuron of the network. Once a measure of the significance is computed for each neuron of each ReLU layer, we can choose a given number of neurons to refine for each layer (line 10), and we can change the refinement levels of Algorithm 1 as needed. Then our verification methodology is applied again using the new refinement levels (line 11).
In this Section, we provide some empirical results about NeVer22. Our experiments are focused on the verification task. For the comparison, we considered networks and properties from the ACAS Xu evaluation [36]. ACAS Xu is an airborne collision avoidance system based on DNNs whose purpose is to issue advisory commands to an autonomous vehicle (ownship) about evasive maneuvers to be performed if another vehicle (intruder) comes too close. In particular, we selected Property 3 and 4 since they could be easily expressed as a single verification query in our tool. In the words of [36], these safety properties “deal with situations where the intruder is directly ahead of the ownship and state that the NN will never issue a COC (clear of conflict) advisory”. Considering the analysis in [36], each property can be assessed on 42 diferent networks depending on the choice of two parameters, i.e., the the previous advisory value and the time to loss of vertical separation. Among the networks available, we selected those for which our over-approximate analysis could not find a definitive answer, ending with a total of 9 networks. Notice that Property 3 and Property 4 are always satisfied in these networks.
In our experimental evaluation, we compare two diferent significance measures. Product significance (PS) computes, for each neuron, the value of the multiplication between its relevance 2All experiments ran on a laptop equipped with an Intel i7-8565 CPU (8 core at 1.8GHz) and 16 GB of memory with Ubuntu 20 operating system. and the area of the triangle abstraction, whereas mixed-R (mR) uses the relevances as coeficients for the ranking used in the standard mixed methodology. The PS refinement ( CEGAR-PS) selects six neurons in the whole network to refine, while the mR refinement ( CEGAR-mR) refines one single neuron for each layer. In Table 1 we show the performance of the two versions of the refinement algorithm, and we compare them with our mixed abstraction methodology. Note that, by design, the number of neurons refined is the same for every methodology: six in the whole network. The diference between the three algorithms is which neurons are selected and how.
As can be seen, the performances of the two refinement algorithms are comparable; however, they seem to be less efective than our mixed methodology and CEGAR-PS seems to be slightly more accurate than CEGAR-mR at the cost of a small increase in the time needed to solve the query. We believe that the diference in performance is mainly attributable to the fact that, while the measurements of relevance we used are valid, they do not capture how the coarseness of the abstraction changes dynamically when a particular neuron is refined. On the contrary, the mixed methodology chooses in each layer the neuron to refine based on the values of the areas of the triangles given the previous layer output. As a consequence, the choice of which neurons to refine is guided by the coarseness of the abstraction after the refinement is already applied in the previous layers.
In this paper we tried to enhance our verification methodology, leveraging a novel counterexample guided abstraction refinement algorithm. The refinement algorithm computes the over-approximate reachable set, searches for a spurious counterexample and then uses it to compute the relevance measures for all neurons in the network. Then, a specific heuristic is used to select which neurons must be refined in computing the new reachable set. Although our experimental results showed that our refinement methodology performances do not present an enhancement with respect to the ones of the algorithms presented in Section 3, we believe that with further investigations we will be able to further enhance this technique. refinement, in: Proceedings of CAV 2000, volume 1855 of Lecture Notes in Computer Science, 2000, pp. 154–169. [29] K. Hornik, M. Stinchcombe, H. White, Multilayer feedforward networks are universal approximators., Neural networks 2 (1989) 359–366. [30] S. Bak, P. S. Duggirala, Simulation-equivalent reachability of large linear systems with inputs, in: International Conference on Computer Aided Verification, Springer, 2017, pp. 401–420. [31] H.-D. Tran, D. M. Lopez, P. Musau, X. Yang, L. V. Nguyen, W. Xiang, T. T. Johnson, Starbased reachability analysis of deep neural networks, in: International Symposium on Formal Methods, Springer, 2019, pp. 670–686. [32] D. Tran, Verification of Learning-enabled Cyber-Physical Systems, Ph.D. thesis, Vanderbilt
University, 2020. [33] R. L. Smith, The hit-and-run sampler: A globally reaching markov chain sampler for generating arbitrary multivariate distributions, in: J. M. Charnes, D. J. Morrice, D. T. Brunner, J. J. Swain (Eds.), Proceedings of the 28th conference on Winter simulation, WSC 1996, Coronado, CA, USA, December 8-11, 1996, IEEE Computer Society, 1996, pp. 260–264. [34] W. Samek, G. Montavon, A. Binder, S. Lapuschkin, K. Müller, Interpreting the predictions of complex ML models by layer-wise relevance propagation, CoRR abs/1611.08191 (2016). [35] G. Montavon, A. Binder, S. Lapuschkin, W. Samek, K. Müller, Layer-wise relevance propagation: An overview, in: Explainable AI: Interpreting, Explaining and Visualizing Deep Learning, volume 11700 of Lecture Notes in Computer Science, Springer, 2019, pp. 193–209. [36] G. Katz, C. W. Barrett, D. L. Dill, K. Julian, M. J. Kochenderfer, Reluplex: An eficient SMT solver for verifying deep neural networks, in: Proceedings of CAV 2017, volume 10426 of Lecture Notes in Computer Science, 2017, pp. 97–117.