domain: info spi

text:
Fateh Boudardara

Abderraouf Boussif

Pierre-Jean Meyer

Mohamed Ghazel

INNAbstract: An INN-Based Abstraction Method for Large-Scale Neural Network Verification

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INNAbstract: An INN-Based Abstraction Method for Large-Scale Neural Network Verification Fateh Boudardara , Abderraouf Boussif , Pierre-Jean Meyer , and Mohamed Ghazel , Member, IEEE Abstract-Neural networks (NNs) have witnessed widespread deployment across various domains, including some safetycritical applications. In this regard, the demand for verifying means of such artificial intelligence techniques is more and more pressing. Nowadays, the development of evaluation approaches for NNs is a hot topic that is attracting considerable interest, and a number of verification methods have been proposed. Yet, a challenging issue for NN verification is pertaining to the scalability when some NNs of practical interest have to be evaluated. This work aims to present INNAbstract, an abstraction method to reduce the size of NNs, which leads to improving the scalability of NN verification and reachability analysis methods. This is achieved by merging neurons while ensuring that the obtained model (i.e., abstract model) overapproximates the original one. INNAbstract supports networks with numerous activation functions. In addition, we propose a heuristic for nodes' selection to build more precise abstract models, in the sense that the outputs are closer to those of the original network. The experimental results illustrate the efficiency of the proposed approach compared to the existing relevant abstraction techniques. Furthermore, they demonstrate that INNAbstract can help the existing verification tools to be applied on larger networks while considering various activation functions.

Index Terms-Formal verification, neural network (NN) abstraction, neural networks (NNs), NN verification.

I. INTRODUCTION

N EURAL networks (NNs) are one of the most widely used techniques in machine learning. They have been successfully applied to solve many complex problems in different domains, including automatic speech recognition, computer vision, and healthcare [START_REF] Li | A survey of convolutional neural networks: Analysis, applications, and prospects[END_REF], [START_REF] Litjens | A survey on deep learning in medical image analysis[END_REF]. The success of NNs motivated the academic and industrial communities to adopt this technique in safety-critical systems, such as autonomous cars and trains [START_REF] Bouguettaya | Vehicle detection from UAV imagery with deep learning: A review[END_REF], [START_REF] Ristić-Durrant | A review of visionbased on-board obstacle detection and distance estimation in railways[END_REF] and air traffic collision avoidance systems [START_REF] Julian | Policy compression for aircraft collision avoidance systems[END_REF]. The development of such systems requires a rigorous process of testing, verification, and validation to ensure that each (software) component in the system meets a set of functional and safety requirements. Evaluating the network's Fateh Boudardara and Abderraouf Boussif are with the Technological Research Institute Railenium, F-59308 Valenciennes, France (e-mail: fateh.boudardara@railenium.eu; abderraouf.boussif@railenium.eu).

Pierre-Jean Meyer and Mohamed Ghazel are with Universite Gustave Eiffel, COSYS-ESTAS, F-59666 Villeneuve d'Ascq, France (e-mail: pierre-jean.meyer@univ-eiffel.fr; mohamed.ghazel@univ-eiffel.fr).

This article has supplementary material provided by the authors and color versions of one or more figures available at https://doi.org/10.1109/ TNNLS.2023.3316551.

Digital Object Identifier 10.1109/TNNLS.2023.3316551 performance on a representative set of samples (test set) is a common way to assess its accuracy. However, this remains insufficient when such NN-based software is used in safetycritical applications since there is no guarantee of how the network would behave on other unseen samples. Indeed, recent studies have demonstrated the sensitivity and the vulnerability of NNs to adversarial attacks (i.e., small perturbations to the inputs that can drastically change the corresponding outputs). These perturbations are generally imperceptible to humans and easy to generate [START_REF] Yuan | Adversarial examples: Attacks and defenses for deep learning[END_REF], [START_REF] Eykholt | Robust physical-world attacks on deep learning visual classification[END_REF]. For instance, Szegedy et al. [START_REF] Szegedy | Intriguing properties of neural networks[END_REF] demonstrated that adding small noise to an image may lead the NN to misclassify the image that was, beforehand, correctly classified. For these reasons, NN verification has become a hot research topic and has witnessed a noticeable interest in the last few years [START_REF] Liu | A survey of deep neural network architectures and their applications[END_REF], [START_REF] Meng | Adversarial robustness of deep neural networks: A survey from a formal verification perspective[END_REF], [START_REF] Urban | A review of formal methods applied to machine learning[END_REF]. Formal verification methods, such as model checking [START_REF] Clarke | Handbook of Model Checking[END_REF], satisfiability analysis (SAT) [START_REF] Biere | Handbook of Satisfiability[END_REF], reachability analysis, and abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] have proven to be effective in offering formal proofs of the safety for both software and hardware systems. Recently, these techniques have been adopted to verify some properties of NNs. Verifying an NN consists of checking that the NN never violates some predefined properties. Namely, for a given input region defined by a set of constraints, we check whether the NN's generated output is necessarily within a safe output region [START_REF] Leofante | Automated verification of neural networks: Advances, challenges and perspectives[END_REF]. Early works dealing with this issue relied on reducing the verification process to an optimization problem by encoding the input-output constraints (the property) and the network's behavior (the model) as a linear programming (LP) problem and then applying an LP-solver, such as mixed integer LP (MILP) [START_REF] Cheng | Maximum resilience of artificial neural networks[END_REF], [START_REF] Lomuscio | An approach to reachability analysis for feed-forward ReLU neural networks[END_REF] or satisfiability modulo theory (SMT) solvers [START_REF] Huang | Safety verification of deep neural networks[END_REF], [START_REF] Katz | The marabou framework for verification and analysis of deep neural networks[END_REF], [START_REF] Pulina | An abstraction-refinement approach to verification of artificial neural networks[END_REF] to check the properties. NN verification is known to be an NP-complete problem [START_REF] Katz | Reluplex: An efficient SMT solver for verifying deep neural networks[END_REF], and the complexity of the verification algorithms increases exponentially with the number of neurons in the network. As a result, most of the existing verifiers encounter the state-space explosion problem. For instance, a straightforward application of SAT/SMT or MILP on a network of n Relu neurons may result in generating 2 n linear subproblems. One way to address this issue is to resort to approximation and abstraction methods. The general concept of these methods is to either linearly approximate the activation function, or merge some neurons of the network to create an abstract one that is a sound overapproximation of the original network [START_REF] Boudardara | A review of abstraction methods towards verifying neural networks[END_REF]. The latter are often called model reduction techniques.

We should mention here another field known as NN compression, which is interested in merging neurons to build smaller networks with comparable performance to the original one. In particular, methods based on quantization [START_REF] Cheng | Quantized CNN: A unified approach to accelerate and compress convolutional networks[END_REF] and pruning [START_REF] Gonzalez-Carabarin | Dynamic probabilistic pruning: A general framework for hardware-constrained pruning at different granularities[END_REF] are extensively used in NN compression. These techniques aim to produce smaller networks to improve their efficiency in terms of memory usage and computational resources. This allows them to be deployed on resourceconstrained devices. However, it is important to emphasize that NN compression does not provide any formal guarantee about the obtained reduced network. Consequently, the verification results on the reduced network cannot be lifted to the original network, and thus no inference can be made about the correctness of the original network. Unlike NN compression, NN abstraction (or model reduction) methods generate abstract networks that are used to enhance the verification process. Indeed, once the required properties have been successfully verified on an abstract network, we can lift this result to the original network, allowing for its safe deployment in the intended system.

