Neuron Similarity-Based Neural Network Verification via Abstraction and Refinement

1 Introduction

Deep neural networks (DNNs) have been widely used in safety-critical domains owing to their exceptional performance, with applications spanning image recognition [Szegedy et al., 2016], autonomous driving [Kiran et al., 2021], and natural language processing [Wolf, 2020]. However, the inherent lack of robustness renders DNNs susceptible to adversarial attacks, wherein minor perturbations to otherwise correct inputs can precipitate significant errors [Athalye et al., 2018; Zheng-Fei et al., 2022; Yang et al., 2023]. Consequently, prior to deployment in safety-critical environments, it is imperative to ensure that neural networks have expected output behavior, thus guaranteeing their reliability in these applications.

†Corresponding author.

Given the imperative need for reliable AI systems in safety-critical domains, researchers have been actively exploring various approaches to enhancing the trustworthiness of DNNs. A particularly promising direction has emerged in the formal methods community, which develops verification techniques [Katz et al., 2019; Henriksen and Lomuscio, 2020; Liu et al., 2021; Kouvaros and Lomuscio, 2021; Lechner et al., 2022] capable of automatically proving the satisfaction of specified input-output specifications for DNNs. However, DNN verification is generally NP-complete with respect to the size of the network model [Sälzer and Lange, 2022], which is computationally intensive even for simple specifications and networks. Consequently, despite recent advancements in verification techniques, the size of verifiable network models remains a significant limiting factor. This computational complexity necessitates the development of more efficient verification strategies to broaden the applicability of formal methods to larger-scale neural networks.

To address this challenge, we propose a novel abstractionrefinement verification method for DNNs based on neuron similarity. For efficient verification, the idea is to define similarity metric between neurons and merge similar neurons into one, so that the network N to be verified is abstracted into a smaller network ¯N. If ¯N satisfies the specified safety property, it indicates that N also satisfies it. Conversely, if ¯N violates the property, the verification process yields a counterexample cex and its genuineness is checked. In case cex is a genuine counterexample, it indicates that the original network N violates the safety property; otherwise cex is a spurious counterexample and the abstract network ¯N is up to refinement. The refinement process increases both the size and accuracy of the abstract network to exclude the spurious cex, followed by iterative verification. This process adopts the counterexample guided abstraction refinement (CEGAR) paradigm [Clarke et al., 2000], which is a promising technique for enhancing formal verification efficiency.

It is worth pointing out that the proposed method is generic and can be integrated with existing verification methods to enhance their efficiency. To evaluate the method, we implement it as a tool named ARVerifier and integrate it with state-of-the-art verifiers α, β-CROWN [Xu et al., 2020; Wang et al., 2021; Shi et al., 2023], Verinet [Henriksen and Lomuscio, 2020], and Marabou [Katz et al., 2019]. We apply ARVerifier to verify the safety properties of the ACAS Xu and MNIST benchmark datasets. Experimental results demonstrate that the method reduces verification time by up to 11.61%, 18.70%, and 12.20%, respectively, for these verifiers. Moreover, ARVerifier improves efficiency by 26.64% and 46.87%, respectively, compared to existing tools CEGAR-NN [Elboher et al., 2020] and NARv [Liu et al., 2024] that support structure-oriented CEGAR-based verification. The main contributions of this paper are summarized as follows.

• We propose an abstraction approach for DNNs that calculates neuron similarity by comprehensively considering interval, specific neuron value, weight, and layer depth influence. The approach minimizes accuracy loss in the network while reducing the number of identical neurons.
• We introduce a refinement approach that determines neuron restoration priority by thoroughly considering the values of neurons corresponding to counterexamples, along with their weights and layer-depth influence. The approach maximizes the restoration of network accuracy while increasing the number of identical neurons.
• We implement the proposed abstraction-refinement method as a tool named ARVerifier, and integrate it with three existing best-performed DNN verification engines: α, β-CROWN, Verinet, and Marabou. Extensive evaluations across multiple datasets demonstrate ARVerifier's advantage in verification efficiency.

2 RelatedWork

Formal verification of neural networks can be broadly categorized into two main approaches: complete and incomplete methods [Liu et al., 2021]. Complete methods precisely encode the network, transforming the verification problem into a global optimization task. While these methods guarantee definitive results, they encounter significant scalability challenge when applied to larger networks. Conversely, incomplete verification methods provide improved scalability but may produce spurious counterexamples, resulting in a lack of guaranteed deterministic outcomes.

