Fully Automatic Neural Network Reduction for Formal Verification
Authors: Tobias Ladner
Matthias Althoff
Venue: Accepted by TMLR ()

Abstract: Formal verification of neural networks is essential before their deployment in safety-critical applications.
However, existing methods for formally verifying neural networks are not yet scalable enough to handle practical problems under strict time constraints.
We address this challenge by introducing a fully automatic and sound reduction of neural networks using reachability analysis.
The soundness ensures that the verification of the reduced network entails the verification of the original network.
Our sound reduction approach is applicable to neural networks with any type of element-wise activation function, such as ReLU, sigmoid, and tanh.
The network reduction is computed on the fly while simultaneously verifying the original network and its specification.
All parameters are automatically tuned to minimize the network size without compromising verifiability.
We further show the applicability of our approach to convolutional neural networks by explicitly exploiting similar neighboring pixels.
Our evaluation shows that our approach reduces large neural networks to a fraction of the original number of neurons
and thus shortens the verification time to a similar degree.

Published in Transactions on Machine Learning Research (06/2025)
Fully Automatic Neural Network Reduction for Formal Verification
Tobias Ladner
Sobias.ladner@tunn de althoff@lum.dd de
Matthias Althoff
School of Computation, Information and Technology
Technical University of Munich, Germany
Reviewed OpenReview: https: openreview. net/ formm? id= gmf leWl VNL
Abstract
Formal verification of neural networks is essential before their deployment in safety-critical applications. However, existing methods for formally verifying neural networks not yet scalable enough to handle practical problems under strict time constraints. We address this challenge by introducing fully automatic and sound reduction of neural networks using reachability analysis. The soundness ensures that the verification of the reduced network entails the verification of the original network. Our sound reduction approach is applicable to neural networks with any type of element-wise activation function, such as ReL.U, sigmoid, and tanh. The network reduction computed on the fly while simultaneously verifying the original network and its specification. All parameters are automatically tuned to minimize the network size without compromising verifiability. We further show the applicability of our approach to convolutional neural networks by explicitly exploiting similar neighboring pixels. Our evaluation shows that our approach reduces large neural net to a fraction of the original number of neurons and thus shortens the verification time to a similar degree.
1 Introduction
Neural networks achieve impressive results in a varicty of fields, inchuding natural language processing (Nassif et al., 2019), computer vision (Li el al., 2022), and medical imaging (Karimi & Salcudean, 2019). In recent. years, neural networks have been deployed safety-critical environments, such as human-robot interac- tion (Mukherjee et al., 2022) and autonomous driving (Zablocki et al., 2022). As real-life applications are inherently exposed to noise, such measurement inaccuracies and external disturbances, the deployment of neural networks in safety-critical environments is limited due to their sensitivity to adversarial attacks (Good- fellow et al., 2015): Even small perturbations of the input to a neural network, which are often barely noticeable to the human eye, can lead to unexpected outpuls, e.g., a different predicted classification of an image or a controller returning an unsafe action. Thus, the formal verification of neural networks has gained importance in recent years (Brix al., 2024; Lopez et al., 2024), where approaches rigorously prove that the output of neural networks meets given specifications.
1.1 Related Work
State of the art. neural network with ReLU activations is NP-hard (Katz et al., 2017). Thus, instead of applying complete algorithms (Huang el al., 2017; Katz et al., 2017), recent developments are made towards incomplete algorithms, where the neural networks are abstracted to enclose the exact behavior of the network. These approaches often formulate the formal verification of neural networks as an optimization problem (Katz et al., 2017; Zhang al., 2018; Katz al., 2019; Müller et al., 2022) or use reachability analysis (Singh et al., 2018a; Bogomolov et al., 2019; Bak, 2021; Lopez al., 2023b; Kochdumper et al., 2023; Ladner & Althoff, 2023).
Formally verifying neural networks is computationally expensive, e.g., verifying

---

Published in Transactions on Machine Learning Research (06/2025)
Optimization-based verifiers reason about neural networks by introducing relaxed, linear constraints for the activation functions and solving these relaxed problems using linear programming, satisfiability modulo theories (SMT) solvers (Katz et al., 2017; Zhang et al., 2018; Katz et al., 2019; Müller et al., 2022), or symbolic interval propagation (Henriksen & Lomuscio, 2020; Singh et al., 2019; Brix & Noll, 2020). Branch-and- strategies (Bunel et al., 2020) can be beneficial by splitting the problem at the neuron level (Botoeva el al., 2020; Singh et al., 2018b), e.g., by splitting ReLU neurons into their linear parts. In general, algorithms that split the problem lead to an exponential time complexity (Katz et al., 2017); so that current state-of-the-art tools (Brix et al., 2024) use more advanced strategies (Wang et al., 2021; Ferrari et al., 2022; Shi et al., 2023).
Verifiers using reachability analysis propagate sets through the neural network and verify a given specification using the computed output set. Simple representatives of this approach use pure interval arithmetic (Pulina & Tacchella, 2010) or convex set representations such as zonotopes (Gehr et al., 2018; Singh et al., 2018a). As with optimization-based verifiers, splitting the set can improve the results (Xiang et al., 2018; Kopetzki & Günnemann, 2021). Non-convex set representations are used to tightly enclose the output due to the inherent nonlinearity of neural networks, including Taylor models (Tvanov et. al., 2021; Bogomolov el al., 2019; Huang et al., 2022), star sets (Bak, 2021; Lopez et al., 2023b), and polynomial zonotopes (Kochdumper et al., 2023; Ladner & Althoff, 2023). However, the scalability to state-of-tho-art networks remains major challenge for optimization- pooimization-based approaches and approaches based on reachability analysis (Brix et al., 2024).
Challenges. Safety-critical environments are often time-critical, e.g., verifying controller of an autonomous car (Topez et al., 2024), or require verifying many instances, e.g., in video verification and in formal explainable artificial intelligence (Bassan & Katz, 2023). Thus, each verification query should be solved quickly to reduce the overall verification time. However, many saate-of-thearr verifiers focus on very challenging queries, with large timeouts per query. For example, the allowed time to verify a single query in the last VNN-COMP (Brix et al., 2024) range up to 20 minutes, which not fcasible in time-critical scenarios.
Sound neural network reduction. One promising research direction to tackle this issue is sound neural network reduction (Boudardara et al., 2023c): Sound neural network reduction reduces the number of neurons and provides formal bounds for the maximum error due to this reduction. Then, we can reason about the original network by verifying the reduced network, which usually requires less computation time. This research direction is closely related to neural network compression (Zhangheng et al., 2022; Deng et al., 2020), where the main goal is to reduce memory usage and compulation time, e.g., for deployment in embedded systems (Deng et al., 2020). This can be done as neural networks are typically over wer-parametrized (Neyshabur et al., 2018). Examples of compression techniques are quantization (Cheng et al., 2017) and pruning (Gonzaloz-Carabarii Carabarin et al., 2024). However, the lack of formal error bounds prevents applying these techniques to the formal verification of neural networks.
Several approaches soundly reduce neural networks with formal error bounds emerged in recent years: An early approach categorizes neurons based analytic properties and merges neurons of the same category afterward (Elboher et al., 2020). Similarly, networks can be reduced using approximative bisimulations (Prab- hakar, 2022). These works are extended using interval neural networks (Prabhakar & Afzal, 2019; Sotoudeh & Thakur, 2020; Boudardara et al., 2022; 2023a;b), where the weights of a neural network are replaced with intervals during the sound reduction. It is worth mentioning that the reduced network can be re-enlarged using residual reasoning (Elboher et al., 2022). For RcLU networks, it is also possible to merge ncurons that are entirely in the nonpositive or nonnegative region, respectively, without inducing outer approximations (Zhong et al., 2023). Network reductions can also be achieved by clustering similar neurons for inputs of given dataset (Ashok et al., 2020); however, 80 80%90% of the neurons remain when formal error bounds are demanded. Convolutional neural networks with max-pooling layers can be reduced by pruning branches leading up to pooling neuron and providing respective error bounds rossky et al., 2022). Most approaches only consider relatively small networks with ReLU neurons, while some approaches also consider sound network reduction for spocific other activation functions such as tanh (Boudardara et al., 2023c).
1.2 Contributions
To summarize, our main contributions are follows:
2

---