In this article, we present INNAbstract, a model reduction method for NNs to enhance the scalability of NN operations, particularly in the context of verification and reachability analysis. The proposed method relies on merging a set of nodes (neurons) and calculating the abstract node's weights using mathematical formulas to ensure that the abstract model is an overapproximation of the original one (i.e., the output of the original network is always within the output range of the abstract network). Indeed, node merging allows for reducing the size of the NN and, hence, instead of verifying properties on the large original model, these properties can be checked on the reduced model with lower computation complexity. This helps improve the scalability of the reachability analysis and verification processes. Unlike other abstraction techniques, INNAbstract applies to NNs with various activation functions. To assess the efficiency and the scalability of the proposed approach, we conducted a series of experiments on a set of selected benchmarks from the literature.

Notice that this work is a revised and extended version of a workshop article [START_REF] Boudardara | Interval weight-based abstraction for neural network verification[END_REF], in which the general idea of the approach along with some early preliminary results was presented. Compared to the preliminary workshop version, in this article.

1) We present the theoretical foundations of the approach while extending it to support a wide range of activation functions (Relu, Tanh, Bipolar Sigmoid, etc.). 2) We provide the formal proofs of the underlying theoretical results, particularly regarding the assurance of the overapproximation relation. 3) We provide the pseudo-algorithms that implement the main steps of the abstraction process. 4) We propose a heuristic for efficiently selecting the nodes to be merged, to enhance the precision of the abstraction. 5) Finally, we present a software tool implementing the approach, which is used to conduct an extensive experimental study (on random-generated and well-known benchmark networks), to evaluate the efficiency of the approach. Furthermore, we compare our method to other relevant approaches from the literature.

The remainder of this article is structured as follows: Section II provides a brief overview of NN verification and abstraction works. Section III gives basic concepts and notations of NNs and recalls some concepts pertaining to the NN verification problem. Section IV presents the proposed abstraction approach along with the underlying pseudo-algorithms, and heuristics for selecting nodes to be merged. The description of the conducted experiments and some related discussion are given in Section V. Finally, Section VI concludes the article and proposes some guidelines for future works.

II. RELATED WORKS

The interest in NN verification can be traced back to the early 2000s [START_REF] Taylor | Methods and Procedures for the Verification and Validation of Artificial Neural Networks[END_REF]. However, the first concrete work that deals with this problem was proposed by Pulina and Tacchella [START_REF] Pulina | An abstraction-refinement approach to verification of artificial neural networks[END_REF], where they proposed an SMT-based verification method for Sigmoid feed-forward NNs. Katz et al. [START_REF] Katz | Reluplex: An efficient SMT solver for verifying deep neural networks[END_REF] introduced Reluplex for Relu networks. Reluplex combines the Simplex optimization method with the SAT technique to handle the nonlinearity of Relu constraints. Many verification methods based on SAT/SMT solvers for Relu NNs have been proposed [START_REF] Huang | Safety verification of deep neural networks[END_REF], [START_REF] Katz | The marabou framework for verification and analysis of deep neural networks[END_REF]. Other methods based on LP-solving encode the network behavior and the input-output constraints as an MILP problem and apply an adequate solver to address the verification problem [START_REF] Lomuscio | An approach to reachability analysis for feed-forward ReLU neural networks[END_REF], [START_REF] Tjeng | Evaluating robustness of neural networks with mixed integer programming[END_REF], [START_REF] Dutta | Output range analysis for deep feedforward neural networks[END_REF]. Although these techniques are exact since they encode the complete behavior of the network and the property to be verified, they are severely limited to small networks due to the complexity and the nonlinearity of NNs [START_REF] Huang | A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability[END_REF].

Another line of research consists of applying the concept of abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] in an attempt to build an abstract network that is easy to verify, and at the same time, overapproximates the behavior of the original network. The abstraction method must ensure that if the property holds on the abstract model, it necessarily holds on the original one. Various approaches based on convex and linear relaxation of the activation function have been proposed. Gehr et al. [START_REF] Gehr | AI2: Safety and robustness certification of neural networks with abstract interpretation[END_REF] applied abstract interpretation to verify NNs for the first time. They proposed an abstraction of the Relu activation function using zonotopes. This approach is lately improved further by proposing an abstraction for other activation functions, such as Tanh and Sigmoid [START_REF] Singh | An abstract domain for certifying neural networks[END_REF], [START_REF] Singh | Fast and effective robustness certification[END_REF]. In other works, the problem of NN verification is formulated as a reachability problem that is solved by calculating the reachable set (region) of the network with respect to some given input region. Therefore, the verification is carried out by checking whether the obtained output region is included in some predefined safe region [START_REF] Wang | Efficient formal safety analysis of neural networks[END_REF], [START_REF] Xiang | Reachable set estimation for neural network control systems: A simulation-guided approach[END_REF], [START_REF] Xiang | Output reachable set estimation and verification for multilayer neural networks[END_REF], [START_REF] Wang | Formal security analysis of neural networks using symbolic intervals[END_REF]. Since reachability methods are incomplete and may generate coarse outputs, some optimization methods are proposed for networks with piecewise linear activation function, particularly for Relu-NN, to provide tighter bounds of the outputs [START_REF] Wu | Efficient neural network analysis with sum-of-infeasibilities[END_REF], [START_REF] Henriksen | DEEPSPLIT: An efficient splitting method for neural network verification via indirect effect analysis[END_REF], [START_REF] Lan | Tight neural network verification via semidefinite relaxations and linear reformulations[END_REF], [START_REF] Wang | Beta-CROWN: Efficient bound propagation with perneuron split constraints for neural network robustness verification[END_REF], [START_REF] Palma | Improved branch and bound for neural network verification via Lagrangian decomposition[END_REF]. Some recent works propose a convex relaxation of Relu networks by considering multiple nodes and the dependencies between them at the same time [START_REF] Singh | Beyond the single neuron convex barrier for neural network certification[END_REF], [START_REF] Müller | PRIMA: General and precise neural network certification via scalable convex hull approximations[END_REF]. In this article, we employed the interval bounds propagation (IBP) algorithm [START_REF] Xiang | Reachable set estimation for neural network control systems: A simulation-guided approach[END_REF] as a reachability analysis technique to calculate the output range of the abstract and original networks.

As a subcategory of abstraction methods, model reduction methods' objective is to build an abstract (also called reduced) model by merging a set of neurons of the same layer. Hence, instead of applying the verification on the large original model, it is rather applied on the smaller abstract model [START_REF] Ashok | DeepAbstract: Neural network abstraction for accelerating verification[END_REF], [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF], [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF]. Ashok et al. [START_REF] Ashok | DeepAbstract: Neural network abstraction for accelerating verification[END_REF] proposed DeepAbstract as a model reduction method. DeepAbstract implements the K-mean clustering algorithm to rearrange Relu nodes of a layer in clusters. Next, each cluster is replaced by its representative node. The overapproximation is established by propagating the error introduced during the merging process and, then, the verifier ERAN [START_REF] Singh | An abstract domain for certifying neural networks[END_REF] is brought into play for verification. Elboher et al. [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] proposed a model reduction method for Relu-NN. The main idea of the approach is to classify neurons into four different categories according to the sign of their outgoing weights (positive and negative), and whether increasing the value of the neuron at hand would increase or decrease the network's output (increasing and decreasing). Finally, model reduction is applied by merging nodes belonging to the same category. To evaluate the performance of the approach, Elboher et al. [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] used the Marabou tool [START_REF] Katz | The marabou framework for verification and analysis of deep neural networks[END_REF] as a back-end verifier and compared the obtained results to those obtained by Marabou without applying the model reduction method. Recently, a similar method to the one of Elboher et al. [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] is proposed by Liu et al. [START_REF] Liu | Abstraction and refinement: Towards scalable and exact verification of neural networks[END_REF], where the authors classify neurons into only two categories (increasing and decreasing) instead of four categories. In addition, they introduced a new operation called FREEZE to replace an increasing (resp. decreasing) neuron by its upper bound (resp. lower bound) and then propagate this constant through the network. Another approach for Relu-NN model reduction based on Interval NNs (INNs) was introduced by [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF]. The abstract node is defined by its incoming and outgoing weights; its incoming weight is the interval-hull of the incoming weights of the corresponding set of merged nodes in the original network, and its outgoing weight is the interval-hull of the outgoing weights of the same set multiplied by its size (i.e., the number of nodes). Moreover, the big-M MILP encoding [START_REF] Cheng | Maximum resilience of artificial neural networks[END_REF] is adopted to compute the output range of the obtained INN. A generalization of this approach is proposed by Sotoudeh and Thakur [START_REF] Sotoudeh | Abstract neural networks[END_REF], where the abstraction can be performed using further abstract domains, such as Zonotopes, and is not restricted to intervals. Recently, Prabhakar defined NN-bisimulation that can be used to reduce the size of NN [START_REF] Prabhakar | Bisimulations for neural network reduction[END_REF]. As a consequence of NNbisimulation's conditions, which are far from being satisfied on real-world models, a more tolerated (mitigated) approach, namely δ-bisimulation, is proposed in the same article [START_REF] Prabhakar | Bisimulations for neural network reduction[END_REF]. Refer to [START_REF] Boudardara | A review of abstraction methods towards verifying neural networks[END_REF], for a comprehensive review of model reduction methods.