Complete methods typically employ rigorous encoding techniques such as mixed integer linear programming (MILP) and satisfiability modulo theory (SMT/SAT). Both MILPbased [Lomuscio and Maganti, 2017; Tjeng et al., 2017; Weng et al., 2018; Akintunde et al., 2018; Botoeva et al., 2020] and SAT/SMT-based [Ehlers, 2017; Liu et al., 2021; Katz et al., 2019; Jia et al., 2023] approaches leverage solvers to address verification constraints. Recent studies [Henriksen and Lomuscio, 2020; Henriksen and Lomuscio, 2021; Wang et al., 2021; Hashemi et al., 2021] have introduced symbolic propagation and input refinement techniques to determine nonlinear neuron bounds within the network model.

These output bounds serve as constraints for linear programming problems, effectively reducing the complexity introduced by nonlinear neurons during the verification. Most of these work focuses on deep neural networks (DNNs) with ReLU activation functions. While these methods offer completeness, they face scalability limitations. Our work addresses this scalability challenge by reducing the network size, thereby enhancing the applicability of these complete DNN verification techniques to larger networks.

Incomplete verification methods [Ma et al., 2018; Pei et al., 2017; Tian et al., 2018; Yang et al., 2022] encompass approaches that employ heuristic search or other dynamic analysis techniques to identify counterexamples that violate safety properties. While effective in finding violations, these methods cannot definitively prove that safety properties hold. Another category of incomplete methods, which includes our approach, leverages abstraction techniques. Existing abstract interpretation-based methods [Gehr et al., 2018; Mirman et al., 2018; Li et al., 2019; Yang et al., 2021] utilize abstract domains (e.g., interval, zonotope, and polyhedra) to approximate constraints from input to output layers, providing relatively accurate output range estimations. In contrast to these methods, the counterexample-guided abstraction and refinement (CEGAR) based approach employed in our work is founded on structural properties of DNNs rather than on computation.

Our work is closely related to CEGAR-NN [Elboher et al., 2020] and NARv [Liu et al., 2024]. CEGAR-NN introduces the structure-oriented CEGAR approach for neural network verification, but its effectiveness is limited due to a preprocessing step that quadruples the network size and an abstraction process that neglects input specifications. NARv improves upon this by only doubling the network size during preprocessing and considering input specifications in neuron merging. However, its neuron merging calculations remain insufficiently comprehensive, and the dependency graphs also constrain refinement flexibility. Unlike these works, our method is not a simple modification or extension but introduces key innovations in both abstraction and refinement processes. While adopting the same preprocessing step as theirs, our method considers not only neuron weights of the current layer but also specific inputs and the DNN hierarchy during abstraction, enabling a more comprehensive and accurate representation of neuron similarity. Furthermore, we employ an adversarial attack-based method for input set generation, effectively mitigating the impact of random generation on initial abstraction, which is a limitation in both previous methods. These enhancements, rooted in principled improvements rather than incremental adjustments, collectively contribute to improved efficiency and less accuracy loss, allowing for more effective verification of larger neural networks.

3 Preliminary

3.1 Deep Neural Network

A deep neural network N consists of n + 1 layers: one input layer, n - 1 hidden layers, and one output layer. Each layer i contains si neurons, with vi,j denoting the value of the j-th neuron. The output vector of the i-th layer is represented as Vi = [vi,1, . . . , vi,si ]T . As the input x propagates through the network, each layer computes a weighted sum and applies an activation function. In this study, we focus on the rectified linear unit (ReLU) activation function, defined as ReLU(x) = max(0, x). For each layer i (i > 1), a weight matrix Wi ∈ Rsi×si-1 and a bias vector Bi ∈ Rsi are associated. The value of the i-th layer is computed as:

This computation proceeds layer by layer until the network output N(x) = Vn is obtained. The weight connecting neurons vi-1,k and vi,j is denoted as w(vi-1,k, vi,j). For each neuron vi,j, we define its upper and lower bounds [Singh et al., 2019] as ub(vi,j) and lb(vi,j), respectively, such that lb(vi,j) ≤ vi,j ≤ ub(vi,j).

3.2 Neural Network Verification