Published in Transactions on Machine Learning Research (06/2025)
We present a novel, fully automatic approach to soundly reduce large neural networks by merging similar neurons for given specification.
The reduced network is constructed on the fly, and the verification of the reduced network entails the verification of the original network.
As opposed to related work, our approach is applicable to all neural networks with element-wise activation functions, including ReLU, sigmoid, and tanh.
The networks considered in the evaluation have up to order of magnitude more neurons in a single layer than previous sound network reduction approaches considered in total, demonstrating the scalability our approach.
We demonstrate our approach using reachability analysis with zonotopes (Girard, 2005; Singh et al., 2018a). The extension to other set-based verification tools is straightforward. The resulting reduced network can also be exported and verified using optimization-based verification tools (Sec. 1.1).
The remainder of this work is structured as follows: Sec. 2 introduces the notation and background for this work. Then, we present our novel, fully automatic, sound network reduction approach in Test. 3. In Test. 4, we discuss applications our approach, including the reduction large convolutional neural networks and how the reduced nelwork can be reused for changed specifications. Finally, we evaluate our approach in Test, and conclude in Test. 6.
2 Preliminaries
2.1
Notation
We denote scalars and vectors by lower-case letters, matrices by upper-case letters, and sets by calligraphic letters. The i-th element of a vector v E R" is written as U(j), and the element in the i-th row and j-th column of a matrix E Raxm is written as A(,,) The i-th row and j-th column are written as Ag.) and A(.)), respectively. The concatenation two matrices A and B is denoted by [A B). We write R. to refer to all positive real numbers. For n N, we denote the identity matrix by In, and we use the notation [n] = (L....,n) Let C S [n], then A(c,)) extracts all rows i E C in lexicographic order. We denote the cardinality of discrete set C by |C]_ Let S C R be continuous set, then S is its projection the i-th dimension. The symbols 0 and 1 refer to matrices with all zeros and ones of proper dimensions, respectively. The set-based evaluation of function f: R" R" is written S(S) (f(x)
E Given two sets S1,S,, then the Minkowski sum is denoted by S + S2 = {si + + 81 E S1, E S2). If either summand of the Minkowski sum is given as a vector, it is implicitly converted to a singleton. The Cartesian product is written S S2 = [[ "57"" $1 E S1 2 E S2). An interval with bounds l R", where I S holds wlement-wise, is denoted by [2, u). Unless otherwise stated, all continuous sets in this paper are represented as zonotopes except for the exact sets denoted by D* and intervals denoted by In-
2.2 Neural Networks
We introduce feed-forward neural networks (Bishop & Nasrabadi, 2006, Sec. 5.1) in their standard form here and discuss the sound reduction of convolutional neural networks in Sec. 4.1.
Definition 1 (Feed-Forward Neural Networks (Bishop & Nasrabadi, 2006, Sec. 5.1)). Given ks allernating linear and nonlinear layers and let R.ne be the input and y E TR be the output of neural network, we can formulate a neural network Q: Rno + Th with y (xx) as follows:
ho x, h4 (hb-1)) y = his
1: E [n].
where Lx: R + n compules the operation of layer k. Let We E x by E R and dbe(-) be the respective continuous activation function (e.g., sigmoid and ReLU), which is applied element-wii wise, then
Ty (h(hh-1) =
Wahh-1+ + by dx
if layer k is linear, otherwise.
3

---

Published in Transactions on Machine Learning Research (06/2025)
Please note that some works formulate the layers of neural network (x(hx-1) = Φ (Wahhh bb), ie., having the linear part and the nonlinear part within one layer. We opted to separate them into individual layers as the enclosure is handled differently (Prop. 3), however, the architecture is the same. Thus, we always have linear and nonlincar layers in alternating fashion.
The last linear and last nonlinear layers are called output layers, all other layers are called hidden layers. If all hidden layers output the same number of neurons, we write 200 refer network with 6 linear and 6 nonlinear hidden layers with 200 neurons each.
2.3 Set-Based Computing
We use reachability analysis verify neural networks: Let X' C IRo be the input set of neural network 4. Then, the exact output y ((x) computed by
Hi = X, = (HH y" H
k E [x]]
(1)
Csually, is constructed by perturbing each dimension of an input x E R up to a maximal perturbation radius E R+. Unfortunately, it computationally infeasible to obtain these exact sets general as the problem is NP-hard for networks with ReLU activations (Katz al., 2017). For that reason, verification tools usually compute outer approximation y 2 ) using specific set representation. Our reduction approach works for any set representation that can be enclosed by interval and that is closed under the Minkowski addition of intervals. We use zonotopes as an example to demonstrate our approach:
Definition 2 (Zonotope (Girard, 2005, Def. 1)). Given center vector E B and a generator matris G E IR=x zonolope is defined as
z= = (c, Gi G)z
c+ Σ 3,G(.)) Bg 8
For zonolopes, the input set given by X² (1x, elno) alln) and the required operations are computed as follows: Proposition (Interval Enclosure (AlthofT, 2010, Prop. 2.2)). Given a zonolope 2 = (c, G) the enclosing interval [1, u] = interval (Z) 2 Z is given by
9 with Ag
I c u=c+Ag
Σ G(S)l
Proposition 2 (Interval Addition (Althoff, 2010, Eq. 2.1)). Given a zonotope 2 = (c, G) C B and on interval I = 11, u] C R",
2 Z (c cr, (G Diag (u - ez)llz
where CI = Lou 2
and Diag (.) returns a diagonal matrir.
2.4
Neural Network Verification
As we use zonotopes as an example to verify neural networks, we briefly introduce the main steps to propagate a zonotope through a neural network. These might differ another verification engine is used. Since the propagation in (1) cannot be computed exactly in general, we enclose the output of cach layer:
Proposition 3 (Image Enclosure (Singh et al., 2018a, Soc. 3)). Let H4-1 2 Hi-1 be an input set to layer k, then
Hr = enclose (I,, Ha-1) 2 Hi
computes an outer-approcimatiiv output set.
While zonotopes can be propagated through linear layers exactly (Girard, 2005), the propagation through nonlinear layers has to be onter-approximativ to ensure soundness. The main steps to enclose the output of
4

---

Published in Transactions on Machine Learning Research (06/2025)
(a) Steps & 2
(b) Steps 3 &
(c) Steps 5 & 6
Output
Output
Output
Input
Input
Input
(x))
Set
Bounds
Polynomial
Approximation error
Figure 1: Main steps of enclosing a nonlinear layer. Step 1: Neuron- sigmoid function. Step 2: Find input bounds. Step 3: Approximate with lincar function. Step 4: Determine approximation error. Step 5: Apply linear transformation on input. Step 6: Enclose using approximation error.
nonlincar layers are illustrated in Fig. 1: For each nonlincar layer, we iterate over all neurons in the current layer by projecting the input set H onto its i-th dimension (Step 1) and determining the input bounds using Prop. 1 (Step 2). We then find an approximating linear function within the input bounds (Bishop & Nasrabadi, 2006, Sec. 3) (Step 3). Crucially, soundness ensured by bounding the approximation error (Step 4). Finally, we apply the linear transformation on Hz-1()) to approximate the nonlinear layer (Step 5) and enclose the activation function using the approximation error (Step 6; Prop. 2). Thus, by propagating given input set X through all layers of neural network and enclosing their output sets using Prop. 3, can enclose the exact output set of the entire network by y H. 2 y = +(x).
2.5 Problem Statement
Given an input set C R"o a neural network 4, and an unsafe set S C R"x we want to automatically construct sound reduced network e for which the verification entails the verification of the original network for the given X' and S:
f(x)
B(X)SS=
This formulation covers all specifications from the VNN competition (Bak al., 2021; Brix et al., 2023), and more complex specifications can also be formulated as reachability problems (Topez et al., 2023a; Wright Stark, 2020). Further, we want the construction and verification of to be faster than verifying & directly.
150
Number of neurons
3 Fully Automatic and Sound Neural Network Reduction
Layer 2
Layer 4
100
Layer 6
Layer 8
Our sound neural network reduction is based on the observation that many neurons a layer behave similarly for a specific input E R"" e-g., many sigmoid neurons are fully saturated and thus output value near or 1 shown in Fig. 2. Neuron saturation (Rakitianskaia & Engelbrecht, 2015) and neural activation patterns (Bäuerle et al., 2022) have been observed in the literature, however, to the best. of our knowledge, they have not been exploited for the verification of neural networks. Please note that our approach restricted to the saturation values of an activation function.
50
Layer 10
Layer 12
0
0
0.2
0.4
0.6
0.8
Output of the activation layer
Figure Sigmoid activations of a 6 x 200 neural network with an image input from the MNIST digit dataset. For specific input x, many neurons output values close to the saturation values 0 and 1.
5

---

Published in Transactions on Machine Learning Research (06/2025)
(a) Original Network
(b) Reduced Network
[0.993, 1.000
B B
2]
[1.2]
5 0.026, 0.000
00.966 1.000
00.994, 0.996]
[0.994, 0.997)
[L. 1.5
[1, 1.5)
(0.269, 0.623
[0.269, 0.623
k
k: k+1
Reduction example on sigmoid neural network using single merge bucket Bk.y.& with y and 8 = 0.01: The shown bounds of each neuron cover the uncertainty after the sigmoid activation function is applied. All neurons within B are replaced by new neuron with constant output 2y + 3y = 5. Then, we bound the approximation error to obtain an outer approximation using Prop. 4.
Figure 3:
3.1 Neuron Merging
Subsequently, we explain how similar neurons can help to construct a reduced network $ where the verification of T entails the verification of the original network $. We gather the neurons with similar values using merge buckets:
Definition 3 (Merge Buckets). Given output bounds In 2 Hj of nonlinear layer E [x]] with my neurons, an output y E RR and tolerance 8 R4, then a merge bucket defined as
BR E [nw]] | In(s) S -y -, +
Conceptually, replace all neurons in merge bucket Bxy,, by single neuron with constant output y and adjust the weight matrices of the linear layers k and h such that the reduced network & approximates the behavior of the original network &. Finally, we add an approximation error I++1 C R the output of the linear layer k + 1 to obtain sound outer approximation (Fig. 3). To simplify the notation, adapt. Def. for linear layers slightly to also include the approximation error:
Wahk-Ithe + Ig layer & is linear, (h
(hhhh11)=
(2)
otherwise,
where I is initialized with [0, 0] C R", With that, we can formally introduce how we merge neurons within the neural network:
Proposition 4 (Neuron Merging). Given a nonlinear hidden layer l E [x] of network D, output bounds I Hi C IR merge bucket B [ng], and the indices of the remaining neurons B [nx] construct a sound reduced network s, where we adjust the nonlinear layer l to only process the remaining neurons, and in the adjacent linear layers, we remove the merged neurons and bound the opprorimation error:
Lager k 1:
W W W--1BB.)
6x- bk-1(3))
I = -1==-11-(7)
and layer ls + 1: W = W ())(.BB)
6x = be+1,
I = WW+11,,8]Zx(1))
Proof. The proof can be found in Appendix A.
Fig. 3 illustrates the neuron merging for a toy neural network with sigmoid activation. Please note that we display the bounds for each neuron as intervals; however, the underlying verification engine might use a different set representation, e.g,, zonotopes.
By iteratively applying Prop. 4, our approach can be naturally extended to multiple disjoint merge buckets:
B BRA (Bk.n.&, Bk.
33)
6