A related research field, known as NN compression, focuses also on reducing the size of NNs by merging neurons and eliminating certain weighted-edges without affecting their accuracy. Techniques such as pruning [START_REF] Gonzalez-Carabarin | Dynamic probabilistic pruning: A general framework for hardware-constrained pruning at different granularities[END_REF], quantization [START_REF] Cheng | Quantized CNN: A unified approach to accelerate and compress convolutional networks[END_REF], and distillation [START_REF] Xu | Deep neural network self-distillation exploiting data representation invariance[END_REF] have gained significant attention in the field. These techniques are more valuable to build compressed NN models to effectively deploy them on resource-constrained devices. However, it is important to note that these techniques do not provide any formal guarantee about the obtained compressed models [START_REF] Mishra | A survey on deep neural network compression: Challenges, overview, and solutions[END_REF], making them unsuitable for verification purposes.

In the present article, we propose a model reduction method that provides formal guarantees on the obtained network and ensures that the reduced model overapproximates the original one. Compared to the aforementioned abstraction works, the abstraction technique elaborated in our work is more general. While most of the previously discussed works are limited to the Relu activation function, our method supports different types of activation functions. Moreover, compared to [START_REF] Ashok | DeepAbstract: Neural network abstraction for accelerating verification[END_REF], where the abstraction depends on the set of input images on which one wants to check the robustness of the network, our approach generates abstract networks independent of any specific input domains. We should also mention the two techniques presented in [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] and [START_REF] Liu | Abstraction and refinement: Towards scalable and exact verification of neural networks[END_REF] which focus on categorizing the weights of the network by analyzing their signs and impact on the output (increasing or decreasing). Both techniques require a preprocessing phase to classify all nodes of the networks. Additionally, these approaches can only merge nodes that belong to the same category. In contrast, our approach does not require any preprocessing phase, and if applied until saturation, a layer can be (theoretically) reduced to a single abstract node. Finally, we should highlight that the approach proposed in [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] is the closest to our technique since both are based on INN. However, there is a significant difference in our approach. Specifically, Prabhakar and Afzal [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] define the abstract weights as the interval-hull of the corresponding weights in the original network. In our method, we define the abstract outgoing weights as the sum of absolute values over the original weights and transfer their signs to the corresponding incoming weights. This approach helps build more precise abstract networks,1 as can be observed through the experimental results discussed in this article.

III. PRELIMINARIES

A. Deep NNs

Deep NNs (DNNs) are a graph-based machine-learning technique. Depending on the application domain, many DNN architectures have been proposed (CNNs, RNNs, etc.) [START_REF] Liu | A survey of deep neural network architectures and their applications[END_REF], [START_REF] Goodfellow | Deep Learning[END_REF], [START_REF] Lecun | Deep learning[END_REF]. In this article, we focus on feed-forward NNs [START_REF] Bebis | Feed-forward neural networks[END_REF] and we use the term DNN to refer to them.

A DNN is a set of interconnected nodes organized in layers. It receives (numerical) data from the input layer and propagates them through its hidden (i.e., intermediate) layers, up to the last one which is called the output layer. Fig. 1 depicts an example of an NN with a 4-D input layer, two hidden layers, and a 2-D output layer. The nodes are connected via weighted edges whose values are determined during the training phase.

Definition 1: For a DNN N , the set of nodes of a layer l i is represented by S i . S 0 is the input set, S n is the output set, and ∀i ∈ {1, 2, . . . , n -1}, S i represents the set of nodes of the hidden layer l i . Two successive layers, l i-1 and l i , are connected via a weighted-matrix W i , such that for i ∈ {1, 2, . . . , n}, w i jk = w(s i-1,k , s i, j ) denotes the weight of the edge connecting

s i-1,k ∈ S i-1 to s i j ∈ S i , for all k ∈ {1, 2, . . . , |S i-1 |} and j ∈ {1, 2, . . . , |S i |}.
Definition 2: Given a node s i j ∈ S i , i ∈ {1, 2, . . . , n}, its valuation v(s i j ) = v i j is calculated as follows:

v(s i j ) = α   s i-1,k ∈S i-1 w(s i-1,k , s i j ) × v(s i-1,k )   ( 1
)
where ∀s 0 j ∈ S 0 , j ∈ {1, 2, . . . , |S 0 |}, v(s 0 j ) = x j is the value of the jth element of the input x, and α : R → R is the activation function of the DNN.

Notice that several types of activation functions can be used with DNNs. For instance, ( 2) and ( 3) define Relu and Tanh functions, respectively,

relu(x) = max(0, x); x ∈ R (2)
tanh(x) = e x e -x e x + e -x ; x ∈ R.

(

) 3
From Definition 2, and with a slight abuse of notation, we use v(S i ) or V i to denote the valuation vector corresponding to all nodes of layer S i , that is,

V i = v(S i ) = [v(s i1 ), v(s i2 ), . . . , v(s i|S i | )] τ .
Definition 3: Given a DNN of n layers with its associated function:

N : R |S 0 | → R |S n | , its valuation for an input x is N (x) = v(S n ).
In Definition 3, the function N is the composition of a set of vector functions f i , where i ∈ {1, 2, . . . , n}, that is,

N = f n • f n-1 • • • • • f 1 ,
where f i is the function of layer l i and is defined as follows:

f i = α W i × v(S i-1 ) (4)
where

W i ∈ R |S i |×|S i-1 |
is the weight matrix of layer l i .

In the remainder of this article, we exchangeably use w i jk or w(s i-1,k , s i j ) to represent the weight of the edge connecting the node s i-1,k ∈ S i-1 to the node s i j ∈ S i .

Remark 1: For the sake of simplicity of formulas and proofs, we did not include biases explicitly in the definition of DNNs. In fact, the bias vector b i of a layer l i can be replaced by a weight vector connecting a new node s i-1,b ∈ S i-1 to all the nodes s i j of S i such that v(s i-1,b ) = 1 and w(s i-1,b , s i j ) = b i j . An illustrative example is given in Fig. 2.

B. DNN Verification