Given a DNN N, an input constraint P, and an output constraint Q, the verification problem φ = ⟨N, P,Q⟩ aims to determine whether there is an input x satisfying P that leads to an output y = N(x) satisfying Q, where P defines the input space and Q represents the negation of the desired safety property. This is to check whether there is a counterexample that violates the safety property. Similar to existing studies [Sälzer and Lange, 2022; Ruan et al., 2018; Elboher et al., 2020], we assume the input constraint is linear, the output layer contains a single neuron y, and the output constraint takes the form y > c for a constant c. For verification problems φ1 = ⟨N, P,Q⟩ and φ2 = ⟨ ¯N, P,Q⟩, ¯N is an over-approximation of N if N(x) ≤ ¯N(x) for any x satisfying P. Consequently, if φ2 is SAFE (UNSAT), then φ1 is also SAFE (UNSAT), since ¯N(x) ≤ c ⇒ N(x) ≤ c. An input x satisfying P is a counterexample for N if N(x) > c. However, if x is a counterexample for ¯N but N(x) ≤ c, then x is called a spurious counterexample for N.

3.3 CEGAR-Based Neural Network Verification

Algorithm 1 specifies the general neural network verification method based on CEGAR. Given a verification problem ⟨N, P,Q⟩, the algorithm returns SAFE if the safety property is satisfied, or UNSAFE along with a counterexample cex.

To solve the verification problem ⟨N, P,Q⟩, the first step is to construct an abstract neural network ¯N derived from the original network N with some abstraction approach. Usually, ¯N is simpler than N so as to enhance verification efficiency. Lines 2-4 verify ¯N using the V erify function, which represents some verification method. If the result is SAFE, the algorithm returns SAFE, indicating that N is also safe. If the verification result is UNSAFE, the algorithm refines ¯N through a loop (Lines 5-12). In each iteration, it extracts a counterexample cex and checks if it applies to the original network N. If so, it returns UNSAFE along with the counterexample. If cex is a spurious counterexample for N, it is used to refine ¯N, making the abstract network approximate the original network with cex no more a counterexample. If no applicable counterexample for N is found by the end of the loop, the algorithm returns SAFE, confirming that N is safe under the given conditions.

Algorithm 1 CEGAR-Based Neural Network Verification Algorithm

Input: ⟨N, P,Q⟩

Output: SAFE / UNSAFE

• 1: Build an abstract DNN ¯N fromN.
• 2: if V erify( ¯N, P,Q) is SAFE then
• 3: return SAFE
• 4: else
• 5: while V erify( ¯N, P,Q) is UNSAFE do
• 6: Extract counterexample cex.
• 7: if cex is a counterexample for N then 8: return UNSAFE, cex
• 9: else
• 10: Refine ¯N using the cex.
• 11: end if
• 12: end while
• 13: end if
• 14: return SAFE

4 Methodology

To address the limitation of existing neural network verification techniques, we propose an abstraction-refinement verification method for DNNs based on neuron similarity, aiming to reduce the size of the verification network and thereby accelerate the verification process. This section provides details of the method, complementing and improving upon the key steps in Algorithm 1.

Specifically, the process of the verification method is shown in Figure 1. First, we preprocess the original network to be verified by classifying its neurons and converting it into an equivalent network to facilitate subsequent abstraction operations. Then, we employ adversarial search to generate an input set. This input set can be used to limit the number of abstraction operations and calculate neuron similarity. After that, by calculating the similarity between pairs of neurons of the same type, we select the most similar neurons and merge them into one neuron to reduce network size while minimizing accuracy loss. The neuron similarity calculation comprehensively considers various factors including interval similarity, value similarity under the same input, and merging impact on the network. This merging process continues until it violates the constraints of the adversarially generated input set, resulting in an abstract network for verification. When a spurious counterexample appears, we determine which neuron to restore from the merged neurons by evaluating both the neuron's value corresponding to the counterexample's input and the impact of its restoration on the network. The proper merged neuron is restored and the network is refined, until a definitive verification result is obtained. Overall, by effectively reducing the network size through abstraction while preserving the model's critical behaviors and decision boundaries, the method can significantly enhance verification efficiency, particularly for complex neural networks. The key steps of the method are detailed as follows.

4.1 Network Preprocessing

The abstraction process aims to reduce the number of neurons by merging neurons within the same layer. To make this process feasible, we first preprocess the original network N. Specifically, we transform N into an equivalent network N ′ , where equivalence means the same output for the same input. In N ′ , neurons are classified into inc (increasing effect) and dec (decreasing effect) neurons. An inc neuron indicates that increasing its value leads to an increase in the network's final output, while a dec neuron has the opposite effect. Recall that the output layer consists of a single neuron. Neurons of the same type can be merged, and the resulting node retains the original classification.