---

Published in Transactions on Machine Learning Research (06/2025)
The merging with multiple disjoint merge buckets can be done in parallel as the required adaptations of the adjacent linear layers do not interfere with each other. The overall approximation error is then given by the Minkowski sum of the individual approximation errors (Prop. 4)
(Prop.
(disjoint
k++
1,
W 11)1(.8)
W WA+1(-Usce By
BB By
(4)
BEB
3.2 Initialization of Merge Buckets
We define two different methods to initialize merge buckets:
Static buckets The merge buckets are determined by the asymplotic values of the respective activation function 6x of nonlinear layer k:
(Br.0.8 1,,1,8)
if Φb sigmoid,
B k,,
BB 1,
if Φb = tanh,
(5)
(Bx,08)
if ΦR = RoLU.
For ReLU layers, setting = and using static merge buckets results in no approximation error similar to the approach (Zhong et al., 2023), as only neurons with entirely negative input for the given input set are removed.
Dynamic buckets
The merge buckets are dynamically initialized using the center the bounds I, [k, uz] C TR of cach neuron:
BR.8 = (BE,q c Lutus i E [mc]],
(6)
where we ensure that the buckets are disjoint and are only used if they contain multiple neurons. Please note that the buckets could also be created using clustering algorithms (Ashok et al., 2020); however, we choose the center of each neuron directly obtain a linear computational overhead. The computational overhead of clustering algorithms might be nogligible for other underlying verification engines than the zonotope approach considered in this work.
3.3 Automatic Determination of Bucket Tolerances
The bucket tolerance d E R4 influences how many neurons are merged, where a larger value results in more aggressive neuron merging and thus larger outer approximation. However, determining good value for 8 is tedious it is not immediately clear how much the network is reduced for any given value for 8. Thus, we automatically determinc d given desired remaining number of neurons in Alg. 1 using binary scarch. We denote the ratio of remaining neurons compared to the original nelwork with the reduction rate p E [o, 1]. To verify a given specification, we initially choose a very small p and iteratively increase it if the reduction too antor-approximative. This rcalizes us to verify many specifications using a heavily reduced network (Test. 5), and thus similar degree, the verification time reduced. Once p = 1 is reached, the original network is used and reduction is applied.

---

Published in Transactions on Machine Learning Research (06/2025)
Algorithm Automatic Determination of Bucket Tolerance
Require: Bounds I& [R: us],, reduction rate p
mmin f- 0, maax < max(u;) min (1x)
do
1) Find upper bound for bucket tolerance
8max f- 10 dmax
4: Initialize merge buckets B ómoc
Sec. 3.2 b Remaining neurons
5: TA + Th - LB 5max
while Rx/nk> p
7: do
2) Binary search
8:
+ (6min + 0max)/2
9:
Initialize merge buckets B8,6
Sec. 3.2
10:
POk +- n - -BBBBr, [B]
b Remaining neurons
11: if nu < pm then
12:
mAX ô
b. Too many neurons merged
13:
else
14:
mmi
Too few neurons merged
15:
end if
16:
while Fvg n 76 p
17:
return Kk.
3.4 On-the-fly Neural Network Reduction
Please note that we require output bounds I₃ of the next nonlinear layer k to merge neurons with similar values using Prop. However, computing them requires the construction of high-dimensional zonotopes via the lincar layer ke - 1 and the propagation of the zonotopes through the nonlinear layer k, where have to compute the image enclosure for all neurons (Prop. 3) which is what should be avoided. Thus, we deploy one-step look-ahead algorithm (Alg. 2) using interval arithmetic (Jaulin et al., 2001) to avoid these expensive computations and reduce the network on the fly. As the look-ahead is just a single step, the computed bounds are tight and do not contribute to the wrapping effect.
Algorithm On-the-lly Neural Network Reduction
Require: Input X, neural network layers Lt, Ie E [ks], roduction rate p 1: Ho < X, Ên &- La
2: for = 2, .. do
if < then
1) Look ahead Prop.
Ix-2 interval interval (2
5: I + LLL (Ix- Determine merge buckets Ba,8
Sec. 3.3
7:
LL-1, Lr, Lx+1 t Merge
D> Prop. 4
8:
end if
9:
2) Verify reduced network D Prop. 3
10:
H4-1 + enclose Ha-
11: H4 + enclose Lix Ha-1)
12: end for
13: return y + Hx
We summarize Alg. 2 subsequently: Instead of propagating the zonolope H itself forward, we just propagate interval bounds of Hx-2 to the next nonlinear layer & (Alg. 2-5). Although intervals are not closed under the lincar map, the output bounds of the linear layer are tight, and the propagation through the nonlinear layer k does induce additional outer approximations. This realizes a tight computation of the output bounds Ia with negligible computational overhead; discussion the overhead be found in

---