Since the parameters of a DNN are determined during the training phase of the model on a limited set of data, DNNs may not cover the whole behavior of the modeled system. For example, a DNN model for image classification may misclassify some human-imperceptible perturbed images, which would cause significant damage if it is deployed in a safety-critical system. That is why verifying NNs is crucial.

In general terms, the goal of verifying a network is to check its correctness with respect to some desired properties. Despite the existence of many types of verification properties for DNN, most of the related works focus on the invariant property. For such property, NN verification aims to prove (or disapprove) that for a specific input region, the DNN output lies within some predefined output region. Accordingly, the verification problem of an NN N : R |S 0 | → R |S n | can be defined with the tuple ⟨N , Pre, Post⟩ such that Pre and Post are constraints on the inputs and the outputs of the DNN N, respectively. In other words, for an input region defined by a set of constraints Pre, the objective is to verify whether all the corresponding outputs are within the region defined by the set of constraints Post. This is formulated as

∀x ∈ R |S 0 | , Pre(x) ⇒ Post(N (x)). (5)
Therefore, the verification process consists of either proving that the property defined in ( 5) is true, or providing For image classification, most of the research works focus on DNN robustness [START_REF] Meng | Adversarial robustness of deep neural networks: A survey from a formal verification perspective[END_REF]. In this case, for a given input image x 0 that is classified as c x 0 , the Pre constraints define a region µ that includes perturbed images around x 0 , and the goal of a verification technique is to check whether all these images have the same class c x 0 using the network N . If so, we say the network is robust with respect to region µ.

a counterexample (x * , y * ) ∈ R |S 0 | × R |S n | such that y * = N (x * ),
A common approach to NN verification is to encode the network and the property to be checked as an LP problem. Then, off-the-shelf LP solvers, for example, SAT/SMT and MILP solvers, can be used to perform the verification process. However, methods based on this approach suffer from the state-space explosion problem. This issue primarily arises from the nonlinear behavior of DNNs induced by the activation functions, including simple functions such as piecewise linear functions [e.g., Relu (2)]. Indeed, a Relu neuron has to be split into two linear equations, namely, if y = relu(x), then y = 0 when x < 0 and y = x when x is positive. Thus, verifying a network of n Relu neurons leads to 2 n linear subproblems, and, accordingly, the complexity of the verification problem grows exponentially with the number of neurons. To cope with this inherent complexity problem, abstraction methods are employed to build smaller networks while conserving the relevant behavior of the original one. For instance, these methods can be used to generate abstract networks, which constitute an overapproximation of the original network by merging its nodes [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF], as defined below.

N | P ⇒ N | P. (6)
The above definition means that any time the property P is satisfied by the abstract network N , P is necessarily satisfied by N . Formula (6) can be combined with Formula (5) as follows:

∀x ∈ R |S 0 | , Pre(x) ∧ Post( N (x)) ⇒ Post(N (x)). (7)
It is worth noticing that if N ̸ | P, no conclusion can be inferred regarding N . In this case, we need to check whether the counterexample violating the property P on N (i.e., N ̸ | P) leads to N ̸ | P. If for the generated counterexample, N ̸ | P but N | P, then this counterexample is called a spurious one and hence no conclusion can be made regarding the satisfiability of P by the original network N .

IV. PROPOSED APPROACH

The objective of our method is to reduce the size of a DNN by merging a set of nodes. Abstracting a set of nodes requires providing formulas to determine the incoming and outgoing weights of the obtained abstract node, and a proof ensuring that the reduced network over-approximates the original one. The broad idea of this approach is to define the output weights of the abstract node as the sum of the absolute values over the outgoing weights of the set of merged nodes and bring back

A. Model Reduction for Networks With Odd Activation Functions

Before discussing the details of the approach, let us first recall the definition of an odd function.

Definition 5:

A function g : R → R is odd if ∀x ∈ R : g(-x) = -g(x).
Examples of some used odd activation functions are Tanh, Bipolar Sigmoid, LeCun's Tanh, the identity function, Hard Tanh, and so on [START_REF] Nwankpa | Activation functions: Comparison of trends in practice and research for deep learning[END_REF].

The method consists of merging a set of nodes Ŝ ⊆ S i , where S i is the set of nodes of hidden layer l i , and replacing the subset Ŝ by an abstract node ŝ that is determined by its weights as follows.

1) Incoming weights:

∀s i-1,k ∈ S i-1 , w(s i-1,k , ŝ) = [ ŵl k , ŵu k ], such that      ŵl k = min s i ∈ Ŝ,s i+1, j ∈S i+1 {sign(w(s i , s i+1, j )) × w(s i-1,k , s i )} ŵu k = max s i ∈ Ŝ,s i+1, j ∈S i+1 {sign(w(s i , s i+1, j )) × w(s i-1,k , s i )}. (8)
2) Outgoing weights for i ← 1 to n -1 do ▷ Explore all layers 4:

∀s i+1, j ∈ S i+1 , w(ŝ, s i+1, j ) = s i ∈ Ŝ |w(s i , s i+1, j )| (9)
P i ← Select N odes( N , i, select Strategy) 5:
Abstract OneLayer ( N , i, P i ) for s i-1,k ∈ S i-1 do 5: calculate ŵ(s i-1,k , ŝ) using Equation 86:

end for 7:

for s i+1, j ∈ S i+1 do 8:

calculate ŵ(ŝ, s i+1, j ) using Equation 99:

end for 10:

for s i ∈ Ŝ do 11:

remove s i 12:

end for

(x) = 1, if x ≥ 0 -1, otherwise. (10)
The main steps of the abstraction method (INNAbstract) are presented in Algorithm 1. The algorithm takes as input two parameters: the original network N and the nodes selection strategy. First, a copy of the original network denoted N is generated. Next, for each layer, a partition P i of disjoint subsets of S i is created using the SelectNodes procedure. Then the procedure AbstractOneLayer, presented in Algorithm 2, is applied for merging each subset Ŝ in the partition P i and calculating the weights of the obtained abstract nodes. Finally, the algorithm returns the abstract network N . SelectNodes may correspond to a random selection, or may implement some heuristics as will be discussed in Section IV-C.

An example of executing Algorithm 1 is given in Fig. 5. In this example, we consider that the network uses the identity activation function (α(x) = x). The application of Algorithm 1 on a network N allows the generation of an abstract network that is an overapproximation of N. Based on Algorithm 1, the following results are stated and proved.

Proposition 1: Let N be an NN. Assume that the activation function of N is odd and monotone. Let Ŝi = (S i \ Ŝ) ∪ {ŝ} be the set of nodes in layer i after applying the abstraction procedure on this layer. Then, we have

∀v(S i-1 ), v(S i+1 ) ⊆ v( Ŝi+1 ).
Proposition 2: Let N be an NN. Assume that the activation function of N is odd and monotone. Let N be the abstract network of N obtained using Algorithm 1. Then, we have

∀x ∈ R |S 0 | , N (x) ⊆ N (x).
The proof of Proposition 1 is given in Appendix . The proof of Proposition 2 is straightforward and can be derived from the proof of Proposition 1 by propagating the abstraction from layer l i to l i+1 , up to l n-1 .

B. Model Reduction Method for Relu-NN

The piecewise linear function Relu [see [START_REF] Litjens | A survey on deep learning in medical image analysis[END_REF]] is monotone; however, it is not odd, thus the model reduction method presented in Section IV-A is not straightforwardly applicable on Relu-NN. Concretely, applying the approach presented in Section IV-A on a Relu-NN does not guarantee the overapproximation, that is, the output of the original network may not be within the range of the output of the reduced network (see the counterexample in Fig. 6).