The process of converting N into an equivalent network N ′ begins with designating the single output y of the last layer as the inc type, and then proceeds layer by layer backwardly. As illustrated in Figure 2, once all neurons in the (i + 1)-th layer have been classified, each neuron vi,j in the i-th layer is split into an inc neuron v+ i,j and a dec neuron vi,j , both inheriting the incoming edges of vi,j. For outgoing edges, v+ i,j retains the positive weighted edges from vi,j to the inc neurons and the negative weighted edges to the dec neurons of the (i + 1)-th layer, with the remaining outgoing edges set to 0. Conversely, vi,j retains the positive weighted edges from vi,j to the dec neurons and the negative weighted edges to the inc neurons of the (i + 1)-th layer, with the other outgoing edges set to 0. The specific operations are defined by the following equations.

Intuitively, when the value of the neuron v+ i,j increases, it

(c) Processing Neuron v1,1

Figure 2: Construction of Initial Abstract Network

affects the subsequent layer in two ways: it increases the values of all connected inc neurons and decreases the values of connected dec neurons. Both effects contribute to an increase in the final output y, which ensures v+ i,j is an inc neuron. On the contrary, vi,j is an dec neuron whose increase always leads to a decrease in the final output y.

4.2 Input Set Generation

Prior to the abstraction phase, it is crucial to control the granularity of the initial abstraction. On the one hand, an overly aggressive abstraction with numerous abstracted neurons results in a coarse network, requiring too many refinement iterations to yield definitive verification results. On the other hand, insufficient abstraction fails to effectively reduce the network scale, potentially increasing verification time. The traditional method [Elboher et al., 2020] for controlling abstraction granularity involves randomly generating an input set X = {x1, . . . , xn}, in which all inputs satisfy the input constraint P and their corresponding outputs satisfy the output constraint Q. The abstraction process is terminated when an input in the set no longer satisfies the corresponding property after an iteration. However, this method's effectiveness is highly variable due to the random nature of the input set generation. To address this limitation, we propose to apply an adversarial attack method, projected gradient descent (PGD) [Madry et al., 2017], to the original network N. The input set X is then formed using the inputs generated during the PGD iteration process. This method yields an input set closer to the decision boundary of the original network N, which is more effective in controlling the abstraction granularity and enhancing the quality of the initial abstraction. Specifically, the PGD-based method is expressed by the following equation:

where x0 is the initial input sampled from the input constraint P, xt is the input at Iteration t, α is the step size, and ΠP denotes the projection onto P . The effectiveness of this method will be demonstrated in the experimental section.

4.3 Abstraction

Having obtained an equivalent neural network N ′ from N, where each neuron is classified as either inc or dec, we perform a merging operation to construct an over-approximated network ¯N ′ . Consider two neurons vi,j and vi,k in the i-th layer, both classified as inc. Let vi-1,p and vi+1,q represent arbitrary neurons in the preceding and subsequent layers, respectively. The merging operation is specified as follows:

• delete neurons vi,j and vi,k along with their associated edges; and
• add a new neuron vi,m and assign the following values to the associated edges.

Intuitively, by employing the max operation in Equation (4), the newly formed neuron vi,m consistently produces an output greater than or equal to that of the original neurons vi,j and vi,k for any given input, as shown in Figure 3. Oppositely, when merging dec neurons, the max operation is replaced with the min operation.

A critical question that arises is how to select the optimal pair of neurons for merging. Our objective is to minimize the loss of network accuracy while reducing the network size. For this, we introduce the concept of neuron similarity. The similarity between two neurons, vi,j and vi,k, is quantified by three metrics: interval similarity, specific value difference, and weight difference. The three metrics are expressed by the following equations.

Interval Similarity (IS) is defined as the ratio of the intersection length to the union length of two intervals, while these intervals are calculated by [Singh et al., 2019]. The Specific Value Difference (SVD) is derived from the input set discussed in the previous section, calculating the difference between the output values of the two neurons for specific input values. The Weight Difference (WD) is computed as the sum of the weight differences between all neurons in the preceding layer and the merged neuron. The comprehensive similarity measure is expressed by the following equation.

Our approach to neuron similarity considers multiple factors. Higher similarity is attributed to neurons that exhibit smaller differences in their values for the same input, have more similar input edge weights, and possess larger overlapping regions in their upper and lower bound intervals. Additionally, we factor in the impact of layer depth. As errors introduced by merging hidden layer neurons tend to be amplified through layer-by-layer propagation, the cumulative effect of multiple neuron errors can significantly influence the output of network. Considering this phenomenon, we incorporate a 2i factor, which biases the merging process to proceed from the deeper layers towards the input. This strategy is not only more accurate compared to the simple backward layerby-layer merging but can also reduce time consumption by decreasing the number of interval calculations. Overall, this comprehensive approach ensures a balance between abstraction efficiency and network accuracy, making it effective to verify complex neural networks.

