Leveraging Over-Parameterization to Improve the Verifiability of Neural Networks

1 Introduction

Neural networks (NNs) have achieved remarkable progress: from solving well-defined challenges such as board games [Silver et al., 2016] and predicting protein structures [Varadi et al., 2024], to enabling broad, openended tasks like multimodal conversational agents [OpenAI, 2025]. One of the key factors in this success is overparameterization, i.e., equipping models with (far) more parameters than training data would dictate [Song et al., 2021; Ding et al., 2022; Belkin et al., 2019; Bunel et al., 2020; Oneto et al., 2023]. In practice, such models often generalize better than traditional approaches constrained to a balanced capacity, even when they can perfectly fit the training set. Despite the outstanding performance of overparameterized NNs and their promising potential in safetycritical domains [Zhang and Li, 2020; Bacciu et al., 2021; Wicker et al., 2018], their adoption remains hindered by the lack of formal guarantees, which raises significant risks. In fact, several studies have shown that NNs, including overparameterized ones, are vulnerable to input perturbations, whether arising from accidental noise [Goodfellow et al., Automated verification aims to address these issues by checking whether NNs satisfy desirable properties [Zhang and Li, 2020]. However, research in this area has prompted the inherent difficulty of the task. From a theoretical perspective, verifying properties of NNs composed solely of affine transformations and ReLU neurons is known to be NP-complete [Katz et al., 2017]. From a practical standpoint, this difficulty is evident, e.g., in the outcomes of the yearly competition of verification tools (VNNCOMP) [Brix et al., 2024]. The reasons behind these results are diverse. For instance, Mixed-Integer Linear Programming (MILP)-based and SMT-based verifiers [Ehlers, 2017; Tjeng and Tedrake, 2017; Wang et al., 2018a; Ryou et al., 2019; Singh et al., 2019] are highly sensitive to network size (i.e., number of parameters), since larger models correspond to larger and harder optimization problems. Abstractionbased verifiers [Gehr et al., 2018; Lemesle et al., 2024; Guidotti et al., 2021] mitigate complexity by overapproximating neuron behavior; however, coarse approximations often require refinement. This typically involves some forms of case-splitting which can rapidly escalate the number of subproblems, leading to substantial runtime increase. Similarly, branch-and-bound verifiers [Bunel et al., 2020; Zhou et al., 2025] and constraint-based approaches [Katz et al., 2019] struggle with networks of large size. Given these limitations, recent efforts to accelerate verification focused on reducing NN complexity. Strategies include enforcing sparsity and shrink network size [Xiao et al., 2019], reducing the number of neurons causing case-splitting [Xiao et al., 2019; Li et al., 2023], network pruning [Guidotti et al., 2020], and applying knowledge distillation to produce smaller yet highperforming models [Krizhevsky et al., 2012].

Our work addresses the following research question: Is it possible to leverage over-parameterization to improve both the accuracy of NNs and their verification time? In other words, rather than designing small models from the outset, reducing their size a posteriori, or mitigating costs solely by training to avoid expensive branching during verification, we explore how over-parameterization itself can be exploited to simultaneously enhance model accuracy and improve verification rutime. In particular, we propose to modify the learning phase of NNs to simultaneously minimize both some classical accuracy metric [Bishop and Bishop, 2023] and an auxiliary one that helps to control the number of neurons that turn out to be problematic during verification (e.g., the Rs loss) [Xu et al., 2024; Liu et al., 2025]. By considering a number of different architectures and training configurations, we show that over-parameterization can be exploited as an instrument to achieve high performance in both tasks. Our approach differs significantly from current state-of-theart methods, where the focus is typically on reducing network size or the number of problematic neurons during or after training, without explicitly investigating the impact of overparameterization on verification time. Our results demonstrate that, on all the NN architectures and the state-of-the-art tools that we consider, suitable over-parameterization will almost always yield models which are easier to verify and not substantially less accurate than their counterparts with baseline over-parameterization only.

The rest of the paper is organized as follows. In Section 2 we introduce some notations and definitions required to understand our contribution. In Section 3 we present our original methodology to train networks in order to yield improved accuracy and verification runtime. Experimental results involving different NN architectures and verification tools are presented and discussed in Section 4, and contextualized with related work in Section 5. We conclude the paper in Section 6 with some final remarks and directions for future work.

2 Preliminaries

Our notations and basic definitions are taken from [Huang et al., 2020]. An NN is defined as a tuple N = (S, T, Φ), where S = {Sk | k ∈ {1, . . . ,K}} is the set of layers, T ⊆ S × S denotes the connections between layers, and Φ = {ϕk | k ∈ {2, . . . ,K - 1}} is the set of functions associated with each non-input and output layer. In a deep NN, S1 is the input layer, SK is the output layer, and all other layers are hidden layers. Each layer Sk consists of sk neurons, with the l-th neuron denoted by nk,l and sk being the size of the layer. Each hidden or output node nk,l (2 ≤ k ≤ K - 1, 1 ≤ l ≤ sk) has a pre-activation value uk,l and a post-activation value vk,l. Input nodes n1,l only have post-activation values v1,l, and output nodes nK,l only have pre-activation values uK,l. Let uk and vk denote the vectors of all pre- and postactivation values in layer k. Each hidden layer is followed by a non-linear activation function to compute vk,l from uk,l. In this work, we use the ReLU (Rectified Linear Unit) activation function, defined as vk,l = max(0, uk,l), and we say that the neuron is active when vk,l = uk,l and inactive otherwise. A neuron is stable if it is either always active or always inactive and unstable otherwise.

In a fully connected (FC) layer, each neuron is connected to all neurons in the previous layer through a weight matrix W k of size ⟨sk, sk-1⟩, where wk l,h represents the weight from neuron h in layer k-1 to neuron l in layer k, plus a bias term bkfc

In a convolutional layer, connections are local and shared through learnable filters F k . Each filter is convolved over the input feature map vk-1 to produce an output feature map uk

where i, j are spatial indices, l is output channel, c is input channel, m, n are filter indices.

Let θ denote the set of all learnable parameters of a neural network N, i.e., the parameters that are optimized during training. Specifically, for FC and convolutional layers, we have

where W k and bkfc correspond to the weights and biases of the FC layers, and F k and bk correspond to the weights and biases of the convolutional layers. These parameters collectively define all trainable aspects of the network.

For a classification problem, the NN assigns a label to an input, i.e., the index of the output node with the largest value

2.1 Training NNs and the Over-Parameterization Effect

Given a training set, i.e., a set of inputs for which the corresponding output labels are known, the process of training a NN for a classification task involves finding values for the parameters θ to minimize an objective function that quantifies how well the model performs. Formally, the objective can be expressed as:L(θ) = Lmain(θ) + ∑i λi Laux,i(θ), (5)

where Lmain represents the task-specific loss, while the terms Laux,i denote auxiliary objectives, each scaled by a coefficient λi. For classification, the term Lmain is typically the cross-entropy loss [Bishop and Bishop, 2023], which acts as a differentiable proxy for the misclassification error over a set of samples, measuring the difference between predicted and true class labels. Auxiliary losses are also commonly defined as differentiable functions, and their aim is to obtain other desirable properties such as adherence to physical principles [Zampini et al., 2025], trustworthiness [Oneto et al., 2024], or improved generalization [Bishop and Bishop, 2023]. Optimization of L(θ) usually proceeds iteratively over multiple epochs, where one epoch corresponds to a complete pass over the training set. Within each epoch, the dataset is divided into mini-batches of manageable size: for each minibatch, the training algorithm computes predictions, evaluates the loss function, and derives the gradient ∇θL(θ) through a technique known as backpropagation [Bishop and Bishop, 2023]. Modern algorithms, such as Adam [Springer et al., 2021], are mostly adaptive gradient-based methods which dynamically adjust learning rates for each parameter.

It is well known [Bishop and Bishop, 2023] that one of the main pitfalls in training a NN is failing to yield a model that generalizes well, for instance by memorizing the training set, but failing to predict correctly samples which are not in the training set - a phenomenon known as overfitting. Interestingly, recent studies [Belkin et al., 2019; Oneto et al., 2023; Nakkiran et al., 2021] have shown that over-parameterization, i.e., adding many more parameters than those seemingly required to maintain good generalization capabilities, does not lead to overfitting, but acts as a form of implicit regularization. Contrary to the classical view of statistical learning theory, which posits a trade-off between fitting the training data and achieving good generalization, over-parameterized NNs suggest that the optimization dynamics of gradient-based methods and the structure of high-dimensional parameter spaces enable such NNs to converge toward solutions that generalize surprisingly well despite their apparent ability to memorize the training set.

2.2 Verifying NNs

Given a network N and a property ψ, verification is the process of checking whether N satisfies ψ. Here we focus on local robustness 1 properties: A NN is said to be locally robust around an input x with respect to a perturbation space P ϵ if the network's output does not change within the neighborhood defined by the bound, where ϵ defines the perturbation space. If x ∈ Rn we can define the P ϵ as the Lp ball centered in x

then a network is locally robust around x if ∀˜x ∈ P ϵ (x), class(x) = class(˜x). This ensures that, for all inputs within the ϵ-Lp ball centered in x, the network assigns the same label . In practice, for verification benchmarks, the L∞ norm is almost always the metric of choice.

Several approaches have been proposed and implemented in NN verification tools, many of which have been evaluated in VNN-Comp [Brix et al., 2024], an international event where tools are evaluated on a variety of NNs under different perturbation models. The set of constraints defining a property is in the VNN-LIB [Demarchi et al., 2023] language, a standard tailored for NN verification which draws from the SMT-LIB language [Barrett et al., 2010]. We focus on four state of the art tools that participated in recent VNN-Comp events: ABCROWN [Zhang et al., 2018; Xu et al., 2020; Salman et al., 2019; Xu et al., 2021; Wang et al., 2021; Zhang et al., 2022a; Zhang et al., 2022b; Kotha et al., 2023; Zhou et al., 2024a; Zhou et al., 2025], MARABOU [Wu et al., 2024], PYRAT [Lemesle et al., 2024], and PYNEVER [Demarchi et al., 2024b; Demarchi et al., 2024a; Demarchi et al., 2022; Guidotti et al., 2021]. ABCROWN is an efficient verifier based on the linear bound propagation framework, combined with specialized branch-andbound (B&B) techniques. PYRAT relies on abstract interpretation across multiple abstract domains, e.g., intervals, zonotopes and constrained zonotopes, to over-approximate reachable states and enable analysis of various NN architectures. MARABOU encodes verification tasks as constraint satisfaction problems, which are solved using a combination of simplex-based reasoning and symbolic propagation. Finally, PYNEVER adopts an abstraction-refinement approach based on symbolic bounds propagation and star sets to represent polytopes.

A key distinction in NN verification lies between incomplete and complete approaches [Huang et al., 2020; Guidotti et al., 2021]. Incomplete verification, e.g., based on abstract intepretation, is efficient but may return inconclusive results, whereas complete verification guarantees a definitive answer, e.g., by refining the abstract analysis. All the tools we consider support complete verification for feedforward NNs with ReLU activation functions. We can observe that the time to perform such verification is largely influenced by the number of unstable neurons [Katz et al., 2017]. Such neurons cannot be treated as linear functions of their inputs and must be handled by more expensive algorithms, e.g., case splitting, which may lead to an exponential growth of verification runtime in the size of the NN.

1 Verifying local robustness properties may also support checking for more general properties, see [Shriver et al., 2021]

2.3 Training for Verification

Given the impact of unstable neurons on the verification phase, training for verification approaches have been proposed to control and reduce their number in the training phase. The main idea is to estimate the lower and upper bounds of neuron pre-activation values, given some interval as input to the NN. The estimate forms the basis of auxiliary objectives that help to maintain the number of unstable neurons small while training. In the literature, we can find two main families of methods based on interval propagation: Naive Interval Propagation (NIP) [Xiao et al., 2019] is computationally efficient, but tends to overestimate bounds in NNs with many hidden layers; Symbolic Interval Propagation (SIP) [Wang et al., 2018b; Demarchi et al., 2024a], on the other hand, preserves symbolic dependencies to produce tighter bounds at the cost of a higher computational overhead than NIP. Once an estimate of unstable neurons is available, some function of such estimate must be added to the objective function of Eq. (5) as an auxiliary objective. A notable example of such a function is the so-called Rs loss [Devlin et al., 2019], a loss function that provides a differentiable measure of neuron stability. Rs loss is based on the following definition:

where lk,l and uk,l are the estimated lower and upper bounds of the pre-activation of neuron l in layer k. Here, k ∈ K indicates the set of layers intended to be stabilized, and l ∈ {1, . . . , nk} corresponds to the indices of the neurons in layer k, with nk denoting the number of neurons in that layer.

Its output lies in (-1, 1), approaching 1 for very stable neurons and -1 for very unstable ones. When training is performed in b mini-batches with dimension B, the bounds are averaged across the batch to obtain representative measures

Finally, the overall Rs loss is computed by summing contributions from all neurons of the K layers

The parameter λ controlling the relative weight of Lrs in Eq. (5) must be carefully tuned to avoid degrading the NN performance [Devlin et al., 2019].

Algorithm 1 Lambda Search

Input: N, dataset, prev acc, prev unst, ϵ, prev lambda, steps limit Output : opt model, metrics, n unst, next lambda 1: candidates← [] 2: min inc←MIN INC 3: max inc←MAX INC 4: increment← (min inc + max inc) / 2 5: opt model, metrics, next lambda←NULL 6: for step = 1 to steps limit do 7: λ ←prev lambda + increment 8: candidate, metrics ← TrainModel(N, dataset, λ) 9: n unst ← IntervalProp( candidate, ϵ, dataset.test set) 10: if metrics.accuracy > prev acc then 11: Append (metrics, n unst, λ) to candidates 12: min inc ← increment 13: increment ← (min inc + max inc) / 2 14: if n unst < prev unst then 15: next lambda ← λ 16: opt model ← candidate 17: return opt model, metrics, n unst, next lambda 18: end if 19: else 20: max inc ← increment 21: increment ← (min inc + max inc) / 2 22: end if 23: end for 24: if candidates ̸= [] then 25: opt model, metrics, n unst, λ ← SelectMin( candidates, key = n unst) 26: next lambda← λ 27: end if 28: return opt model, metrics, n unst, next lambda

3 Methodology

In the following, we assume that a class of NN architectures is predefined by specifying the number and type of hidden layers - either convolutional or FC - together with input and output layers appropriately sized for the dataset under consideration. In our training protocol, referred to as the Neuron Stability Protocol (NSP), we construct an ordered sequence of NN architectures belonging to the aforementioned class, where each architecture in the sequence is characterized by an increasing number of parameters, i.e., neurons in the hidden layers. The total number of parameters in each architecture approximately doubles with respect to the previous one in the sequence. The first architecture is selected so as to be capable of fitting the training set; heuristically, this is achieved by employing a number of parameters comparable to the number of samples in the dataset. The last architecture in the sequence is the largest one that can be trained while maintaining a reasonable use of computational resources 2 .

We train each architecture in the sequence using the Rs loss as an auxiliary objective. Since the verification process targets local robustness properties, we estimate the preactivation bounds through an interval propagation technique, considering an ϵ-L∞ ball centered on each training sample as input to the network. As previously discussed, setting the weight λ of the Rs loss term in the objective function of Eq. (5) is crucial. The smallest network in the sequence is trained with λ = 0, meaning that no neuron stability control is enforced for it. This network serves as a baseline, establishing the minimum acceptable test accuracy and the maximum tolerated number of unstable neurons for the subsequent architectures in the sequence. The goal of the NSP is therefore to identify the largest network and the corresponding nonzero value of λ that together yield effective over-parameterization while simultaneously reducing the number of unstable neurons. The underlying intuition is that over-parameterization enables both higher test accuracy and stronger regularization; in other words, larger networks can sustain higher values of λ without a loss in accuracy, thereby exhibiting fewer unstable neurons.

As part of the NSP, we developed an algorithm for the automatic tuning of λ, referred to as the Lambda Search Algorithm (LSA), whose pseudo-code is reported in Algorithm 1. Given a NN architecture N, a dataset, an initial minimum acceptable test accuracy prev acc, and a maximum tolerated number of unstable neurons prev unst, the algorithm iteratively determines the optimal value of λ starting from a minimum value prev lambda, within a maximum number of search steps steps limit, and using propagation intervals of size ϵ. For each architecture in the NSP sequence, the value of prev lambda corresponds to the λ used for the previous architecture, while prev unst denotes its associated number of unstable neurons. As customary, the dataset is assumed to be divided into a training set (dataset.train set) for parameter optimization and a test set (dataset.test set) for estimating generalization performance. LSA returns the best trained network for the given architecture (optimal model), along with the corresponding metrics (metrics), the estimated number of unstable neurons (n unst), and the selected value of λ (next lambda).

At each iteration of the main loop of the LSA (Lines 522), a candidate model is trained using the TrainModel function, which optimizes the following objective function:

where Lrs(θ) denotes the Rs loss, and Lmain(θ) is the standard cross-entropy loss. The hyperparameter λ (Line 6) is computed by incrementing prev lambda by a small adaptive step whose value lies within the constants MIN INC and MAX INC, defining the search window for λ. The candidate model is then evaluated via an interval propagation method (Line 8), which estimates the average number of unstable neurons (n unst) using ϵ-L∞ balls centered on each test sample. If the candidate model's accuracy improves over the previous iteration (Line 9), the triple containing (i) its performance metrics, (ii) the number of unstable neurons, and (iii) the corresponding λ value is stored, and the increment bounds are updated (Lines 11-12) for larger λ values. If the number of unstable neurons falls below prev unst, the search terminates early, returning the best λ along with the trained model and associated metrics. Otherwise, the search continues with smaller increments of λ (Lines 19-20). After at most steps limit iterations, if one or more candidate models have been collected (Line 23), the model exhibiting the lowest instability is selected as the optimal one by the SelectMinimum routine (Line 24). The corresponding λ and test accuracy are then propagated as reference values for the next, larger architecture in the NSP sequence. If a candidate model fails to improve test accuracy compared to previous architectures, it is simply discarded. The NSP introduces additional computational overhead during the training phase. If over-parameterized networks were trained without simultaneously enforcing neuron stability, the time required for interval propagation and for searching an appropriate value of λ could be saved. Nonetheless, this extra cost is justified by the improved neuron stability achieved by the resulting models.

2 In principle, there is no upper bound on the degree of over-parameterization of a NN. However, in practice, it is unnecessary to further increase the network size once the over-parameterization effect becomes evident.

4 Experimental Analysis

To assess whether NSP effectively achieves its intended goal and to collect empirical evidence addressing our main research question, we consider three classes of NN architectures commonly employed across application domains, namely:

• Shallow (SH) architectures, comprising a single FC hidden layer of dimension hdim;
• Complex (CX) architectures, comprising two FC hidden layers with dimensions hdim1 and hdim2;
• Convolutional (CV) architectures, consisting of a convolutional layer with either a 5×5 or 2×2 kernel (depending on the dataset), zero padding, stride 1, and 17 filters,
• followed by an FC hidden layer of dimension hdim. The number and size of the filters were optimized using Optuna [Akiba et al., 2019] to maximize accuracy;
• Convolutional Fixed (CF) architectures, which employ a pretrained, over-parameterized ResNet18 backbone followed by a single FC hidden layer of dimension hdim, which is the only component subject to verification.

For each architecture class, a family of networks with progressively increasing numbers of parameters was defined according to NSP. An overview of the corresponding dimensions is reported in Table 1. Each class was trained using both NSP and a standard machine learning approach, referred to as the baseline training protocol (BTP). The BTP adopts the same training configuration as NSP, but excludes the Rs loss term and the tuning of λ. The training and evaluation procedures are detailed in the following sections.

4.1 Experimental Setup

Three datasets were considered: MNIST, a dataset of grayscale handwritten digits, Fashion-MNIST (FMNIST), a more challenging dataset of grayscale images representing fashion items, and CIFAR-10, a dataset of RGB images of 10 different classes 3 . The SH, CX, and CV architectures were trained on MNIST. For FMNIST, only the CX and CV architectures were considered, while the CF architectures were trained on CIFAR-10. Due to the overparameterized design of the networks, all architectures achieved near 100% training accuracy on all datasets.

The CV models take as input a single-channel 28 × 28 image straight from the MNIST and FMNIST datasets, while the SH and CX networks receive a corresponding flattened vector of size 784; the CF models take as input a 32 × 32 RGB image. All networks produce an output of 10 neurons each representing one of the ten different classes. Both datasets were divided into 60,000 training samples - dataset.train set in Algorithm (1) - and 10,000 test samples - dataset.train set in Algorithm (1).

The training algorithm 4 was configured with the Adam optimizer having a fixed learning rate of 0.001, for 4,000 epochs and a batch size of 128 samples. We also experimented with adaptive learning rate schedulers, such as StepLR [Springer et al., 2021], under various configurations. However, maintaining a fixed learning rate ultimately led to more stable convergence and overall better performance. When using NSP, we set ϵ to 0.03 for MNIST and FMNIST and 0.169 for CIFAR-10, consistently with the properties that we verify, and we chose NIP for IntervalProp in LSA. In particular, the lower and upper bounds to estimate the stability of hidden layers neurons were computed using our own implementation for SH, CX and CFarchitectures, and an implementation based on auto LiRPA [Xu et al., 2020] for CV networks. We adopted the NIP approach over SIP to reduce the computational cost of the learning phase and avoid imposing time limits on the overall training procedure.

Verification was carried out considering 100 different local robustness properties for each dataset with the same noise considered during training. For all architectures except CF, the noise is applied to the input space, whereas for CF architectures it is applied to the feature space.

3 All data are retrieved from torchvision.datasets

4 Link to repository: https://github.com/NeVerTools/IJCAI-2026

We checked properties on trained NNs with ABCROWN, PYRAT, MARABOU, and PYNEVER 5 . Whenever possible we considered the same configuration of VNNCOMP 2024 [Brix et al., 2024] ensuring that each solver would performs complete verification. Each solver was allowed a fixed CPU time per instance. For MNIST, the limits were 15 seconds for the SH and CX classes and 60 seconds for the CV class. For FMNIST, the limits were 180 seconds for the CX class and 400 seconds for the CV class. For CIFAR-10, a time limit of 180 seconds was used for the CF architectures. For each neural network architecture, 100 instances were evaluated, and performance was assessed using the median runtime, which is robust to timed-out instances, and the number of cases in which the solver reached the allotted time limit without a conclusive answer. All experiments were conducted on five identical workstations equipped with an Intel Core i7-7400F CPU, 32 GB of RAM, and an NVIDIA RTX 5070 GPU, running Ubuntu 24.04.2 LTS. All NNs were implemented and trained using Python 3.10 and the PyTorch cu116 library, ensuring consistency across all experimental runs.

4.2 Experimental Results

Our first set of results concerns the learning phase and is reported in Table 2. In the table, for each architecture (column Architecture), we show the final accuracy on the training and test sets (column Acc. (Train/Test)) and the average estimated number of unstable nodes (column Unst. Nodes), both for BTP (first group) and NSP (second group). For NSP, we also report the final value of the parameter λ obtained through LSA. Missing entries in the table correspond to networks for which NSP failed to achieve any accuracy improvement. For both BTP and NSP, the estimate of unstable nodes is computed by NIP at the end of training and is obtained by averaging the number of unstable nodes calculated across all samples in the test set. From Table 2, we observe that the effect of over-parameterization emerges consistently across all architectures and under both training protocols. While the NSP protocol explicitly enforces this trend, under the BTP protocol the increase in accuracy arises naturally as a consequence of the larger network size. However, this trend is not strictly monotonic: for example, in the CX architectures trained with BTP, we observe a drop in test accuracy at CX-500, followed by a recovery as the network size further increases. Notably, when using NSP, we successfully reduced the number of unstable neurons compared to BTP across all architectures, except for the smallest ones in each class, where NSP uses λ = 0. Moreover, with NSP, the number of unstable neurons tends to decrease as network size increases in the CX and CV architectures, whereas in the SH architectures this pattern is less regular. Finally, the difference in accuracy between networks trained with BTP and NSP remains negligible, reflecting the trade-off introduced by the Rs loss term in NSP. As far as training runtime is concerned, the overhead of NSP over BTP remains confined to a 2× factor for each epoch on SH, CF and CV architectures, whereas it limited to a 3× factor on CX architectures. In Table 3, we present the results of running the solvers on the trained NNs. In the table, for each architecture (column Benchmark), we report the performance of the solvers (groups of columns labeled by solver name) in terms of median runtime and number of timeouts, expressed as <time>/<time-outs>. Results are shown for networks trained under both BTP and NSP (columns BTP and NSP, respectively, for each solver). The first observation from Table 3 is that, with the exception of the entries underlined, the number of properties causing solver time-outs consistently decreases when using NSP instead of BTP. We interpret this as clear evidence that the most challenging properties for each solver become verifiable within the allotted time limits once the number of unstable neurons is reduced. Importantly, this improvement does not come at the expense of accuracy. On the contrary, due to over-parameterization, NSP leads to increased accuracy and - somewhat counterintuitively for verification - networks of larger size. A second observation concerns the median runtimes, for which the picture is less conclusive. While it is generally true that verifying NNs trained with NSP is less computationally expensive than verifying their BTP-trained counterparts, the rate at which runtimes grow within the same class of architectures does not always favor NSP. In other words, although NSP typically reduces overall verification cost, its impact on runtime scalability is not uniformly positive across all architectures. Finally, we note that the trends discussed above appear to be largely independent of the specific internal algorithms used by each solver. Although some solvers perform better outof-the-box, reducing the number of unstable neurons through NSP - particularly for the most challenging properties - tends to yield benefits across nearly all solvers.

5 The version of the verifiers is the latest one as of Nov. 2025

4.3 Discussion

Our results suggest that combining structured regularization aimed at reducing the number of unstable neurons with overparameterization can improve both accuracy and verifiability, particularly for properties that are otherwise challenging for verifiers. Furthermore, our experiments provide an interesting perspective on whether NN verifiers are more sensitive to the number of unstable neurons or to network dimensionality. For the architectures we considered, ABCROWN, PYRAT, and PYNEVER exhibit only a modest increase in median runtime as the number of parameters grows, regardless of whether BTP or NSP is used. Conversely, MARABOU shows the greatest sensitivity to dimensionality and the least sensitivity to improvements in neuron stability. Overall, these findings suggest that coupling advanced learning techniques designed with verification in mind with solvers capable of exploiting the resulting network properties could represent a promising pathway toward scalable NN verification.

Despite these encouraging results, several limitations remain. A primary challenge is the computational overhead introduced by interval propagation methods used to estimate pre-activation bounds during training. While these techniques produce tight bounds for shallow networks, their precision and scalability deteriorate as network depth increases. In particular, although SIP yields tighter bounds than NIP, it incurs in significantly higher time and memory costs.

From a machine learning perspective, stacking many FC layers with ReLU activations provides no accuracy benefit, making SIP unnecessary in such settings. In contrast, deep convolutional architectures genuinely benefit from increased depth and are essential for achieving competitive accuracy on datasets such as CIFAR-10. However, in the literature regarding "learning-for-verification" approaches typically rely on small networks, achieving limited test accuracy (around 60%) [Xu et al., 2024] and operating far from the overparameterized regime [Liu et al., 2025]. Architectures required for high accuracy on CIFAR-10, remain impractical to train with current SIP-based regularization methods due to their computational cost. For these reasons, we restricted our experiments to relatively small architectures and we verified only the last layer in CF architectures.

Additionally, we relied on off-the-shelf solver implementations and did not optimize their internal algorithms to exploit the structural modifications induced by our training procedure. Future work should focus on improving interval analysis methods and adapting solvers to better leverage trainingtime regularization.

5 RelatedWorks

A broad spectrum of methodologies has been proposed in the literature to enhance the amenability of NNs to formal verification. A significant body of work has focused on improving the efficiency of verification algorithms based on MILP [Ehlers, 2017; Tjeng and Tedrake, 2017; Wang et al., 2018a; Ryou et al., 2019; Singh et al., 2019], which generally benefit from models characterized by a smaller number of variables. This property has been exploited by promoting sparsity within NN architectures [Xiao et al., 2019], thereby reducing the number of variables and accelerating the verification process. Moreover, alternative activation functions have been proposed as substitutes for ReLU, motivated by the observation that its linearization often induces excessive overapproximation. Since linearization constitutes a core strategy in many NN verification frameworks, a piecewise activation function exhibiting tighter linearizability was introduced in [Leofante et al., 2023], effectively mitigating this issue.

A complementary line of research explicitly targets the enforcement of ReLU stability [Xiao et al., 2019; Baninajjar et al., 2024; Xu et al., 2024; Li et al., 2023], thereby reducing the number of unstable neurons that exacerbate branching during verification. Such methods either prune marginally unstable neurons with negligible influence on predictive accuracy or incorporate dedicated regularization terms during training to promote neuron stability.

Another prominent research direction addresses the verification of large-scale architectures through model compression techniques, including pruning [Xiao et al., 2019; Guidotti et al., 2020; Min and Motani, 2020] and knowledge distillation [Shriver et al., 2019]. These approaches effectively concentrate the representational capacity of a large network into a smaller, verification-friendly model.

In contrast to these prevailing trends, our work explores an alternative paradigm. Specifically, we demonstrate that, for suitably dimensioned and trained architectures, it is possible to leverage over-parameterization [Belkin et al., 2019; Oneto et al., 2023; Nakkiran et al., 2021] to improve both learning performance and verifiability. When combined with a neuron-stability regularizer, over-parameterization enables the training of larger models that remain as verifiable as their smaller counterparts while achieving superior accuracy. This finding suggests that over-parameterization, traditionally regarded as a source of inefficiency, can instead be harnessed to concurrently enhance performance and facilitate verification, provided that appropriate regularization is applied.

6 Conclusions

Our study demonstrates that over-parameterization, traditionally regarded to improve generalization, can also play a decisive role in enhancing the verifiability of NNs. In particular, we introduced the Neuron Stability Protocol and its associated algorithm, which leverage increased network capacity to simultaneously improve accuracy and reduce neuron instability, thereby redefining the training objective to favor more verifiable models. These findings suggest that overparameterization should not be seen merely as a byproduct of modern deep learning practice or as an obstacle to verification, but rather as a deliberate design principle for achieving a balance between expressivity and formal verifiability. Future work will extend this analysis to more complex architectures and verification scenarios, with the goal of further elucidating the structural relationships among over-parameterization, accuracy, neuron stability, and verifiability in NNs.

Acknowledgements

This work has been partially supported by (i) the project ELSA - European Lighthouse on Secure and Safe AI, funded by the European Union's Horizon Europe programme under Grant Agreement No. 101070617; (ii) the project SERICS (PE00000014) under the NRRP MUR programme funded by the EU - NGEU; (iii) the project FAIR (PE00000013) under the NRRP MUR programme funded by the EU - NGEU; and (iv) the project FISA-2023-00128, funded by the MUR programme "Fondo italiano per le scienze applicate".