In this section, we present a relaxation of the method presented in Section IV-A, so it can support Relu-NN. The idea is to check whether the incoming weight to every node s ∈ Ŝ has the same sign as its corresponding outgoing weight, and if so, the lower bounds are calculated using the following equation instead of ( 8

): 2      ŵl k = min s i ∈ Ŝ,s i+1, j ∈S i+1 {w(s i-1,k , s i )} ŵu k = max s i ∈ Ŝ,s i+1, j ∈S i+1 {sign(w(s i , s i+1, j )) × w(s i-1,k , s i )}. (11)
2

The formula for calculating the upper bounds of the incoming weights is the same as NN with odd and monotone, that is, Equation 9. for every subset Ŝ in P i do update ŵ(s i-1,k , ŝ) using Equation 118:

end if 9:
end for 10:

for s i+1, j ∈ S i+1 do 11: calculate ŵ(ŝ, s i+1, j ) using Equation 912: end for 13:

for s i ∈ Ŝ do replace all the scalar-weights w of layer l i by an interval [min(w, 0), w] 19: end procedure For two nodes s i-1,k ∈ S i-1 and s ∈ Ŝ ⊆ S i , we define w * i+1, j ∈ {w((s, s i+1, j )) : s i+1, j ∈ S i+1 } as the weight minimizing {sign(w(s, s i+1, j )) × w(s i-1,k , s)}. For a subset Ŝ ⊆ P i of nodes to be abstracted, if all the concrete nodes s ∈ Ŝ satisfy in the following equation below, then the incoming weights of the abstract node ŝ are calculated using [START_REF] Urban | A review of formal methods applied to machine learning[END_REF] s∈ŝ sign(w * i+1, j ) = sign(w(s i-1,k , s)) .

The second step consists of replacing every scalar weight w of layer l i by an interval weight ŵ = [min(w, 0), w]. This is done at the end of the abstraction process of layer l i and before switching to layer l i+1 . The main steps of abstracting a set of nodes of a hidden layer l i of a Relu-NN are summarized in Algorithm 3. The algorithm can be applied on multiple layers as presented in Algorithm 4.

In the following, we state the main results for the abstraction of Relu-NN. Due to the limit on the number of pages, the proof of Proposition 3 is omitted from the article. We should mention that proof of Proposition 4 can be derived from that of Proposition 3 by propagating the abstraction from layer l i to l i+1 , up to l n-1 .

Proposition 3: Let N be an NN. Assume that Relu is the activation function of N . Let Ŝi = (S i \ Ŝ) ∪ {ŝ} be the set of nodes upon applying the abstraction on S i . Then, we have

∀v(S i-1 ), v(S i+1 ) ⊆ v( Ŝi+1 ).
Proposition 4: Let N be an NN. Assume that Relu is the activation function of N . Let N be the abstract network of N obtained using Algorithm 4. Then, we have

∀x ∈ R |S 0 | , N (x) ⊆ N (x).

C. Heuristic for Nodes Selection

The precision of the reduced model depends mostly on the features of the merged nodes. One of the most important features is the sign of the outgoing weights since we use this feature to calculate the weights of the abstract node. Therefore, we propose a heuristic to select the set of nodes to be merged on each layer based on the sign of their outgoing weights. Recall that the sign of outgoing weights of the initial network affects the sign of both incoming and outgoing weights of the abstract network after merging (multiplying incoming weights by this sign, and taking the absolute value for outgoing weights). Therefore, intuitively, it seems more likely that the abstract network will be closer to the original one when the outgoing weights are positive.

In our approach, we propose a heuristic for nodes selection giving priority to nodes having positive outgoing weights, that sor t (sum r ows )

6:

save the first nb Abst nodes in a set Ŝ 7:

return Ŝ 8: end procedure is, the nodes that have more positive weights are to be merged first. This is done by calculating the sign of the outgoing weight matrix of the hidden layer l i , summing the obtained matrix by rows, and then sorting the obtained list. Finally, the selection of the nodes to be merged is done by picking nbAbst nodes from the top of this ordered list, where nbAbst is a parameter of NodeSelectionHeuris procedure that is summarized in Algorithm 5. Notice that NodeSelectionHeuris is used within the procedure SelectNodes in Algorithms 1 and 4 if selectStrategy = heursitics.

V. EXPERIMENTS AND EVALUATION

For evaluation purposes, we implemented the approach as a Python software prototype. The implementation includes three main modules.

1) Network_Reader: reads the DNN model and the inputs' constraints. The tool supports both NNET and ONNX formats. 2) Abstractor: a proof-of-concept implementation of the presented approach, which is used to generate abstract networks from the initial one brought by the first module (Network_Reader). 3) Analyzer: we implemented and adjusted IBP method 3 [START_REF] Xiang | Reachable set estimation for neural network control systems: A simulation-guided approach[END_REF] to support INN, and we used it to calculate the output range of the network. The remaining of the section is dedicated to the empirical evaluation of our approach. It includes a description of the evaluation setup and a summary of the obtained results. A discussion of the obtained results is provided in Section V-C.

In fact, we conducted a set of experiments on networks with a Tanh activation function, which is odd and monotone, 3 IBP is an algorithm to calculate the output range of NNs by propagating the inputs (intervals) through the network's layers. To examine the impact of the network's size on the abstraction method, we generate a set of abstract networks with different sizes. 2) Evaluation on Benchmarks: applying model reduction on two benchmarks: MNIST 4 and ACAS Xu [START_REF] Katz | Reluplex: An efficient SMT solver for verifying deep neural networks[END_REF] for Tanh-NN and Relu-NN, respectively. 3) Heuristic's Improvement: applying our method with two different node selection strategies: random and based on the proposed heuristic, to assess the improvement brought by the latter. A set of Relu-NN of different sizes and depths is used. Additionally, we performed a comparison study between our method and two other abstraction techniques proposed in [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] and [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF]. Since the latter support only the Relu activation function, we considered random Relu-NN and ACAS Xu benchmark networks. The obtained results are depicted iteratively in various tables and graphs throughout the article. In the sequel, we refer to the obtained results using our abstraction method, the method introduced in [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF], and the method presented in [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF]

A. Experiments on Random NNs

In this first part, we perform an evaluation study on a set of randomly generated networks with the odd monotone activation function Tanh, and the Relu activation function. The generated networks have five inputs, L = 20 hidden layers with n l = 30 nodes per layer, and one output. We apply our method to produce abstract networks of different sizes (different layer sizes): nl ∈ {25, 20, 15, 10} as presented in Table I.

Next, for an input X * ∈ [-1, 1], we apply a perturbation ϵ ∈ [0.01, 0.1] to generate input bounds [X * -ϵ, X * + ϵ], then, we compute the output bounds of the original model as well as of the abstract networks using the IBP algorithm.

Over 50 runs, we calculate the average of the output's upper bound, the abstraction time, the IBP computation time, and the total computation time which represents the sum of the abstraction time and output range computation time on the abstract networks. The obtained results on Tanh-NN are presented in Tables I andII. Furthermore, we depict these results graphically in Figs. 7 and8. For Relu-NN, we compare the results to the ones obtained using the abstraction method of Elboher et al. [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] and INN [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF]. Finally, Figs. 9-11 provide more details about these results. A thorough discussion of the obtained results is provided in Section V-C. The networks have 784 inputs and 10 outputs; however, the size and the number of hidden layers may change. In this work, we perform our experiments on the network tansig_200_100_50_onnx.onnx which has three hidden layers with 200, 100, and 50 nodes, successively. We select an image from the MNIST dataset and then we apply a perturbation (ϵ) on each pixel using the L ∞ norm [START_REF] Huang | A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability[END_REF]. Next, we calculate the output range of the network using the IBP algorithm. Similarly, using the same input image and perturbation ϵ, we calculate the average of the output range of the reduced models over 50 runs. We also calculate the average of the IBP computation time for the original and reduced models and the average of the abstraction time.