4.4 Refinement

As illustrated in Algorithm 1, the initial abstraction yields an over-approximation network ¯N ′ that may produce spurious counterexamples cex with ¯N ′ (cex) > c. To address this issue, we introduce a refinement process to eliminate spurious counterexamples, which is essentially the inverse of the abstraction. The process transforms ¯N ′ into another approximation network ¯N ′′ such that ¯N ′′ (cex) ≤ c. Moreover, for any input x, the refinement ensures that N(x) ≤ ¯N ′′ (x) ≤ ¯N ′ (x), where N is the original network.

Specifically, the refinement operation involves selecting a neuron vi,j from the abstract neuron ¯ vi,j ′ and reverting it to its pre-merged state, thereby reducing the network output according to a spurious counterexample cex. While abstraction aims to simplify the network, refinement seeks to restore network accuracy to eliminate spurious counterexamples, albeit at the cost of increasing the neuron count. The neuron selection in the refinement process is quantified by the following equation.

Here, ¯ vi,j ′ denotes the merged neuron, while vi,j represents a neuron in the initial network that was merged into ¯ vi,j ′ . The equation quantifies the impact on the network output when restoring vi,j from ¯ vi,j ′ . Since neurons preceding the i-th layer remain unaffected after the restoration, the product of the (i - 1)-th layer's value in the counterexample cex together with the weight difference of incoming edges before and after the restoration intuitively represents the impact of separating vi,j . In addition, the weight difference of outgoing edges before and after the restoration affects the output of the current layer. Finally, similar to the abstraction, the refinement process considers the influence of layer depth. However, to maximize the impact of restored neurons on the output, we tend to prioritize the restoration of neurons in earlier layers.

5 Experimental Evaluation

The proposed method has been implemented as a tool named ARVerifier (Abstraction and Refinement Verifier for neural networks). The tool is generic as its backend verification engine is flexible, allowing integration with any complete verification tool capable of finding out counterexamples for unsafe verification problems. To assess the performance of ARVerifier, we integrate three state-of-the-art complete tools as the backend verification engines: α, β-CROWN, Verinet, and Marabou.

5.1 Benchmarks and Experimental Configuration

The neural networks considered in the experiments are from the fully connected benchmarks used in the international verification of neural networks competition (VNN-COMP) [Brix et al., 2024; Brix et al., 2023], specifically the ACAS Xu and MNIST datasets.

ACAS Xu [Julian et al., 2016] consists of 45 ReLU-based DNNs for airborne collision avoidance, guiding aircraft steering based on sensor data. These networks, widely used in verification research, each have 5 inputs, 5 outputs, and 300 ReLU neurons in 6 layers. Our verification follows safety properties from [Katz et al., 2017], testing 4 properties across all 45 networks and 6 on a single network.

The MNIST [LeCun, 1998] dataset consists of handwritten digits 0-9, represented as 28×28 grayscale images. We employ three fully connected DNNs: MNIST2, MNIST4, and MNIST6, respectively comprising 2, 4, and 6 hidden layers, each with 256 ReLU neurons. Our verification assesses local adversarial robustness, testing 25 images with l∞ perturbations of 0.02 and 0.05.

Experiments are performed on a 64-bit Ubuntu 18.04 platform equipped with 64 GB of RAM and an Intel i77700 quad-core processor. All verification tools are implemented in Python 3.8. For the tools involving MILP solving, α, β-CROWN and Marabou use Gurobi 9.1, while Verinet uses Xpress 9.0 as the backend solver. Due to its feature, α, β-CROWN is executed with an additional NVIDIA TITAN RTX GPU with 24 GB memory. Besides, we impose a 30-minute timeout for each verification problem, while maintaining default values for other parameters.

5.2 Performance Enhancement: ARVerifier's Impact on Existing Verifiers

We first evaluate ARVerifier's efficacy in enhancing the performance of existing neural network verifiers. Specifically, three configurations of ARVerifier are implemented: ARVerifier[Marabou], ARVerifier[α, β-CROWN], and ARVerifier[Verinet], utilizing Marabou, α, β-CROWN, and Verinet

(c) MNIST6 δ = 0.02

(d) MNIST6 δ = 0.05