Published in Transactions on Machine Learning Research (06/2025)
Appendix A. After Is is obtained, the merge buckets are determined (Alg. 2), and the network is reduced by merging the respective neurons (Alg. 2). Finally, we propagate the zonotope Ha-2 through the reduced layers. Thus, we never construct a high-dimensional zonotope during the verification. Note that the number of imput and output neurons remains unchanged.
Theorem 1 (Sound Neural Network Reduction). Given an input set X, a neural network @, and a reduction mle P, Alg. 2 constructs reduced network & satisfying the problem statement in Sec. 2.5.
Proof. The proof can be found in Appendix A.
4
Applications
In this section, we discuss additional applications of our novel neural network reduction approach.
4.1 Reduction of Convolutional Neural Networks and Sound Image Compression
Convolutional neural networks are obtaining state-of-the-art results for image classification tasks (Li et al., 2022). However, neural networks for image classification are typically very large and thus particularly hard to verify. We show in this section that our novel neural network reduction approach can be naturally extended convolutional networks. Let us start by introduging the main layer within a convolutional network:
Definition (Convolutional Layer (Bishop Nasrabadi, 2006, Sec. 5.5.6)). Given an input E Rei xhixwi and a kernel K Reo xex xwx, a convolutional layer computes the output O geoxho xwo for k E [co],
E [ho], [wo] follows:
hg
WKK
O(kiis)
K m (U.ttm55tt
1=1 m= n=1
where ho = h1 - (hx 1), wo = wy (wx 1) and c₁ co are the number of imput and output channels, respectively.
Convolutional layers can be viewed linear layers defined in Def. with shared weights (Bishop & Nasrabadi, 2006, Sec. 5.5.6). The exact construc- tion of such a linear layer is given in Ap- pendix A. Thus, our approach is also di- rectly applicable for convolutional layers. An analogous conversion can be done for other typical layers within a convolutional network, such as subsampling and average pooling layers (Bishop & Nasrabadi, 2006, Sec. 5.5.6).
Original
Compressed
V1
+
One important property of convolutional networks the preservation of neighbor- hood: As the same kernel is applied the entire input, pixels of the output have similar values if the respective pixels in the input have similar values. Neighbor- ing pixels having similar values are typical in the field of image classification because many images contain large areas or ob- jects with a similar color. For example, the sky has similar shades of blue, and traffic signs typically have only one background color and one foreground color. To the best of our knowledge, our approach is the first to explicitly exploit this property of
Figure 4: Visualization of CIFAR-10 images: Original images (left) and corresponding compressed images (right), where we set all neurons within the same merge bucket B B to value Wi to extract the compressed image without added approximation error. Verifying the compressed image with formal error bounds drastically reduces the number of neurons of hidden layers.

---

Published in Transactions on Machine Learning Research (06/2025)
convolutional networks for sound neural network reduction. Intuitively, uncertain image is compressed into superpixels with formal error bounds. Let us demonstrate this by an example: CIFAR-10 images require 32 x 32 x 3 = 3072 input neurons to the network. However, many of these pixels have very similar values (Fig. 4). Thus, using our approach with dynamic merge buckets (Sec. 3.2), we can compress an image with Tormal error bounds as follows:
Corollary 1 (Sound Compression). Given an uncertain image X C. R geixkixwi and a reduction rate E [0, 1}, we can construct neural network $ that compresses this image with formal error bounds as follows: Let K E Rexxexxxx1 be kernel of a convolutional layer, where
-f
for k= 1, otherwise,
K(K1111)
k, E [cr],
and & be neural nelwork with Iwo convolutional layers with kernel K and one ReLU aclivation. The reduced network & obtained by applying Thm. 1 using X, p, and dynamic merge buckets compresses the input X with sound error bounds according to p.
Proof. The proof can be found in Appendix A.
In the truck example in Fig. 4, for perturbation radius e 0.01 and a reduction rate p 0, all 3072 neurons of the hidden layer of the compression network Φ are dynamically merged using 21 merge buckets. Thus, the image is compressed into a 21-dimensional space in the hidden layer of h and then re-enlarged to 3072 neurons in the output layer with added approximation error. Please note that usually, the image is not re-enlarged and the compressod image is passed to the actual network (sce below), where we again merge similar neurons using our approach we just do this here for illustration purposes (Fig. 4): Due to the three color channels, the original truck image has 983 unique colors, which get compressed into 178 unique colors with formal error bounds. Similarly, the original horse image has 891 unique colors, which get compressed into 142 unique colors, again using 21 dynamic merge buckets.
In larger convolutional networks, a similar compression happens in each hidden layer; however, these are usually not as easy to grasp visually due to the increased number channels in hidden layers. Note that we can prepend the layers of the compression network defined in Cor. 1 to any network as a preprocessing step to reduce the input dimension. The required steps for this preprocessing are provided in Alg. 3: We first construct the compression network as in Cor. 1. As only compute the layers of the reduced network in Alg. 3, we only require the input set represented as interval Zx, which is usually the case for many benchmarks (Brix et al., 2024). Thus, we can construct new low-dimensional imput H-22 represented by the used set representation according to the remaining neurons. Thus, we are not required to initialize the high-dimeensioaal input set using a more complexx set representation, which usually speeds up the computation In our case using zonotopes, this preprocessing step results in much fewer generators (Prop. 2) and thus speeds up the computation. The output set computed in Alg. 3 by propagating the set through all remaining layers and reducing them the fly (Alg. 2). Due to the on-the-fly fly reduction, the more complex set representation is kept in a low-dimensional space by the time it arrives at a given layer, this layer is already reduced (Thm. 1). This becomes increasingly beneficial with the complexity of the set representation used to verify the network. Note that Alg. 3 works on any neural network, but is especially beneficial for convolutional networks because neighboring pixels often have similar values.
Algorithm Sound Compression Preprocessing
Require: Input Zx, neural network Dorg, reduction rate p
1: L-2, L_ Lo + Construct pre
> Cor.
L_2, Lo Reduce using Ix. P
D Thm.
3: H_2 +- 2000tope([-_2(zx))
D Prop.
4: (+rg(+)++ + Dorg (o-(((())))
>. Prepend layers
5: y t Exccute Alg. 2 using H-2, D Dorg:
> Thm.
6: return y
10

---

Published in Transactions on Machine Learning Research (06/2025)
4.2 Reusing Reduced Networks
In general, our approach requires the computation of new reduced neural network for different input sets. In this section, we highlight several applications where the reduced networks can be reused nevertheless:
4.2.1 Branch-and-bound
Current state-of-the-art tools, c.g.; all top-ranked tools of the last VNN competition (Brix al., 2023), verify neural network by applying various branch-and-bound algorithms in the verification. Branch-and- algorithms (Bunel et al., 2020) partition the verification problem into multiple simpler subproblems, solve them individually, and aggregate the results to reason about the overall problem (Sec. 1.1). Our novel reduction approach is orthogonal to these branch-and- bound algorithms and thus can be combined with them. Since the reduced nelwork does not depend on using a specific set representation, we can reuse the reduced network on all subsets of the input set:
Corollary (Rousing Reduced Network on Subscts). Given a neural network D an input set X, and a reduction rale Py then reduced nelwork & according to Thm. 1 can be reused for all X" C X.
Proof.
The proof can be found in Appendix A.
4.2.2 Export of reduced network
As the reduced network can be reused as described above, we provide an interface to export a reduced network for later usage, e.g, to verily the reduced network using another verification lool. Please note that a reduced network of the form given in (2), having the approximation error added to the output of linear layers. As these approximation errors can be seen as additional inputs to the network, most verifiers can verify networks of this form, including optimization-basee neural networks (Prabhakar & Afzal, 2019; Sotoudeh & Thakur, 2020; Boudardara et al., 2022; 2023a;b) have intervals the weight matrices of the network, which is much harder to integrate into existing verifiers.
verifiers. In contrast, related work using interval
4.2.3 Closed-loop verification
In closed-loop scenarios, neural network is used as controller in dynamic system, which is updated every At. While well in open-loop verification, other techniques are more common in closed-loop scenarios (Lopez et al., 2024). The issue with branch-and-bour strategies is that each subset has be propagated according to differential equation until the next network eval- uation (every At), where each subset might again get splitted. Therefore, many techniques use more sophisticated set representation (Kochdumper et al., 2023; Bogomolov et al., 2019; Lopez et al., 2023b) and improve the abstraction by enclosing nonlinear functions with higher-order polynomials (Ladner & Althoff, 2023).
2
strategies work
Altitude
Goal set Reachable set Simulations
2
3
Time
Figure 5: Quadrotor example (Lopez et al., 2024, Fig. 15): As the reachable set stays within a given goal set, a reduced network can be reused as long the reachable set stays within the goal sct.
One frequent goal in closed-loop verification is to show the stability of given dynamic system over specified time horizon. For example, the QUAD benchmark in the last ARCH competition (Lopez et al., 2023a) requires showing the stability of a neural- network-controlled quadrotor at a given altitude (Fig. 5). We can infer from the simulations that the state of the system barely changes over the last sccond. Thus, we can slightly enlarge the current reachable set 4s and use it to reduce the size of the network. This reduced network can then be reused in subsequent evaluations if the reachable set stays within the set used to reduce the network controller (Cor. 2).
11

---

Published in Transactions on Machine Learning Research (06/2025)
0.10
0.50
CORA
CROWN (GPU)
CROWN
Fully automatic (Ours)
CROWN
10a
10a
Cumulative time [s]
10a
10a
10
10a
109
10-1
100
0
20
40
60
80
100
20
40
60
80
100
Number of verified instances
Number verified instances
(a)
(b)
Figure 6: Comparison of our approach with varying reduction rates p to CORA and a, B.R-CROWN: (a)
ERAN 6 x 200 sigmoid network on MNIST with varying reduction rates, (b) Marabou large convolutional
network on CIFAR-10 using our fully automatic verification approach. Be aware of the log scale.
5
Evaluation
We implemented our approach in the MATLAB toolbox CORA (Althoff, 2015; Singh et al., 2018a) and evaluate it using several benchmarks and neural network variants from the VNN competition (Bak et al., 2021). The main results are presented in this section. All evaluation details, additional experiments, and ablation studies are given in Appendix B.
Main results. Our goal is to verify given queries very quickly to make formal verification tools applicable in time-critical scenarios, e.g., video streaming, where fast verification results are demanded. However, even for relatively small networks, the verification times for non-trivial queries can be comparatively long. For example, on the ERAN 200 sigmoid network classifying MNIST images, verification takes on average 1.5s per instance using the state-of-tho-art tool a, 3-CROWN (Xu et al., 2020; Zhang et al., 2018; Wang et al., 2021) to obtain initial bounds using GPU, which might not always be available in embedded systems. Without GPU, this can take significantly longer (4.5s in this case). With our novel network reduction, we can verify most instances with only 10% of the neurons (Fig. 6a), such that the overall verification time including reducing the network- is reduced to just 200ms on a CPU (-96% verification time).
For instances that cannot be verified with so few neurons, the reduction rate p is iteratively increased until the instance is verified or the original network (p 1) is reached. We show this iterative process on the CIFAR-10 dataset in Fig. 6b using the large convolutional neural network taken from the Marabou benchmark. Initially, most instances can be verified very quickly using small reduction rate p. For these instances, the verification time is substantially faster than a, C.B-CROWN (-60% verification time). If an instance cannot be verified at this abstraction level, is iteratively increased, which results in slightly longer verification times. Such a jump in verification time is clearly visible after ~ 40 instances. Overall, our fully automatic reduction approach is still 30% faster (Fig. 6). Please visit Sec. B.2 for an ablation study on this topic.
To obtain a better understanding on which neurons are merged throughout the verification process, we show in Fig. 7 the average remaining number of neurons of different network architectures while still verifying the images. The experiments show that large reduction rates are possible without sacrificing verifiability, especially for convolutional neural networks and including various activation functions.
This is in stark contrast to related work, where usually much smaller networks with only ReLU activation are analyzod. For example, 80 -90% of the neurons of the ERAN networks remain in related work once formal guarantecs are demanded (Ashok et al., 2020, Fig. 2 & Tab. 2), whereas we reduce it to just 30% for the ERAN networks (Fig. 7a) and 10 15% for the Marabou networks (Fig. 7b). Additionally, our approach can
12

---

Published in Transactions on Machine Learning Research (06/2025)
800
8,000
Remaining neurons
x 200 Sigmoid
CNN (large)
600
x 200 ReLU
6,000
CNN (medium)
CNN (small)
400
4,000
200
2,000
1
2
4
6
8
10
12
14
2
4
6
8
10
Number of imput neurons of layer k
Number of input neurons of layer k
(a)
(b)
-104
Remaining neurons
3,000
CNN (ReLU)
0.01
CNN (Sigmoid)
0.001
2,000
CNN (Tanh)
1,000
0
1
2
8
2
6
8
10 12
14
Number of input neurons layer
Number of input neurons of layer &
(c)
(d)
Figure 7: Average number of remaining neurons of networks taken from the (a) ERAN and (b) Marabou, (c)
ERAN CNN variants, and (d) Cifar2020 benchmarks.
handle networks with any type of element wise activation function (Fig. 7c) and can handle much larger networks (Fig. 7d, shown with different perturbation radii c). Specifically, the network from the Cifar2020 benchmark has more neurons in single layer than related work consider in total (Boudardara et al., 2023c).
Additional experiments. In Appendix B, we analyze each component of our approach in an ablation study and conduct additional experiments, including on sound image compression preprocessing, non-image inputs, and closed-loop verification.
6 Conclusion
We present fully automatic and sound reduction approach to verify neural networks. Our approach considers the given specification during the reduction, which enables larger reductions than related work without compromising verifiability. All parameters of our approach are automatically tuned to minimize verification time, which greatly improves the usability our approach. Additionally, while related work mostly consider networks with ReLU activations, our approach is agnostic towards the type of activation function the reduction realized using the respective output bounds. This simple yet. effective approach is demonstrated in extensive evaluation and ablation studies, where the verification time is reduced by up to 96%. These results are achieved networks much larger than previously considered in sound neural network reduction. Moreover, we show how our reduced network can be reused despite its restriction on the input set during branch-and-bound algorithms and closed-loop verification. We hope this research advances the safe deployment neural networks safety- and time-critical environments.
ERAN network variants taken from the ERAN website: wtwp:/uww...oo/tttsssr//eeeeeeee
13

---

Published in Transactions on Machine Learning Research (06/2025)
Acknowledgements
The authors gratefully acknowledge partial financial support from the project FAT under project number 286525601 and the project SFB 1608 under project number 501798263, both funded by the German Research Foundation (Deutsche Forschnngggemiinscaaff, DFG). We also want to thank Florian Finkeldei, Tukas Koller, and Mark Wetzlinger from our research group for their revisions of the manuscript.
References
Matthias Althoff. Reachability analysis and its application to the safety assessment of autonomous cars. PhD thesis, Technische Universität München, 2010.
Matthias Althoff. An introduction to CORA 2015. In Proc. of the Workshop Applied Verification for Continuous and Hybrid Systems, pp. 120-151, 2015.
Pranav Ashok, Vahid Hashemi, Jan Kietinsky, and Stefanie Mohr. DeepAbstract: Neural network abstraction for accelerating verification. Tn International Symposium on Aulomated Technology for Verification ond Analysis, pp. 92 107, 2020.
Stanley Bak. nnenum: Verification of relu neural networks with optimized abstraction refinement. In NASA Formal Methods Symposium, pp. 19-36, 2021.
Stanley Bak, Changliu Liu, and Taylor T. Johnson. The second international verification of neural networks competition (VNN-COMP 2021): summary and results. arXiv preprinl orXiv:2109.00498, 2021.
Shahaf Bassan and Guy Katz. Towards formal XAI: formally approximate minimal explanations of neural networks. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 187-207, 2023.
Alex Bäuerle, Daniel Jönsson, and Timo Ropinski. Neural activation patterns (NAPs): Visual explainability of learned concepts. arXiu preprint 2Xix:2206100111 2022.
Christopher M. Bishop and Nasser M Nasrabadi. Pattern recognition and machine learning, volume 4. 2006.
Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. JuliaReach: A toolbox for set-based reachability. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 39-44, 2019.
Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient verification of relu-based neural networks via dependency analysis. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pp. 3291 12992, 2020.
Fateh Boudardara, Abderraouf Boussif, Pierre-Jean Meyer, and Mohamed Ghazel. Interval weight-based abstraction for neural network verification. In International Conference on Computer Safety, Reliability, and Securily, pp. 330 342, 2022.
Fatch Boudardara, Abderraouf Boussif, and Mohamed Ghazel. A sound abstraction method towards efficient neural networks verification. In International Conference on Verification and Evaluation of Computer and Communication Systems, pp. 76-89. Springer, 2023a.
Fateh Boudardara, Abderraouf Boussif, Pierre-Jean Meyer, and Mohamed Ghazel. INNAbstract: An INN-based abstraction method for large-scale neural network verification. IEFE Transactions on Neural Networks and Learning Systems, 2023b.
Fateh Boudardara, Abderraouf Boussif, Pierre-Jean Meyer, and Mohamed Ghazel. A review of abstraction methods towards verifying neural networks. ACM Transactions on Embedded Computing Systems, 2023c.
Christopher Brix and Thomas Noll. Debona: Decoupled boundary network analysis for tighter bounds and faster adversarial robustness proofs. arXio preprint 2rXiv:2006.00440, 2020.
14

---

Published in Transactions on Machine Learning Research (06/2025)
Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The fourth international verification of neural networks competition (VNN-COMP 2023): Summary and results. arviv preprint XrXi:2331 2.1:200...67000, 2023.
Christopher Brix, Stanley Bak, Taylor T. Johnson, and Haoze Wu. The fifth international verification of neural networks competition (VNN-COMP 2024): Summary and results. arXiv preprinl arxi:224 Xiu:2412.19985, 2024.
Rudy Bunel, P. Mudigonda, mkker Turkaslan, Philip Torr, Jingyue Lu, and Pushmeet, Kohli. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21:1 39, 2020.
Jian Cheng, Jiaxiang Wu, Cong Leng, Yuhang Wang, and Qinghao Hu. Quantized CNN: A unified approach to accelerate and compress convolutional networks. IEEE Transactions on Neural Networks and Learning Systems, 29:4730 4743, 2017.
Lei Deng, Guoqi Li, Song Han, Luping Shi, and Yuan Xie. Model compression and hardware acceleration for neural networks: A comprehensive survey. Proceedings of the IEEE, 108:485-55 532, 2020.
Yizhak Yisrael Elboher, Justin Gottschlich, and Guy Katz. An abstraction- framework for neural network verification. In International Conference on Computer Aided Verification, pp. 43-65, 2020.
Yizhak Yisrael Elboher, Elazar Cohen, and Guy Katz. Neural network verification using residual reasoning. In International Conference on Software Engineering and Formal Methods, pp. 173-189, 2022.
Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanović, and Martin Vechev. Complete verification via multi- neuron relaxation guided sauchhand-boure In International Conference on Learning Representations, 2022.
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. AI2: Safely and robustness certification of neural networks with abstract interprelation. In IEEE Symposium on Security and Privacy, pp. 3 18, 2018.
Antoine Girard. Reachability of uncertain linear systems using zonotopes. In International Workshop on Hybrid Systems: Computation and Control, pp. 291 305, 2005.
Lizeth Gonzalez- Carabari,,,, Iris AM Huijben, Bastian Vceling, Alexandre Schmid, and Ruud JG van Sloun. Dynamic probabilistic pruning: A general framework for hardware-constrained pruming at different. gramularities. IEEE Transactions Neural Networks and Learning Systems, 35:733 744, 2024.
Ian Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In International Conference on Learning Representations, 2015.
Patrick Henriksen and Alessio Lomuscio. Efficient neural network verification via adaptive refinement and adversarial search. In Furopean Conference on Artificial Intelligence, volume 325, pp. 2513-2520. 2020.
Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li, and Qi Zhu. POLAR: A polynomial arithmetic framework for verifying neural-betwork controlled systems. In Automated Technology for Verification and Analysis, pp. 414-430, 2022.
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In International Conference on Computer Aided Verification, pp. 3 29, 2017.
Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, George Pappas, and Insup Lec. Verisig 2.0: Verification of neural network controllers using Taylor model preconditioning, In International Conference on Computer Aided Verification, pp. 269-262, 2021.
Lue Jaulin, Michel Kieffer, Olivier Didrit, and éric Walter. Interval analysis. 2001.
15

---

Published in Transactions on Machine Learning Research (06/2025)
Davood Karimi and Septimiu E Salcudean. Reducing the Hausdorff distance in medical image segmentation with convolutional neural networks. IEEE Transaclions on Medical Imaging, 39:499-5 513, 2019.
Guy Katz, Clark Barreut David L Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient. SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117, 2017.
Guy Katz, Derek A. Huang, Duligur Theling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, et al. The Marabou framework for verification and analysis of deep neural networks. In International Conference Compuler Aided Verification, pp. 443 -422, 2019.
Niklas Kochdumper, Christian Schilling, Matthias Althoff, and Stanley Bak. Open-and closed-loop neural network verification using polynomial zonotopes. In NASA Formal Methods Symposium, pp. 16-36, 2023.
Lukas Koller, Tobias Ladner, and Matthias Althoff. Set-based training for neural network verification. arx preprint Xr:::2401.14466 2024.
Anna-Kathrin Kopetzki and Stephan Günnemann. Reachable sets of classifiers and regression models: (Non-)robustness analysis and robust training. Machine Learning, 110:1175-11977 2021.
Tobias Ladner and Matthias AlthofT. Automatic abstraction refinement. in neural network verification using sensitivity analysis. In Proceedings of the 26th ACM International Conference on Hybrid Systems: Compulation and Control, pp. 1 13, 2023.
Zewen Li, Fan Liu, Wenjie Yang, Shouheng Peng, and Jun Zhou, A survey of convolutional neural networks: Analysis, applications, and prospects. IEEE Transactions on Neural Networks and Learning Systems, 33: 2022.
Diego Manzanas Lopez, Matthias AlthofT, Marcelo Forets, Taylor T. Johnson, Tobias Ladner, and Christian Schilling. ARCH-COMP23 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In Proceedings of 10th International Workshop Applied Verification for Continuous and Hybrid Systems, volume 96, pp. 89-125, 2023a.
Diego Manzanas Lopez, Sung Woo Choi, Hoang- Dung Tran, and Taylor T. Johnson. NNV 2.0: The neural network verification tool. In International Conference on Computer Aided Verificalion, pp. 397 04724,2,45 2023b.
Diego Manzanas Lopez, Matthias Althoff, Luis Benet, Clemens Blab, Marcelo Forets, Yuhao Jia, Taylor T, Johnson, Mannel Kranzl, Tobias Ladner, Lukas Linauer, al. ARCH-COMP24 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In EPIC Series in Computing, 2024.
Debasmita Mukherjee, Kashish Gupta, Li Hsin Chang, and Homayoun Najjaran. A survey of robot learning strategies for human-robot collaboration in industrial scttings. Robotics and Computer-Integrater Manufacturing, 73, 2022.
Mark Niklas Müllrr, Gleb Makarchuk, Gagandeop Singh, Markus Püschel, and Martin Vechev. PRIMA: General and precise neural network certification via scalable convex hull approximations. Proceedings of the ACM Programming Languages, 6:1-33] 2022.
Ali Bou Nassif, Ismail Shahin, Intinan Attili, Mohammad Azzeh, and Khaled Shaalan. Speech recognition using deep neural networks: A systematic review. IEEE access, 1119143-19663 2019.
Behnam Neyshabur, Zhiyuan Li, Srinadh Bhojanapalli, Yann LeCun, and Nathan Srebro. Towards understand- ing the role of pereeaaraettionooonn in generalization of neural networks. arXiv preprint wxXi:1805.12001 2018.
Matan Ostrovsky, Clark Barrett, and Guy Katz. An abstraaction-refinmmett approach to verifying convolutional neural networks. In International Symposium on Automated Technology for Verification and Analysis pp. 391-30 -96, 2022.
16

---

Published in Transactions on Machine Learning Research (06/2025)
Pavithra Prabhakar. Bisimulations for neural network reduction. In International Conference on Verification, Model Checking, and Abstract Interprelation, pp. 285-300, 2022.
Pavithra. Prabhakar and Zahra Rahimi Afzal. Abstraction based output range analysis for neural networks. Advances in Neural Information Processing Systems, 32, 2019.
Luca Pulina and Armando Tacchella. An abstrrattion-refiemmntt approach to verification of artificial neural
networks. In International Conference on Computer Aided Verification, pp. 243 257, 2010.
Anna Rakitianskaia and Andries Engelbrecht. Measuring saturation in neural networks. Tn IEEE Symposium
Series on Computational Intelligence, pp. 1423 1430, 2015.
Zhouxing Shi, Qirui Jin, J Zico Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. Formal verification for neural networks with general nonlincarities via branch-and-bound, 2nd Workshop on Formal Verification of Machine Learning, 2023.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. Advances in Neural Information Processing Systems, 31, 2018a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In International Conference on Learning Representations, 2018b.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3:1-30, 2019.
Matthew Sotoudeh and Aditya Thakur. Abstract neural networks. In Static Analysis, pp. 65 88, 2020.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-ncuron split constraints for complete and incomplete ncural network verification. Advances in Newral Information Processing Systems, 34, 2021.
Thomas Wright and Ian Stark. Property-directed verified monitoring of signal temporal logic. In Runtime Verification, pp. 339-358, 2020.
Weiming Xiang, Hoang-Dung Tran, and Taylor T. Johnson. Outpul reachable set estimation and verification for multilayer neural networks. IEEE Transactions Newral Networks and Learning Systems, 29:5777-5788 2018.
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 63:1129-1144 2020.
Éloi Zablocki, Hédi Ben- YounYs, Patrick Pérez, and Matthieu Cord. Explainability of deep vision-based autonomous driving systems: Review and challenges. International Journal of Computer Vision, 130: 2425 2452, 2022.
Hongyang Zhang, Yaodong Yu, Jiantao Jiao, Eric Xing, Laurent El Ghaoui, and Michael Jordan. Theoretically principled trade-off between robustness and accuracy. In International conference on machine learning, pp- 7472 7482, 2019.
Huan Zhang, Tsui-Wa Weng, Pin-Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in Neural Information Processing Systems, 31, 2018
LI Zhangheng, Tianlong Chen, Linyi Li, Bo Li, and Zhangyang Wang. Can pruning improve certified robustness of neural networks? Transactions on Machine Learning Research, 2022.
Yuyi Zhong, Ruiwei Wang, and Siau-Cheng Khoo. Expediting neural network verification via network reduction. arx preprint arXiv:2308.0333 2023.
17

---

Published in Transactions on Machine Learning Research (06/2025)
Appendix
A Proofs
In this section, we give the missing proof of the main body of the paper:
Proposition 4 (Neuron Merging). Given a nonlinear hidden layer k E [x] of a network D, output bounds I 2 Hz C IR**, merge bucket B _ [ng], and the indices of the remaining neurons B [mg]]B, we construct sound reduced network $, where we adjust the nonlinear layer k to only process the remaining neurons, and in the adjacent linear layers, we remove the merged neurons and bound the approzimation error:
Layer k 1:
W WK k-1BB.))
d 1111(1))
Ig-1 =====k-1005 I-))
and layer lo + 1:
Wx+1 = W W++1(.B)
b = bx+1,
22 = B)+
Proof. Soundness. We show that the output Hot1 of layer + of the reduced network o is an outer approximation of the exact set Hz+1"
Ha+1 (1) La+1 (Lx (La-1
La+1 (Lx (Wa- + bx- + (I-11))
Without loss of generality, we relabel the neurons such that B [|]]] and partition the neurons of layer k using the Cartesian product:
Ha+11 La+1 (Le ((W
bx-1(B) @ I()) ( + 6 1(5)
I k- (1))
Rewriting the merged neurons (first term) using (1) and the remaining neurons (second term) using Lx-1, L as defined in Prop. results in:
Ha+1 Lu+i (Ia ( @ (I-1(B)) x Iu (In (H(
We then enclose all merged neurons by the given interval bounds:
Hi+1
(Def.
L (INBB) Lu (Ix-1(H() =H
H4+11
and propagate them forward to the next nonlinear layer k 1. This operation implicitly propagates the new constant neuron forward the bias of the layer k+ 1 as well without inducing additional outer approximations. Thus, using the identity W I2) = Wt a W. W(BB)IZ, we obtain:
= (Def. 1) WK+1 (IN(8) x La (In-I(HG-2)) + bx+1
H4t1
= (7) 2 W W Tux (Tx-1(F( + bet1-
Finally, rearranging the terms obtains Σ as defined in Prop. 4:
H4 (Wa+i).3) Ls (Hx- bk+1 W1+1(.8)I11B))
= =Tx+1 (Tx (H+-)(H)
which we can enclose using the underlying verification engine:
(Prop. 3)
Hh+1 S Nat1-
Hence, Hat1 C Hert1 C Rett-
18

---

Published in Transactions on Machine Learning Research (06/2025)
Overhead complexity of Alg. 2. To analyze the complexity of the overhead due to bound propagation
in Alg. 2 (Alg. 2 to 2); let us introduce some notations: Given two functions f.D. we use the notation (()) E O(((z)) = lim sup lg(a] xc, and f(x) (gg(z)) + limsup la(a)]
[((]
[f(x] 0. Then, the
computation bounds using intervals through both layers (Alg. 2) can be done in (7k--1 In contrast, propagating the zonotope Mx-2 C R through the next linear layer & - in 1( as Hx-2 has al least 7 generators, with additional computations necessary to enclose the nonlinear layer & (Prop. 3). As ((p n (( 0, the computational overhead for the bound propagation is negligible. This becomes even more favorable with more complex set representations being used as they usually do not have& a better computational complexity than zonolopes on the relevant operations.
Theorem 1 (Sound Neural Network Reduction). Given an input set X, a neural network &, and reduction rate p, Alg. 2 constructs reduced network e satisfying the problem statement in Sec. 2.5.
Proof. For the main condition in the problem statement. (Sec. 2.5)
T (X)ns
to hold, we require that (x) 2 ((x) holds. This is the case as each step in Alg. 2 is outer-approximative In particular, as Prop. 4 holds, the computed error bounds ensure that the output of the original network is contained in the output of the reduced network. Please note that the subset relation holds for the exact evaluation of the respective sets, but might not hold Prop. applied to compute the output set as a different abstraction might be used.
Transformation of convolutional layers linear layers. Convolutional layers can be transformed regular linear layers as defined in Def. by viewing them línear layers with shared weights (Bishop & Nasrabadi, 2006, Sec. 5.5.6). Let briefly restate the definition of a convolutional layer for convenience: Definition 4 (Convolutional Layer (Bishop & Nasrabadi, 2006, Sec. 5.5.6)). Given an input I E g xhrxwr and a kernel K E Reoxe xei xhx xwx a convolutional layer computes the output O E Reoxho xwo for l E [col, E [ho], j E [wr]] as follows:
hx
O(kis)) =
K ((..mmm) [ (1++m.++))
1=1 m=
where ho = b, - (hx- 1), wo wr (wk 1) and er, co are the number of inpul and outpul channels, respectively.
The same operation as in Def. 4 can be computed by flattening the input image into vector:
i= [1
Ier]".
(8)
with 4 [(a..) ... Tamrl E [cr],
and correctly populating each row of the weight matrix WK
with the kernel K:
((LLL)) K(L12)
K(LLL
WK
(9)
Kieo. bx.)))
Please note that WK is very sparse. If the convolutional layer has bias, the construction of the resulting bias vector is analogous.
Corollary (Sound Compression). Given an uncertain image C R x and a reduction rate E [0, 1], can construct neural network & that compresses this image with formal error bounds as follows: Let K E xexxxxxxx1 be kernel of a convolutional layer, where
((I.1111) ={ 1 for k = I, otherwise,
k, (crl-
(7)
19

---

Published in Transactions on Machine Learning Research (06/2025)
Table 1: Network sizes and activation functions. Most networks are taken from VNN-COMP benchmarks (Brix et al., 2024)) and the others are variants from them provided by the team proposing the respective benchmarkk
Dataset
Benchmark
Activation
Description
ReLU
Fully-connected with x 100 ncurons
ReLU/Sige /Sigmoid
Fully-connected with x 200 neurons
FRAN
ReLU
Fully-connected with x 500 neurons
ReLU ReLU//igan /Simmiid /Tanh /aanh
CNN with convolutions and 2 linear layers
MNIST
Sigmoid
Fully-connected with 6 x 200 neurons
ReLU
Fully-connected with x 256 neurons
MNISTFC
ReLU
Fully-connected with 256 neurons
ReLU
Fully-connected with x 256 neurons
ReLU
Large CNN with convolutions and 2 linear layers Medium CNN with 2 convolutions and 2 linear layers Small CNN with convolutions and 2 lincar layers
Marabou
ReLU
CIFAR-10
ReLU
Cifar2020
ReLU
CNN with convolutions and 3 linear layers
ACAS-XU
ReLU
Fully-connected with 50 neurons
QUAD
Sigmoid
Fully-connected with 3 x 64 neurons
and & be neural network with two concolutional layers with kernel K and one ReLU activation. The reduced network pp obtained by applying Thm. 1 using X, and dynamic merge buckets compresses the input X with sound error bounds according to p-
Proof. The original network & computes the identity by construction. The image is compressed in the hidden layer of & (Thm. 1). The computed bounds ensure X' C (,(x).
Corollary (Reusing Reduced Network on Subsets). Given a neural network $ an input set X, and reduction rale then a reduced network p according to Thm. 1 can be reused for all X" C C.
Proof. The proof follows from the construction o using Thm. 1.
B Additional Experiments and Ablation Studies
B.1 Evaluation Details
All computations were performed on an Intel@ Co Gen. 11 17-11800H CPU @2.30GHz with 64GB memory if not stated otherwise. The GPU results for a, 3-CROWN were computed on the same device using a NVIDIA GeForce RTX 3080 laptop GPU. Details about the individual network can be found in Tab. 1. For all image datascts, we sample 100 correctly classified images from the test set and average the results. The perturbation radius e R4 is always stated with respect to the normalized images X c [0, 1) If not otherwise stated, feed-forward neural networks reduced using static merge buckets and convolutional neural networks using dynamic merge buckets (Sec. 3.2).
Figures showing remaining number of neurons: For all figures showing the remaining number neurons while still verifying the given specification, our reduction results are illustrated by the mean remaining input neurons per nonlinear layer al even E [<]. The number of input and output neurons of the entire nelwork are displayed at k = 1 and & = k + 1, respectively. We do not show the number of input neurons of a linear layer + 1, as it has the same number of input ncurons as the preceding nonlincar layer k. The number of neurons of the original network is shown in the same color with reduced opacity. Additionally, we show error bars indicating standard deviation from the mean reduction per layer.
20

---

Published in Transactions on Machine Learning Research (06/2025)
Relative verification time
0.8
0.8
0.6
0.6
0.4
0.4
0.2
0.2
0.2
0.4
0.6
0.8
0.2
0.4
0.6
0.8
Reduction rate
Reduction rate p
Figure 8: The relative verification time of the reduced network primarily depends on the reduction rate p: ERAN sigmoid network (left) and ERAN CNN (right).
10%
P 20%
P 30%
Label
5
= 40%
50%
60%
2
70%
P 80%
90%
-70
-60
50
40
30
-20
110
10
Original
Prediction
Figure 9: Fully automatic network reduction: Comparison of outer-approximative bounds of the prediction for an MNIST image with = 0.01 using the ERAN sigmoid network for different reduction rates
B.2 Ablation Study
In this section, revisit all components and parameters to analyze their impact on the overall result.
B.2.1 Varying the Reduction Rate P
Let us first analyze the effect of the reduction rate on the overall verification process. We exemplarily show the relative verification time of two networks in Fig. 8, where the shown times are normalized by the time to verify single query using the original networks (0.97s the for FRAN sigmoid network and 3.76s ERAN convolutional neural network). Please note that the times for the network as the networks reduced on-the-fly (Alg. 2). Thus, Fig. 8 shows that whenever the networks are reduced to a certain reduction rate the overall verification time is reduced to a similar degree.
also include the time to reduce
For a challenging MNIST image with label 6, Fig. 9 shows the computed outer-approximativn output bounds using the ERAN sigmoid work for different p. The bounds quickly converge with increasing p, and the image can be verified with p Z 30% in this example.
B.2.2 Varying the Bucket Tolerance 5
Please note that our approach automatically tunes all internal parameters for any user-defined reduction rate p. In particular, the bucket tolerance 8 is chosen accordingly such that the desired amount of neurons are merged (Alg. 1). To obtain a better understanding on this internal parameter, we vary the bucket tolerance 8 for different perturbation radii e, where larger value for 8 results in more aggressive merging, and show the corresponding reduction rate p and number of verified instances in Tab. 2. The effects heavily depend
21

---

Published in Transactions on Machine Learning Research (06/2025)
Table ERAN benchmark: Change of verification rate (VR) and reduction rate p with varying perturbation
radius c and bucket tolerance 5.
Network 6 x 200
Sigmoid
ReLU
5
p
VR [%]]
p
VR [%]]
0.0050
0.1000
0.2392
69.00
0.5496
76.00
0.0050
0.0100
0.3700
99.00
0.5500
100.00
0.0050
0.0050
0.4242
100.00
0.5573
100.00
0.0050
0.0010
0.5146
100.00
0.5607
100.00
0.0050
0.0001
0.6380
100.00
0.5618
100.00
0.0020
0.1000
0.1640
94.00
0.3602
95.00
0.0020
0.0100
0.3028
99.00
0.3556
100.00
0.0020
0.0050
0.3455
100.00
0.3549
100.00
0.0020
0.0010
0.4705
100.00
0.3479
100.00
0.0020
0.0001
0.6004
100.00
0.3494
100.00
0.0010
0.1000
0.1318
98.00
0.3143
92.00
0.0010
0.0100
0.2782
100.00
0.2846
100.00
0.0010
0.0050
0.3336
100.00
0.2931
100.00
0.0010
0.0010
0.4507
100.00
0.2909
100.00
0.0010
0.0001
0.5882
100.00
0.2882
100.00
800
800
Remaining neurons
6 x 500
ReLU
6 x 256 ReLU
600
6 x 200
ReLU
600
4 256
ReLU
6 x 100 ReLU
2 256 ReLU
400
400
200
200
0
1
4
10
12
14
2
4
8
10 12 14
Number of input neurons of layer k
Number of input neurons of layer k
(a)
(b)
Figure 10: Reduction results with varying network sizes: (a) ERAN network variants and (b) MNISTFC networks.
the specifications and networks, such that the size of the resulting reduced network is not immediately clear. Fortunately, a user only has to specify the reduction rate and this internal parameter is tuned automatically.
B.2.3 Varying the Network Size
Let us also analyze our approach with varying network sizes. In particular, we vary (i) the number of hidden neurons and (ii) the number of layers on an otherwise identical network architecture. For the first experiment, we take network variants from the ERAN benchmark?. and show the result in Fig. 10a: Despite the different number of hidden neurons in the original network, the number of remaining neurons in the verified reduced network are not proportional the respoctive original network. We assume that this is due to the typical peee-pprrmetiiziee of net works (Neyshabur et al., 2018), with larger networks having larger over parametrization, and our reduction approach extracts the relevant subnetwork. A similar observation
2 ERAN network variants taken from the ERAN website:
22

---

Published in Transactions on Machine Learning Research (06/2025)
Remaining neurons
3,000
CNN (static)
CNN (dynamic)
2,000
1,000
0
2
Number of input neurons of layer k
Figure 11: Convolutional neural networks roquire dynamic morge buckets to exploit similar neighboring pixels.
Table 3: Average reduction rates for large perturbation radii the CORA benchmark. Entries marked with
hyphen (-) indicate combinations where not enough verifiable images were found for meaningful average.
Dataset Training
0.01
0.02
0.05
0.1
MNIST
Standard (Bishop & Nasrabadi, 2006)
0.3338
MNIST Trades (Zhang et al., 2019)
0.2760
0.3666
MNIST
Set (Koller et al., 2024)
0.1821
0.1879
0.2467
0.3556
can be made with increasing number of layers (Fig. 10b), where the nelworks are laken from the MNISTFC benchmark.
B.2.4 Static vs. Dynamic Merge Buckets
Let us also analyze the types of merge buckets (Sec. 3.2). While saturated neurons are common in fully- connected networks (Fig. 2), these might not occur in convolutional neural networks. We show this in Fig. 11 on a convolutional neural net work taken from the ERAN benchmark, where large reductions are only possible when dynamic merge buckets are used using a fixed bucket tolerance 5.
B.2.5 Large Perturbation Radii
In this study, we analyze the impact of large perturbation radii on the network reduction while still verifying the specification. Please note that networks are generally not robust against large perturbation radii. In VNN-COMP (Brix et al., 2024), typical perturbation radii for standard neural networks are around e = 0.01 with respect to the normalized images X' C [0, 10 However, counterexamples can casily be extracted for larger radii and thus the specification is falsified. Of course, such networks can also not be verified using our approach. However, there is some literature robustifying the networks (e.g., through adversarial training) and VNN-COMP also has benchmark CORA fcaturing such networks, which can be used to demonstrate our approach on larger perturbation radii. We present the reduction results on those networks in Tab. 3.
B.3
Additional Experiments
B.3.1 Sound Image Compressing as Preprocessing Step
Fig. 12 shows how the sound compression preprocessing of the input image (Alg. 3) can further reduce the overall network size (ERAN CNN with sigmoid activation). The prepended layers shown at -1 and 0 only have very few remaining neurons, where we only show the number of neurons corresponding to the dimension of the constructed zonotope. Thus, the average total verification time reduced from 4.59s to 0.78s as the initial reduction (Alg. 3, Alg. 3) is computationally cheap and the representation of the involved sets much smaller, i.e., the zonotopes have fewer generators, compared to verifying the original network. Our evaluation
23

---

Published in Transactions on Machine Learning Research (06/2025)
Remaining neurons
3,000
Compression
Normal
2,000
1,000
0
-1
2
8
Number of input neurons of layer k
Figure 12: ERAN CNN with sigmoid activation: Input compression (Alg. 3) versus normal reduction (Alg. 2).
Table 4: Average network reduction and verification time of property of the ACAS Xu benchmark.
Neural Network
Number of Neurons
Verification Time
Original Network
100.00 %
7.38s
Reduced Network
61.33 %
4.21s
shows that, on average, only 28 input neurons remain compared to the 784 input neurons of the original image (Fig. 12).
B.3.2 Reusing Reduced Network
Finally, we give two examples where the reduced network was reused despite its input set restriction (Cor. 2).
ACAS Xu benchmark We demonstrate the applicability of our approach on non-image data using the ACAS Xu benchmark (Bak et al., 2021). The benchmark consists of multiple networks and properties used verify turn advisories to an aircraft to avoid collisions. The networks have 6 50 hidden layers with 5 input and 5 output neurons. As this benehmark is particularly hard to verify, apply branch-and-boung strategy by recursively splitting the input set along the most sensitive dimension. Using Cor. 2, can reduce the network once on the original input set and reuse the reduced network to verify all subsets. The reduced network has on average only 60% of the neurons of the original network (Tab. 4, averaged over 10 runs). While Boudardara et al. (2023b) state that they can reduce the ACAS Xu networks down to a total number of 10 neurons, the obtained output sets are very conservative with radius up to 10'7 (Boudardara al., 2023b, Fig. 14-16), which makes it impossible verify the given specification.
Closed-loop verification Finally, let us revisit the quadrotor example from Sec. 4.2 show the applicability of our approach in closed-loop systems: We enlarge the current reachable set at t = 4s by factor of 1.5 to compute the reduced network controller. This enlargement is necessary as the reachable set still oscillates around its equilibrium. The reduced network can then be reused in 60% of the remaining network evaluations. Whenever the current reachable set lcaves the enlarged set used to reduce the network, the verification algorithm falls back to the original network until the reduced network can be used again. In the quadrotor example, the reduced network was always used again after one time step. Fig. 13 shows the relevant part of Fig. 5 and includes the reachable set computed with the reduced network, where both reachable sets remain within the desired goal region, and the reachable set computed with the reduced network is insignificantly larger.
24

---

Published in Transactions on Machine Learning Research (06/2025)
1.2
Altitude
0.8
set
Simulations
Reachable set (4)
Network reduction
Reachable set (4)
0.6
3
3.2
3.4
3.6
3.8
4.2
4.4
4.6
4.8
5
Time
Figure 13: Quadrotor example: We can reuse a reduced network once the system starts to converge to the desired altitude. The resulting reachable set insignificantly larger.
25


Reviews:
[{"review_id": "KVtds1G1iS", "reviewer": "Reviewer_1aVQ", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths\n- significant speed-up (up to 96%) in verification demonstrated across multiple benchmarks (ERAN, Marabou, CIFAR-10).\n- applicable to convolutional networks.\n- significantly reduces computation even on CPU-only systems, which is essential for embedded systems.\n\nWeaknesses\n- the merging is based on bounds derived from interval arithmetic during look-ahead steps. While efficient, this could be overly conservative in high-dimensional or highly nonlinear settings, potentially reducing effectiveness.\n- while the method is extended to convolutional networks, recurrent or transformer-based architectures are not considered, potentially limiting the scope in certain domains like NLP.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper proposes a novel and fully automatic technique for the sound reduction of neural networks to enhance the scalability of formal verification tools. The core idea is to reduce the number of neurons in a neural network while preserving soundness, meaning that any verification result on the reduced network guarantees the same result for the original network. The method applies to networks with element-wise activation functions (ReLU, sigmoid, tanh) and integrates reachability analysis using zonotopes to ensure soundness. The technique dynamically merges similar neurons on-the-fly, which avoids constructing high-dimensional sets during verification, thereby improving efficiency.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "The paper is well-written and clear. Despite what I reported as weaknesses, the paper is a good contribution that, in my opinion, does not require significant work.\n\nI list some suggestions:\n- in the introduction the content of the paper is only summarized with bullet points but not discussed in detail for example with respect to related works. I would suggest improving the introduction to better frame what the paper proposes with respect to competitors.\n- in section 2.2 the description of neural networks is not clear to me, especially in the differences between linear and nonlinear layers. For example, the paper always talk about \"linear and nonlinear\" but maybe talking about \"linear or nonlinear\" layers would be more correct. I suggest rewriting this section.\n- algorithm 1 could be written using the entire line width instead of half page, this will improve readability of comments and pseudocode.", "broader_impact_concerns": "No concerns", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "y5dtCakqeV", "reviewer": "Reviewer_HC6c", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "strengths:\n- The paper is very polished and easy to understand.\n- The main body of the paper is well-structured and straightforward to digest.\n- The authors make an effort to provide a broad perspective.\n\nweaknesses:\n- It is not entirely clear what the specific contribution of this paper is. Although I am not an expert, neuron merging, pruning, or abstraction, or however it is termed, does not seem novel to me. Given that, I am surprised that such methods are not incorporated in existing high-competitive verifiers, especially considering the extreme superiority that the approach of this paper claims to have.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "No", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper outlines an algorithm for the formal verification of neural networks, accommodating various activation functions such as ReLU, Sigmoid, and Tanh. The method builds upon an abstraction idea, where neurons within a neural network that exhibit similar behaviour regarding the property to be verified are merged. This results in a smaller network that can be verified in place of the original network without loosing soundness of the verification approach. The approach is referred to as \"reduction\" and can be used in combination with standard procedures such as zonotope- or intervall-based verfication approaches. The method's superior performance is demonstrated through experiments on standard benchmarks.", "claims_and_evidence_yn": "No", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "Somewhere, perhaps in the introduction, it should be made clearer what specific challenge this paper overcomes that related work did not. If I am not mistaken, the general approach is not entirely new; for example, refer to Ashok et al.'s \"DeepAbstract: Neural Network Abstraction for Accelerating Verification\". I am curious about what differentiates the setting in this paper from such related work. I noticed that this work is discussed in the related work section, but why isnt it, for example, compared to the methods this paper suggests  in the experiments? \n\nLikewise, there must be some downside to the verification approach suggested here, compared to the non-reduction-based approaches of \\alpha\\beta-CROWN, no? Otherwise, I would be surprised why merging isnt used in all verifiers already, since the idea is around for a few years already. Assuming that I am not completely mistaken here, such drawbacks are not clear in the current paper.", "broader_impact_concerns": "There are none.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "H3DzKGSVF0", "reviewer": "Reviewer_7ryJ", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strength: \n1. the proposed method is sound, which is a good aspect for an approximation method; \n2. the paper is well-written and well-motivated;\n3. the experiments sufficiently support the claims.\n\nWeakness:\n1. the method is implemented in MATLAB, which greatly reduces its impact: SOTA algorithms are all implemented in PyTorch, allowing easy application and re-development;\n2. the evaluated specification is small: $\\epsilon=0.01$. I wonder if the approximation still works well for larger $\\epsilon$, since a larger specification leads to more approximation errors in network compression.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This work observes that many neurons have similar activations in the specification and propose a new method to dynamically merge similar neurons to reduce the network size before running a formal verification. The proposed method is sound, meaning that verifications automatically transfer to the original unreduced network. The result shows that with the proposed method, even keeping an approximation network that has ~10% size is able to verify many inputs. This work concludes that the proposed method enjoys better timing than SOTA algorithms.", "claims_and_evidence_yn": "Yes", "claims_explanation": "", "audience_yn": "Yes", "audience_explanation": "", "requested_changes": "1. While this is not necessary, I recommend the authors to re-implement their method in PyTorch/Tensorflow or any modern machine learning frameworks instead of MATLAB to allow others apply their methods. Note that all SOTA methods, e.g., $\\alpha$-$\\beta$-CROWN and MNBaB, have such implementations available.\n2. Please include a study with a wider set of $\\epsilon$, especially larger values.", "broader_impact_concerns": "No concern is identified.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Decision: Accept (poster)