B. Experiments on MNIST and ACAS Xu Benchmarks

Figs. 12 and 13 summarize the obtained results. Since the hidden layers do not have the same number of nodes, the X -axis in Figs. 12 and 13 represents the percentage of the remaining nodes after abstraction. For instance, the value 0.9 means that the number of the nodes in each hidden layer of the abstract network has been reduced by 10% (180, 90, and 45, successively). 2) ACAS Xu: We consider the ACAS Xu networks as a case study to evaluate our method on realistic Relu-NN. The benchmark ACAS Xu is an airborne-collision avoidance system that has 45 networks [START_REF] Julian | Policy compression for aircraft collision avoidance systems[END_REF]. These networks are trained to provide advisories for an unmanned aircraft (ownership) to avoid a collision with another aircraft (intruder). Each network has seven inputs of sensor measurements, such as the speed of the ownership and the intruder, the distance between them and their directions, and so on. The network processes these inputs and returns five outputs that are scores of a possible advisory for the ownership: clear-of-conflict, strong/weak turn to the left, or strong/weak turn to the right.

For a given network and inputs' constraints of a specific property, 6 we compute the corresponding output range on the original network as well as on the generated abstract networks using the three methods, namely, our method (INNAbstract), INN [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF], and the technique presented in Elboher et al. [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF]. Over 50 runs, and for each network, we calculate the output upper bound average, the average of the IBP computation time, the abstraction time, and the total computation time. The results are shown in Figs. 141516.

Through the performed experiments, we can observe that the computation time values obtained using Elboher et al.'s method were excessively high, making it challenging to compare the original network with the abstract networks generated using the INNAbstract and INN methods. For a comprehensive comparison, we include

C. Discussion

As illustrated in Figs. 8, 10, 11, 12, 14, and 15, decreasing the size of the network (i.e., reducing the number of the 6 In this article, we used the property φ 5 presented in [START_REF] Katz | Reluplex: An efficient SMT solver for verifying deep neural networks[END_REF], and the network ACASXU_experimental_v2a_1_1.nnet. remaining nodes) by performing more abstraction leads to a linear increase in the abstraction time and a significant decrease in the IBP computation time. As a result, the total computation time, defined as the sum of the abstraction time and the IBP computation time, is also decreased. Additionally, the IBP algorithm is always faster on the abstract networks than on the original ones. With the exception of the abstract networks that are generated using Elboher et al., the total computation time on the abstract networks of INNAbstract and INN is consistently lower than the computation time on the original ones, especially when the abstraction degree is significant [see Figs. 11(a) and 15(a)]. Moreover, the computation time of INNAbstract is always smaller than that of INNs. For example, in Fig. 15(a) when the number of the remaining nodes is 10, which represents a reduction of the original network's size by 80%, the whole process on the abstract models obtained using INNAbstract (abstraction + IBP) is two times faster than the IBP on the original model.

Moreover, all three model reduction methods exhibit similar IBP computation times, which decrease as the size of the abstract networks decreases. This can be explained by the fact that the IBP algorithm is performed on networks of the same size (same remaining nodes). However, by comparing upper bound of the output. Furthermore, when focusing on the output range results of the three abstraction methods, we can see that the output range's upper bounds of abstract networks obtained using INNAbstract are generally smaller than the output ranges of those obtained using Elboher et al. [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] and INNs [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF]. Specifically, INNAbstract significantly outperforms Elboher et al. considering the different sizes of the abstract networks. Although the INN abstraction method initially shows slightly better performance when only a few neurons are merged, its performance drops drastically as the abstraction becomes more intensive (more neurons are merged), where the output range of the obtained abstract networks increases rapidly. In contrast, we can notice that the output range on abstract networks obtained using INNAbstract exhibits a slow increase with the number of remaining nodes, and INNAbstract outperforms the INN method when significant abstraction is applied.

In Fig. 13, we can observe that the output range of the abstract models is fairly close to the output range of the original one. Interestingly, the output's upper bound of different abstract networks does not change while varying the number of the remaining nodes. This is potentially related to the behavior of Tanh with large (resp. small) values, where the slope is almost null and the output of Tanh is basically 1 (resp. -1).

The main conclusion through these series of experiments is that: while the IBP computation time decreases, the abstraction time and the output range related to INNAbstract models exhibit a linear and slow increase with the number of merged nodes. Furthermore, we can observe that the total computation time (including both the abstraction and output range computation) on the abstract networks obtained using INNAbstract is consistently lower than the computation time on the original networks. Furthermore, according to the conducted experiments and the obtained results, INNAbstract significantly outperforms Elboher et al. [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] and INN [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] approaches in the sense that it produces tighter output bounds in less time. This highlights the effectiveness of INNAbstract in reducing the computation time, thus allowing for faster analysis and operations on NN.

It is worth recalling that the IBP is a very fast algorithm and allows for calculating an overapproximation of the outputs. Thus, the gain in precision and computation time will be more significant with other more precise methods.

D. Heuristic's Improvement

The objective of this section is to assess the performance of our model reduction method when combined with the proposed heuristic for node selection (Algorithm 5). To achieve this, we conduct a series of experiments on a set of randomly generated Relu-NN using two node selection strategies: random selection and heuristic-based selection. Namely, we generate various networks with different sizes by varying the number of layers L and the number of nodes on each layer n l to examine their impact on the heuristic's performance. More details about the generation of these networks are given in Section V-A. Next, we calculate the output range of the obtained abstract networks and we determine the improvement rate (I rate ) in terms of precision using the proposed heuristic. This is done by calculating the percentage of the difference between the output range with respect to the output range of the abstraction method with the random nodes selection using the following formula: where U rand and U heuris are the upper bounds of the abstract network using INNABstract with the random and heuristicbased strategy for node selection, respectively. Fig. 17 depicts the obtained results, where Fig. 17 As shown by the results presented in Fig. 17, the combination of the proposed heuristic with INNAbstract can enhance the precision of the generated abstract networks. Moreover, the performance of the heuristic depends on the number of layers and hidden nodes in the initial network. Specifically, the proposed heuristic performs better with large networks, since the population from where the nodes are selected is large, thus the algorithm has more options.

I rate = U rand -U heuris U rand × 100
To illustrate the improvement in terms of precision through the proposed heuristics, we chose the configurations L = 20 and n l = 40 to generate a random network of 20 layers, with 40 nodes in each hidden layer. We then compute the output range and the abstraction time of the resultant abstract networks, employing both random and heuristic selection strategies.

As depicted in Fig. 18(a), the output range obtained using INNAbstract in combination with the proposed heuristic is tighter compared to the output range obtained using INNAbstract with a random selection of nodes. Furthermore, the improvements become more significant when more nodes are merged. However, it is important to note that achieving these improvements comes at the cost of increased abstraction time, as illustrated in Fig. 18(b).

Finally, it is worth noticing that we have conducted the same experiments on Tanh-NN; however, the improvement rate remains negligible. This is mainly due to the nature of the Tanh function (illustrated by its hyperbolic behavior) which tends to push the output value to either end of the curve (1 or -1) due to its S-like shape, that is, in the region close to zero, if we slightly change the input value, the respective changes in the output are very large and vice versa.

VI. CONCLUSION

In this work, we presented INNAbstract, a model reduction method for NNs. The approach consists of merging nodes of the same layer and provides a formula to calculate the new weights ensuring that the output range of the original model is always included within that of the abstract one. The proposed approach supports NNs with Relu and oddmonotone activation functions, including Tanh and Bipolar Sigmoid. With the aim of enhancing the performance of the approach, we proposed a heuristic for node selection based on some features of the network's nodes. Furthermore, we carried out a series of experiments using randomly generated NNs in addition to some benchmarks to assess the performance of the proposed method. We also compared the performance of our method to other relevant works from the literature.