Figure 4: Run Time Comparison (in Seconds, Log Scale) of ARVerifier on MNIST Models: PGD-Generated vs. Randomly Generated Input Sets

as the backend verifiers, respectively. These configurations are then compared with their standalone counterparts without ARVerifier integration. Table 1 presents the experimental outcomes across six configurations for the ACAS Xu, MNIST2, MNIST4, and MNIST6 models, where ver denotes the number of verifiable safety properties, t(s) represents the average verification time per property in seconds. Bold data highlight the superior results between each pair of compared configurations under the same benchmark. The ALL row at the bottom summarizes the total number of verifiable safety properties, the cumulative verification time across all the benchmarks.

As is shown in Table 1, ARVerifier configurations generally outperform their original counterparts, solving more problems in less time. Specifically, ARVerifier[α, β-CROWN], ARVerifier[Verinet], and ARVerifier[Marabou] exhibit superior efficiency in verifying relatively larger network models MNIST4 and MNIST6 compared to the standalone α, β-CROWN, Verinet, and Marabou, respectively. However, for smaller models, ARVerifier[α, β-CROWN] and ARVerifier[Verinet] may require additional verification time. This is because these tools are already efficient in dealing with smaller models and can verify their problems in a short time. By contrast, ARVerifier's abstraction-refinement process and subsequent re-verification of refined networks introduce additional time overhead, ultimately leading to longer verification time for such cases. Another observation is that ARVerifier[Marabou] exhibits consistent improvement across most scenarios compared with the original Marabou, which also indicates the effectiveness of the proposed abstraction method in enhancing the efficiency of neural network verification. Overall, ARVerifier[α, β-CROWN], ARVerifier[Verinet], and ARVerifier[Marabou] reduce verification times by 11.61%, 18.70%, and 12.20%, respectively, compared to their original configurations.

Furthermore, we conduct ablation studies to evaluate the performance improvement achieved by using PGD adversarial attacks for input set generation compared to random generation. We employ Verinet as the backend verifier for ARVerifier, varying only the input set generation method to isolate its impact. To obtain more pronounced results, we performed these experiments on the relatively larger MNIST4 and MNIST6 models. As illustrated in Figure 4, the majority of data points and crosses are positioned above the gray line, demonstrating that the PGD-based input set generation method outperforms random generation across most verification scenarios.

5.3 Comparative Analysis: ARVerifier vs CEGAR-based Approaches

We conduct a comparative analysis of ARVerifier against existing CEGAR-based approaches NARv [Liu et al., 2024] and CEGAR-NN [Elboher et al., 2020], all utilizing Verinet as their backend verification engine. In this analysis, α, β-CROWN is not considered because it lacks a unified solving strategy and requires manual fine-tuning to achieve optimal results for networks of different sizes and obtained with different abstraction strategies. Marabou is not used owing to its relatively slower verification speed. Table 2 presents the experimental outcomes for these three configurations across the ACAS Xu, MNIST2, MNIST4, and MNIST6 models. For each configuration, ver denotes the number of verifiable safety properties, t(s) represents the average verification time per property in seconds, and size indicates the average neuron count in the network following the initial abstraction. Bold data highlight the best results among compared configurations under the same benchmark. The ALL

row summarizes the total number of verifiable safety properties, cumulative verification time, and aggregate neuron count after the initial abstraction across all benchmarks.

According to the results in Table 2, ARVerifier exhibits superior performance compared to NARv and CEGAR-NN across the key metrics: problem-solving quantity, verification time, and abstract network size. CEGAR-NN's poor network size reduction stems from its preprocessing stage that quadruples the network size, as well as its structure-based abstraction process that disregards input attributes. NARv matches ARVerifier in network size reduction, its use of randomly generated input sets for abstraction restriction leads to suboptimal initial abstraction, necessitating multiple refinements and resulting in limited verification performance. Specifically, ARVerifier demonstrates improvements by 26.64% and 46.87% in verification efficiency compared to NARv and CEGAR-NN, respectively. These results underscore the effectiveness of ARVerifier in neural network verification.

6 Conclusion

This paper proposes a generic abstraction-refinement method for neural networks verification. Specifically, we introduce an abstraction procedure based on neuron similarity and a corresponding refinement strategy to improve the verification efficiency. We implement the method in a tool and evaluate it on two widely used benchmarks. Experimental results demonstrate that our method can significantly enhance the scalability and efficiency of state-of-the-art complete verification tools without compromising their accuracy, particularly for larger network models.

Acknowledgments

This work is supported by National Natural Science Foundation of China through grant No.62192734, 62402372.