The results of the experimental study show that INNAbstract can effectively be used to reduce the size of large networks, leading to reduced computation costs, while providing formal guarantees that the generated abstract networks overapproximate the original ones. Additionally, the proposed heuristic allows for significantly improving the precision of the abstraction method. From the obtained results, the manipulation operations on abstract networks are clearly faster. However, there is a tradeoff between abstraction, precision, and computation time. Furthermore, on the basis of the conducted experiments, INNAbstract outperforms the other relevant abstraction methods presented in Elboher et al. [START_REF] Elboher | An abstraction-based framework for neural network verification[END_REF] and Prabhakar and Afzal [START_REF] Prabhakar | Abstraction based output range analysis for neural networks[END_REF] in terms of both precision and computation time.

We plan to pursue this work in different directions. First, we want to integrate our model reduction method with This article has been accepted for inclusion in a future issue of this journal. Content is final as presented, with the exception of pagination.

Authorized licensed use limited to: IFSTTAR. Downloaded on October 06,2023 at 07:03:30 UTC from IEEE Xplore. Restrictions apply. more precise NN-bound propagation and verification methods. Moreover, we will investigate the abstraction approach to support additional activation functions. Finally, we intend to explore more heuristics for node selection toward generating more precise abstract networks.

APPENDIX

We provide in this section the formal proof of the soundness of our proposed method for NNs with odd and monotone activation functions, namely Proposition 1. We would like to note that, due to page limitations, the proof of Proposition 3 is omitted from this version of the article.

PROOF OF PROPOSITION 1

Proposition 1: Let N be an NN. Assume that the activation function of N is odd and monotone. Let Ŝi = (S i \ Ŝ) ∪ {ŝ} Be the set of nodes after applying the abstraction on S i . Then, we have ∀v(S i-1 ), v(S i+1 ) ⊆ v( Ŝi+1 ).

■

In Proposition 1, v(S i+1 ) ⊆ v( Ŝi+1 means that v(s i+1, j ) ∈ v(ŝ i+1, j ), ∀ j ∈ {1, 2, . . . , m|}, where m = |S i+1 | = | Ŝi+1 |. Proposition 1 considers merging many nodes on a hidden layer l i , and for the sake of simplicity, we provide the proof of merging two nodes. The generalization of this proof by considering multiple nodes can be done following the same steps.

Assume that we want to merge two hidden nodes s 1 and s 2 of a hidden layer l i , such that l i-1 , l i , and l i+1 all have an odd and monotone activation function, and let ŝ denotes the obtained abstract node.

We denote by a k (resp. b k ) the incoming weights of s 1 (resp. s 2 ) from node s i-1,k ∈ S i-1 a k = w(s i-1,k , s 1 ) b k = w(s i-1,k , s 2 ) and we denote by c j (resp. d j ) the outgoing weight of s 1 (resp. s 2 ) for each node s i+1, j ∈ S i+1 , that is, c j = w(s 1 , s i+1, j ) d j = w(s 2 , s i+1, j ).

The weights of the remaining edges connecting other nodes than s 1 and s 2 (s ∈ S i \ {s 1 , s 2 }) to each node s i+1, j ∈ S i+1 are defined as follows:

w(s, s i+1, j ) = w s,s j .

We denote by ŝ the obtained abstract node after merging s 1 and s 2 using Algorithm 2. The new abstract layer is denoted as Ŝi = ŝ ∪ {S i \ {s 1 , s 2 }}. For clarity, we use v k instead of v i-1,k . Since the activation function α is monotone and odd, that is, ∀x ∈ R : α(-x) = -α(x) and where z i+1, j (resp. ẑi+1, j ) is the value of s i+1, j (resp. ŝi+1, j ) before applying the activation function α, and m = |S i-1 | is the number of nodes of layer l i-1 and ŵk = [ ŵl k , ŵu k ] is the abstract weight connecting each node s k ∈ S i-1 to the abstract node ŝ ∈ Ŝi as defined in Algorithm 2. The main results is to prove that v i+1, j ∈ vi+1, j .

∀x 1 , x 2 ∈ R : x 1 ≤ x 2 ⇒ α(x 1 ) ≤ α(x 2 ).
By definition of ŵk , we have

ŵl k v k ≤ sign(c j )a k v k ≤ ŵu k v k , if v k ≥ 0 ŵu k v k ≤ sign(c j )a k v k ≤ ŵl k v k , Otherwise.
Two cases need to be proved, v k ≥ 0 and v k < 0. We provide below a detailed proof for the case v k ≥ 0. The proof of the second case, that is, v k < 0, is omitted and it is done similarly by just inverting the lower and upper bounds of ŵk when multiplying it by v k . Assume that v k ≥ 0, multiplying the aforementioned inequality by sign(c j ), we obtain

         if c j ≥ 0: sign(c j ) ŵl k v k ≤ sign(c j )sign(c j )a k v k ≤ sign(c j ) ŵu k v k Otherwise:
sign(c j ) ŵu k v k ≤ sign(c j )sign(c j )a k v k ≤ sign(c j ) ŵl k v k .

The proof contains two parts: c j ≥ 0 and c j < 0. Here, we provide details of the proof for the first case: sign(c j ) ≥ 0. The proof of the other case (sign(c j ) < 0) can be performed following the same logic, using the fact that α is odd, so α(sign(c j ) × x) = sign(c j ) × α(x), and that we have sign(c j ) × c j = |c j |.

For sign(c j ) ≥ 0 and by taking the sum over all k, we have

Summing inequalities ( 14) and [START_REF] Leofante | Automated verification of neural networks: Advances, challenges and perspectives[END_REF] with the remaining incoming nodes values to s i+1, j ∈ S i+1 \ {s 1 , s 2 }, we obtain

And since α is monotone, by applying the activation α on the inequality ( 16), we obtain v(ŝ i+1, j ) l ≤ v(s i+1, j ) ≤ v(ŝ i+1, j ) u . Finally, we have v i+1, j ∈ vi+1, j ∀ j ∈ {1, . . . , n}.

□

ACKNOWLEDGMENT

This research work contributes to the French collaborative project TASV (autonomous passengers service train), with Railenium, SNCF, Alstom Crespin, Thales, Bosch, and SpirOps. It was carried out in the framework of IRT Railenium, Valenciennes, France, and, therefore, was granted public funds within the scope of the French Program "Investissements d'Avenir."

Manuscript received 23

 23 December 2022; revised 31 July 2023; accepted 11 September 2023. (Corresponding author: Fateh Boudardara.)

Fig. 1 .

 1 Fig. 1. Example of an NN.

Fig. 2 .

 2 Fig. 2. Example explaining how to replace the bias vector with a weight vector. (a) Network with a bias vector. (b) Equivalent network to the one presented in (a) where biases are replaced by weights, s.t. v(S i-1,b ) = 1.

Fig. 3 .

 3 Fig. 3. Example of an INN of three layers.

  Pre(x * ) holds true and Post(y * ) is false.

Definition 4 :

 4 A network N with its associated function N : R |S 0 | → R |S n | is an overapproximation of a network N if the following relation is fulfilled:

Fig. 4 .

 4 Fig. 4. Example explaining the main idea of the proposed approach, where the incoming weight to the abstract node ŝ is: ŵl = min {sign(c) × a, sign(d) × b} and ŵu = max{sign(c) × a, sign(d) × b}. (a) Original network. (b) Abstract network.

Fig. 5 .

 5 Fig. 5. Example of the abstraction method applied on two neurons of a hidden layer l i . For v(s i-1,1 ) = 1, then we have v(s i+1,1 ) = 0 and v(s i+1,2 ) = 5, v(ŝ i+1,1 ) = [-10, 15] and v(ŝ i+1,2 ) = [-4, 6]. Hence, the overapproximation is fulfilled, since v(s i+1,k ) ∈ v(ŝ i+1,k ) for k = 1, 2. (a) Network N : s i p and s iq are to be merged. (b) Obtained abstract model N .

  end procedure where |.| is the absolute value, and sign is the sign function defined as: sign : R → {-1, 1} sign

Fig. 6 .

 6 Fig. 6. Counterexample of applying Algorithm 2 on a Relu-NN. Assume that v(s 1 ) = 2, then v(s 4 ) = 8 and v(ŝ 4 ) = [12, 18], hence v(s 4 ) ̸ ∈ v(ŝ 4 ). (a) Network N : s 2 and s 3 are to be merged. (b) Obtained abstract model N . Algorithm 3 Pseudo-Algorithm of the Abstraction Method Applied on One Relu Hidden Layer l i 1: procedure ABSTRACT1RELULAYER(N , i, Ŝ ) ▷ N : the network, i : the layer's number 2:

ŝ 4 :

 4 for s i-1,k ∈ S i-1 do 5: calculate ŵ(s i-1,k , ŝ) using Equation8and determine w * i+1, j 6:if Equation 12 is true then 7:

Algorithm 4 5 :

 45 Pseudo-Algorithm of INNAbstract for Relu-NN 1: procedure ABSTRACT(N , selectStrategy) 2: N ← duplicate(N ) ▷ Initialize the abstract network 3: for i ← 1 to n -1 do ▷ Explore all layers 4: Ŝ ← Select N odes( N , i, select Strategy) Abstract1Relu Layer ( N , i, Ŝ)

Fig. 7 .

 7 Fig. 7. Output range results on Tanh-NN.

Fig. 8 .

 8 Fig. 8. Total computation time, IBP, and abstraction time results on Tanh-NN. (a) Total computation time. (b) IBP computation time. (c) Abstraction time.

Fig. 9 . 1 )

 91 Fig. 9. Output range results on Relu-NN.

  , as INNAbstract, Elboher et al., and INN, respectively. The results obtained on the original initial network are denoted by original.

Fig. 10 .

 10 Fig. 10. Total computation time, IBP, and abstraction time results on Relu-NN. (a) Total computation time. (b) IBP computation time. (c) Abstraction time.

1 )

 1 MNIST: In this second series of experiments on Tanh-NN, we use the ONNX networks trained on the dataset of handwriting digits, namely MNIST. The networks are available on the VNN 2020 Competition's GitHub repository.5

Fig. 11 .

 11 Fig. 11. Total computation time and the abstraction time for INNAbstract and INN on Relu-NN. (a) Total computation time. (b) Abstraction time.

Fig. 12 .Fig. 13 .

 1213 Fig. 12. Total computation time, IBP, and abstraction time results on MNIST Tanh-NN. (a) Total computation time. (b) IBP computation time. (c) Abstraction time.

  Figs. 11 and 15 to display the computation time values for the INNAbstract, INN, and original network on the Relu-NN and ACAS Xu benchmark, respectively.

  the abstraction time of INNAbstract to the two other methods [shown in Figs. 10(c) and 14(c)] and more specifically to INNs [see Figs. 11(b) and 15(b)], we can observe that INNAbstract is faster. Namely, when considering the same number of abstract neurons, INNAbstract generates abstract networks in less time compared to the other methods. We can also observe that the Elboher et al. method is computationally expensive compared to INNAbstract and INN. This can be attributed to the preprocessing phase, which involves classifying neurons into different categories and potentially splitting numerous neurons. As a result, the network to be abstracted may have a larger size than the original one, which leads to increasing the abstraction time, significantly. Additionally, the abstraction time using our method increases linearly, and hence much more slowly compared to INNs [see Figs. 11(b) and 15(b)]. Moreover, the total computation time of INNAbstract is less than the total computation time of both methods. This clearly illustrates the efficiency of our method, which can handle larger networks without a significant increase in abstraction time. Figs. 7, 9, 13, and 16 show the results of the output range of the different abstractions. A general observation from Figs. 7, 9, and 16 shows that decreasing the size of the abstract network, which leads to less precise network, increases the

Fig. 14 .Fig. 15 .Fig. 16 .

 141516 Fig. 14. Total computation time, IBP, and abstraction time results on ACAS Xu Relu-NN. (a) Total computation time. (b) IBP computation time. (c) Abstraction time.

Fig. 17 .

 17 Fig. 17. Graph representing the improvement of the output range using the proposed heuristic. Results on networks with different numbers of (a) layers, L = 20 and L = 40, and (b) nodes per layer, n l = 30 and n l = 40.

  (a) represents the results on networks with different layers number (L = 20, L = 40) and the same number of nodes on hidden layers (n l = 30), and Fig. 17

  (b) represents the results of networks whose layers number is set to 20 (L = 20) and have different hidden layer sizes (n l = 30, n l = 40).

Fig. 18 .

 18 Fig. 18. Output range and abstraction time results on Relu-NN with random and heuristics-based selection strategy. (a) Output range (upper bound). (b) Abstraction time.

For each j ∈ {1, 2 ,

 2 . . . , |S i+1 |}, we have v i+1, j = α(z i+1, j )

  ŵl k ≤ sign(c j )a k ≤ ŵu k ŵl k ≤ sign(d j )b k ≤ ŵu k ∀k = {1,2, . . . , m}, ∀ j ∈ {1, 2, . . . , n}. Thus, we have

k v k . ( 13 )

 13 j ) ŵu k v k .And since α is monotone increasing, we haveα j ) ŵu k v k .Since α is odd, we have α(sign(c j ) × x) = sign(c j ) × α(x), thus the previous inequality is equivalent to sign(c j )α Multiplying equality (13) by c j implies|c j | × α m k=1 ŵl k v k ≤ c j × α m k=1 a k v k ≤ |c j | × α m k=1 ŵu k v k .(14)Recalling that sign(c j ) × c j = |c j |. The same reasoning remains valid when we replace a k by b k and c j by d j|d j | × α m k=1 ŵl k v k ≤ d j × α

(

  |c j | + |d j |) × α m k=1 ŵl k v k + s∈S i \s1,s2 w s,s j v(s) ≤ c j × α m k=1 a k v k +d j × α m k=1 b k v k + s∈S i \s1,s2 w s,s j v(s) ≤ (|c j | + |d j |) × α m k=1 ŵu k v k + s∈S i \s1,s2w s,s j v(s).

  Pseudo-Code of the Abstraction Method Applied on One Hidden Layer l

	6:	end for
	7:	return	N
	8: end procedure
	Algorithm 2

i 1: procedure ABSTRACTONELAYER(N , i, P i ) ▷ P i a set containing the partitions 2:

for every subset Ŝ in P i do 3:

create a node ŝ 4:

TABLE I OUTPUT

 I RESULTS ON Tanh-NN, L = 20 LAYERS TABLE II ABSTRACTION TIME AND TOTAL COMPUTATION TIME

ON Tanh-NN, L = 20 LAYERS

In the sense that its output is closer to the output of the original network.

This article has been accepted for inclusion in a future issue of this journal. Content is final as presented, with the exception of pagination.Authorized licensed use limited to: IFSTTAR. Downloaded on October 06,2023 at 07:03:30 UTC from IEEE Xplore. Restrictions apply.

A database of handwritten digits, available in http://yann.lecun.com/ exdb/mnist/

Available in: https://github.com/verivital/vnn-comp/tree/master/2020/ NLN/benchmark/mnist/tanh