Uncovering the Limits of Proof Sharing for Neural Networks

# Uncovering the Limits of Proof Sharing for Neural Networks
Source: [https://arxiv.org/html/2608.19351](https://arxiv.org/html/2608.19351)
###### Abstract

Robustness verification of neural networks is increasingly important, due to their use in many critical domains\. In certain scenarios, proof sharing has been shown to accelerate incomplete verification techniques by reusing intermediate\-layer abstract states, or*templates*, across queries\. However, questions remain as to the robustness of template\-based acceleration across varying network architectures, properties, datasets, and training methods\. In this work, we perform a systematic study of the effectiveness of template\-based acceleration and its limits\. Our study shows that template subsumption rates can vary widely across scenarios\. We present a novel metric of*jointly stable neurons*to explain this variation, showing that in some cases template\-based techniques are very unlikely to provide any speedup\. Then, we presentFastCert, a novel technique for*automatically*distributing templates across neural network layers to increase performance impact, eschewing templates entirely if they are unlikely to produce a speedup\. Across a large set of covering\-design basedL0L\_\{0\}\-verification tasks,FastCertachieved an average speedup of1\.13×\{1\.13\\times\}over an extant template\-based reuse technique\.

## 1Introduction

Neural networks have emerged as the dominant paradigm for image classification, powering applications from autonomous driving to medical diagnosis\. Despite their success, it is established that carefully crafted perturbations known as adversarial examples can cause networks to misclassify inputs, while remaining imperceptible to human observers\[[35](https://arxiv.org/html/2608.19351#bib.bib18),[12](https://arxiv.org/html/2608.19351#bib.bib19),[5](https://arxiv.org/html/2608.19351#bib.bib20)\]\.

To mitigate these risks, there has been significant interest in creating certifiably robust neural networks, resistant to adversarial threats\[[18](https://arxiv.org/html/2608.19351#bib.bib24)\]\. These methods expose networks to adversarial perturbations during training, often leveraging formal verification techniques to guide and refine the optimization process\[[41](https://arxiv.org/html/2608.19351#bib.bib23),[20](https://arxiv.org/html/2608.19351#bib.bib22)\]\. Then, formal verifiers\[[42](https://arxiv.org/html/2608.19351#bib.bib27),[17](https://arxiv.org/html/2608.19351#bib.bib29)\]are used post\-training to guarantee the network’s robustness to specified perturbations, such as sound but incomplete verifiers based on abstract interpretation\[[30](https://arxiv.org/html/2608.19351#bib.bib8),[31](https://arxiv.org/html/2608.19351#bib.bib13),[41](https://arxiv.org/html/2608.19351#bib.bib23)\]\.

Recent work has shown that intermediate abstractions computed by such incomplete verifiers can be generalized into templates\[[37](https://arxiv.org/html/2608.19351#bib.bib1),[10](https://arxiv.org/html/2608.19351#bib.bib3)\], enabling proofs to bereusedand accelerating subsequent verification queries\. Typically, a small set of templates are derived by verifying localL∞L\_\{\\infty\}properties\[[35](https://arxiv.org/html/2608.19351#bib.bib18),[12](https://arxiv.org/html/2608.19351#bib.bib19),[18](https://arxiv.org/html/2608.19351#bib.bib24)\], each permitting perturbations within a related region of the input space\. These methods have been shown to be effective on related properties of the same input over the same or quantized networks, such as shifted patches or randomtt\-pixel perturbations over an image\. But, the effectiveness of template\-based acceleration has not been studied carefully in the context of other properties such asL0L\_\{0\}verification, a realistic threat model\[[15](https://arxiv.org/html/2608.19351#bib.bib47)\]where there have been significant recent advances in verification practicality\[[26](https://arxiv.org/html/2608.19351#bib.bib35),[28](https://arxiv.org/html/2608.19351#bib.bib37)\]\. Further, no work has studied the limits of template\-based acceleration across a variety of network architectures, properties, data sets, and training methods\.

Our first key contribution is a systematic framework characterizing when template reuse is a principled accelerator for robustness verification and when the verifier should instead run without it\. For a template\-based verifier to achieve speedups, a high percentage of verification queries must be subsumed by a small set of templates, but at the same time, each template must be precise enough to enable query verification\. We devise a novel metric of*jointly stable neurons*across a set of abstract states to explain the potential for template reuse given this tradeoff\. Through a limit study, we show that if the percentage of jointly stable neurons is low, extant template\-based proof sharing techniques are unlikely to provide any verification speedup\. Our measurements across several networks and training methods show that the potential for template\-based acceleration varies widely across scenarios\.

Given the observed variance in template effectiveness, there exists a need to automatically determine how best to employ templates for a given verification task\. Our second key contribution is a novel techniqueFastCertto*automatically*distribute templates across layers of a neural network to maximize performance impact, or eschew templates if they are unlikely to produce a speedup\.FastCertperforms profiling and template generation before verification, predicting template subsumption rates by sampling a very small set of queries\. We implementFastCertand show that for a state\-of\-the\-artL0L\_\{0\}verifier, it nearly always provides a greater speedup than previous proof\-sharing techniques in cases where templates can be effective, while significantly mitigating the slowdown when templates are ineffective\.

This paper makes the following contributions:

- •We perform a limit study of the effectiveness of template\-based proof reuse, characterize its potential success using a novel metric of jointly stable neurons and showing the success rate varies widely\.
- •We give a method to automatically determine whether, where, and how to apply template reuse for a given network and set of verification tasks\.
- •We implement our approach in a toolFastCertand demonstrate its practicality for accelerating covering\-design\-basedL0L\_\{0\}verification, with an average speedup of1\.13×\{1\.13\\times\}over the state\-of\-the\-art approach for applying templates \(a 7 hour reduction in wall\-clock time\.\)\.

## 2Background

Neural NetworksA neural networkNNis a functionN:ℝdin→ℝdoutN:\\mathbb\{R\}^\{d\_\{\\text\{in\}\}\}\\to\\mathbb\{R\}^\{d\_\{\\text\{out\}\}\}, commonly built from a composition of individual layersNL∘NL−1∘⋯∘N1N\_\{L\}\\circ N\_\{L\-1\}\\circ\\cdots\\circ N\_\{1\}\. We consider fully\-connected feed\-forward networks, where each layerNi​\(𝐱\)=ReLU​\(𝐀𝐱\+𝐛\)N\_\{i\}\(\\mathbf\{x\}\)=\\text\{ReLU\}\(\\mathbf\{A\}\\mathbf\{x\}\+\\mathbf\{b\}\)\. The Rectified Linear Unit \(ReLU\) activation appliesmax⁡\(⋅,0\)\\max\(\\cdot,0\)element\-wise\. For a classification task withccclasses, the network outputsdout:=cd\_\{\\text\{out\}\}:=cscores, assigning the class with the highest score as its prediction\. Fork<Lk<L,N1:kN\_\{1:k\}denotes the application of the firstkklayers andNk\+1:LN\_\{k\+1:L\}denote the finalL−kL\-klayers\.

Local Robustness VerificationGiven a set of inputs and a postconditionψ\\psi, neural network verification aims to prove thatψ\\psiholds on the network output for all given inputs\[[1](https://arxiv.org/html/2608.19351#bib.bib6)\]\.*Local robustness verification*proves thatψ\\psiholds for all network outputs corresponding to an input regionℐ⁡\(𝐱0\)\\mathcal\{I\}\(\\mathbf\{x\}\_\{0\}\)formed around some input𝐱0\\mathbf\{x\}\_\{0\}\. Formally, local robustness verification proves that∀𝐳∈ℐ⁡\(𝐱0\),N⁡\(𝐳\)⊧ψ\\forall\\mathbf\{z\}\\in\\mathcal\{I\}\(\\mathbf\{x\}\_\{0\}\),N\(\\mathbf\{z\}\)\\models\\psi\. We writeℐ⁡\(𝐱0\)⊧ψ\\mathcal\{I\}\(\\mathbf\{x\}\_\{0\}\)\\models\\psiif the property holds\.

Threat Models and SpecificationsTheL0L\_\{0\}threat model captures*sparse*perturbations: given an input𝐱0\\mathbf\{x\}\_\{0\}, the admissible regionℐL0​\(𝐱0,k\)\\mathcal\{I\}\_\{L\_\{0\}\}\(\\mathbf\{x\}\_\{0\},k\)is\{𝐳∣‖𝐱0−𝐳‖0≤k\}\\\{\\mathbf\{z\}\\mid\\\|\\mathbf\{x\}\_\{0\}\-\\mathbf\{z\}\\\|\_\{0\}\\leq k\\\}, allowing an adversary to arbitrarily modify up tokkinput features\[[34](https://arxiv.org/html/2608.19351#bib.bib31),[21](https://arxiv.org/html/2608.19351#bib.bib34),[8](https://arxiv.org/html/2608.19351#bib.bib36)\]\. Unlike norm\-bounded dense noise \(e\.g\., smallL∞L\_\{\\infty\}deviations\) that yields a single convex region, theL0L\_\{0\}model induces a combinatorial family of verification subproblems for one image, corresponding to the many choices of which features are altered\. In the patch threat model\[[6](https://arxiv.org/html/2608.19351#bib.bib32),[9](https://arxiv.org/html/2608.19351#bib.bib21)\], an adversary may arbitrarily perturb the pixels inside a single contiguousw×hw\\times hregion, leaving all other pixels unchanged; the input regionℐpatch​\(𝐱0,w,h\)\\mathcal\{I\}\_\{\\text\{patch\}\}\(\\mathbf\{x\}\_\{0\},w,h\)allows arbitrary changes to anyw×hw\\times hpatch within the image, yielding multiple verification subproblems across patch locations\. In geometric perturbations, the adversary applies a transformTδT\_\{\\delta\}from a prescribed family \(e\.g\., bounded rotation/contrast/brightness\), with parametersδ∈Δ\\delta\\in\\Delta; the input regionℐgeo​\(𝐱0,Δ\)=\{Tδ​\(𝐱0\)∣δ∈Δ\}\\mathcal\{I\}\_\{\\text\{geo\}\}\(\\mathbf\{x\}\_\{0\},\\Delta\)=\\\{T\_\{\\delta\}\(\\mathbf\{x\}\_\{0\}\)\\mid\\delta\\in\\Delta\\\}is typically non\-convex due to resampling/interpolation and is commonly verified by splittingΔ\\Deltainto finitely manyrrcases\[[2](https://arxiv.org/html/2608.19351#bib.bib4)\]\.

Robustness Under Adversarial ThreatsTo defend against the adversarial threat, specialized types of neural network training is employed\. It pursues a dual objective: minimize classification loss on data while maximizing robustness so predictions remain stable within the threat model\. PGD\[[18](https://arxiv.org/html/2608.19351#bib.bib24)\]training does this empirically by finding worst\-case perturbations per example and updating the model to classify them; IBP\[[20](https://arxiv.org/html/2608.19351#bib.bib22)\]training does it with sound guarantees by propagating bounds to certify that all inputs in a region keep the label and optimizing the certified margin\. Recent methods such as SABR\[[22](https://arxiv.org/html/2608.19351#bib.bib26)\]compute bounds on small, carefully selected subregions of the adversarial space to reduce approximation error and improve both standard and certified accuracy, while TAPS\[[19](https://arxiv.org/html/2608.19351#bib.bib25)\]combines IBP and PGD to optimize more precise but unsound worst\-case loss approximations\. CURE\[[13](https://arxiv.org/html/2608.19351#bib.bib33)\]targets multi\-norm robustness by regularizing and shaping networks so bounds remain tight across multiple norms\. For localized threats, certified patch defenses\[[6](https://arxiv.org/html/2608.19351#bib.bib32)\]extend guarantees from norm\-bounded noise to contiguous regions by reasoning over all patch placements\.

Verification via Abstract InterpretationScalable neural network verifiers typically rely on*abstract interpretation*\[[7](https://arxiv.org/html/2608.19351#bib.bib46),[30](https://arxiv.org/html/2608.19351#bib.bib8),[31](https://arxiv.org/html/2608.19351#bib.bib13),[32](https://arxiv.org/html/2608.19351#bib.bib30)\]to soundly overapproximate the set of reachable outputs\. The verifier first encodes the input region with a shape in some*abstract domain*\(e\.g\., boxes, zonotopes, or polyhedra\) that enclosesℐ⁡\(𝐱0\)\\mathcal\{I\}\(\\mathbf\{x\}\_\{0\}\)\. This shape is propagated layer by layer via*abstract transformers*that overapproximate each layer’s concrete operations\. Afterkklayers, the resulting*abstract state*SkS\_\{k\}overapproximates the concrete states reachable at that layer\. At the output layer,SLS\_\{L\}bounds all possible network outputs; if it also satisfies the postconditionψ\\psi, the property is certified to hold\. This approach is sound but incomplete: the overapproximation may be too coarse to prove a validψ\\psi\.

## 3Proof Templates

In this section, we describe template\-based proof sharing for incomplete verification and present a simple performance model for when reuse is beneficial\.

### 3\.1Preliminaries

Neural network verification via abstract interpretation has been optimized using*proof templates*\[[37](https://arxiv.org/html/2608.19351#bib.bib1),[10](https://arxiv.org/html/2608.19351#bib.bib3)\]\. A template at an intermediate layerkkis an abstract stateTkT\_\{k\}that has been certified to satisfy the postconditionψ\\psi, i\.e\.,Nk\+1:L\(Tk\)⊧ψN\_\{k\+1:L\}\(T\_\{k\}\)\\models\\psi\. To use a template for a new verification query, the verifier propagates the query to layerkk, obtaining abstract stateQkQ\_\{k\}\. IfQkQ\_\{k\}is fully contained within the template, termed*subsumption*, and denotedQk⊑TkQ\_\{k\}\\sqsubseteq T\_\{k\}, thenNk\+1:L\(Tk\)⊧ψN\_\{k\+1:L\}\(T\_\{k\}\)\\models\\psiimpliesNk\+1:L\(Qk\)⊧ψN\_\{k\+1:L\}\(Q\_\{k\}\)\\models\\psi, verifying the query without further propagation\.

In practice, the box domain is employed for representing templates\[[37](https://arxiv.org/html/2608.19351#bib.bib1),[10](https://arxiv.org/html/2608.19351#bib.bib3)\]: at layerkk, a box is a vector of intervals,Sk=⟨\[lj,uj\]⟩j=1nkS\_\{k\}=\\left\\langle\[l\_\{j\},u\_\{j\}\]\\right\\rangle\_\{j=1\}^\{n\_\{k\}\}, with each interval bounding the output of neuronjj\. Subsumption checking in the box domain is very efficient, making it desirable for templates\.

Figure 1:Template reuse in a 4\-layer network\. From an input imagexx, we first verify an initial query underℐ∞​\(x\)\\mathcal\{I\}\_\{\\infty\}\(x\), then build a layer\-k=2k\{=\}2template by iteratively relaxing the layer\-2 abstract state while it remains verifiable \(represented by the yellow region with dotted boundary\)\. For a later query underℐ0​\(x\)\\mathcal\{I\}\_\{0\}\(x\), the propagated layer\-2 query state is subsumed by the template, so the property is proved immediately and propagation through layers 3 and 4 is skipped, saving tail cost\.
### 3\.2Template Construction and Use

In prior work\[[10](https://arxiv.org/html/2608.19351#bib.bib3),[37](https://arxiv.org/html/2608.19351#bib.bib1)\], a verified query is leveraged to construct a proof template by generalizing its intermediate\-layer abstract state\. In[fig\.1](https://arxiv.org/html/2608.19351#S3.F1), the abstract interpreter first verifies anL∞L\_\{\\infty\}queryℐ∞​\(x\)\\mathcal\{I\}\_\{\\infty\}\(x\)—it computes an abstract state after each layer over\-approximating the result of passing the input region through the previous layers\. The query is considered verified if the final abstract state, computed after layer 4, satisfies the post\-conditionψ\\psi\. For[fig\.1](https://arxiv.org/html/2608.19351#S3.F1), as shown by the decision boundary after layer 4, the query is successfully verified\.

To construct a template, first, a set of layers is chosen at which to use templates\. At a selected layerkk, the previously\-computed abstract state is iteratively relaxed while preserving verifiability through the suffixNk\+1:LN\_\{k\+1:L\}, yielding a more general state that can subsume subsequent queries whose layer\-kkstates are similar\. Existing approaches commonly instantiate this procedure fromL∞L\_\{\\infty\}specifications\[[10](https://arxiv.org/html/2608.19351#bib.bib3),[37](https://arxiv.org/html/2608.19351#bib.bib1)\]: they first use binary search to find the largest verifiableL∞L\_\{\\infty\}\-ball around the input, then relax the resulting layer\-kkabstract state to maximize generality subject to successful propagation and discharge onNk\+1:LN\_\{k\+1:L\}\. The resulting relaxed state is stored as a template at layerkk, which can be reused for potential subsumption of future queries\. Moreover, prior work shows that replacing a singleL∞L\_\{\\infty\}\-ball over the input space with multiple maskedL∞L\_\{\\infty\}\-balls over subregions yields a more diverse template set and increases subsumption rates\[[10](https://arxiv.org/html/2608.19351#bib.bib3),[37](https://arxiv.org/html/2608.19351#bib.bib1)\]\.

Using templates requires checking if the abstract shape computed for a subsequent query is subsumed by a template \(see[section3\.1](https://arxiv.org/html/2608.19351#S3.SS1)\)\. For[fig\.1](https://arxiv.org/html/2608.19351#S3.F1), a template is placed after layer 2 \(the yellow region with dotted boundary\), and a subsequent query aims to verify anL0L\_\{0\}queryℐ0​\(x\)\\mathcal\{I\}\_\{0\}\(x\)\. Since the abstract state for this query is contained within the layer 2 template, the property is verified, without further propagation of the abstract state through the remaining layers\.

### 3\.3A Performance Model for Template\-Based Verification

The potential performance improvement provided by proof sharing with templates is impacted by various factors, and depending on the template subsumption rate, templates may even lead to a slowdown \(which we observed in practice\)\. We will refer back to the model presented here when discussing the potential for template\-based speedups for different networks \([section4](https://arxiv.org/html/2608.19351#S4)\) and presenting our technique for automatically optimizing template usage \([section5](https://arxiv.org/html/2608.19351#S5)\)\.

Consider a networkNNwithLLlayers and a fixed inputxxinducingrrverification specifications\. Fix a reuse layerkkand a template set𝒯\\mathcal\{T\}of sizemm\. Lettgent\_\{\\mathrm\{gen\}\}denote the one\-time cost to construct𝒯\\mathcal\{T\};tpref​\(k\)t\_\{\\mathrm\{pref\}\}\(k\)the per\-specification cost to propagate throughN1:kN\_\{1:k\};tmatch​\(m\)t\_\{\\mathrm\{match\}\}\(m\)the per\-specification cost to test subsumptionQk⊑TQ\_\{k\}\\sqsubseteq Tfor allT∈𝒯T\\in\\mathcal\{T\}; andttail​\(k\)t\_\{\\mathrm\{tail\}\}\(k\)the per\-specification cost to complete verification overNk\+1:LN\_\{k\+1:L\}when no match occurs\. Letρk∈\[0,1\]\\rho\_\{k\}\\in\[0,1\]be the fraction of therrspecifications whose layer\-kkabstract state is subsumed by at least one template in𝒯\\mathcal\{T\}\. The expected end\-to\-end verification time with template reuse is then,

tgen\+r⁡\(tpref​\(k\)\+tmatch​\(m\)\+\(1−ρk\)​ttail​\(k\)\)t\_\{\\mathrm\{gen\}\}\+r\\Bigl\(t\_\{\\mathrm\{pref\}\}\(k\)\+t\_\{\\mathrm\{match\}\}\(m\)\+\(1\-\\rho\_\{k\}\)\\,t\_\{\\mathrm\{tail\}\}\(k\)\\Bigr\)\(1\)
Under the assumption that the baseline verification exhibits approximately constant per\-layer computational costν\\nu, it follows thattpref​\(k\)=k​νt\_\{\\mathrm\{pref\}\}\(k\)=k\\nu,ttail​\(k\)=\(L−k\)​νt\_\{\\mathrm\{tail\}\}\(k\)=\(L\-k\)\\nu,tgen=λ​m​L​νt\_\{\\mathrm\{gen\}\}=\\lambda mL\\nufor template creation time parameterλ\>0\\lambda\>0andtmatch​\(m\)=η​mt\_\{\\mathrm\{match\}\}\(m\)=\\eta mfor template matching time parameterη\>0\\eta\>0\. SpeedupSS, relative to baseline verification timer​L​νrL\\nuis therefore,

S=\(1\+λ​mr\+η​mL​ν−ρk​L−kL\)−1S\\;=\\;\\Bigl\(1\+\\lambda\\tfrac\{m\}\{r\}\+\\tfrac\{\\eta m\}\{L\\nu\}\-\\rho\_\{k\}\\tfrac\{L\-k\}\{L\}\\Bigr\)^\{\-1\}\(2\)
HenceS\>1S\>1is precisely when the*saved tail cost*ρk​\(L−k\)/L\\rho\_\{k\}\(L\-k\)/Lexceeds the*amortized overheads*of template generation and lookup,λ​m/r\+η​m/\(L​ν\)\\lambda m/r\+\\eta m/\(L\\nu\)\. Operationally, this favors \(i\)*earlier viable layers*where\(L−k\)/L\(L\-k\)/Lis large, provided the queries yields a sufficiently highρk\\rho\_\{k\}; \(ii\)*a small number of templates*to keep lookup and generation costs small; and \(iii\)*large number*of specifications, which amortizetgent\_\{\\mathrm\{gen\}\}\. Using templates at very deep layers \(small residual\) or oversized template sets \(large overhead\) eliminate gains, in which case the template based approach might not be beneficial\.

With this speedup model, prior work\[[37](https://arxiv.org/html/2608.19351#bib.bib1),[10](https://arxiv.org/html/2608.19351#bib.bib3)\]has shown that template reuse can yield significant performance gains for patch verification, fixed\-sizeL0L\_\{0\}verification, and geometric perturbations\. In such scenarios, verification instances countrris typically a few hundred and template set lengthmmis up to 4\. However, prior work did not perform a rigorous study of the impacts of neural network type, dataset, training method, and layer choice on the effectiveness of template\-based proof sharing\.

## 4The Limits of Template\-Based Proof Sharing

Here, we first present a model for understanding the limits of existing template\-based proof sharing techniques to speed neural network verification, based on the concept of*neuron stability*\. Then, we present a limit study of template\-based proof reuse, showing its applicability varies widely depending on specific settings\.

### 4\.1Efficient Proof Sharing and Neuron Stability

For efficient proof sharing via templates,[section3\.3](https://arxiv.org/html/2608.19351#S3.SS3)shows that we need \(1\) a high template match rate, \(2\) low cost to compute templates, and \(3\) low cost to determine template subsumption for an abstract shape\. Further, there is a baseline correctness condition that \(4\) the abstract interpreter can verify the property for the template\. Here, we explore how neuron stability interacts with these conditions, specifically how many unstable neurons make it very unlikely all four conditions can be simultaneously satisfied\.

Neural network ReLU activation layers \(see[section2](https://arxiv.org/html/2608.19351#S2)\) act element\-wise, suppressing negative pre\-activations and preserving positive ones\. ReLU therefore partitions neurons into active \(positive output\) and inactive \(zero output\) sets, creating an activation pattern\. In abstract interpretation, when propagating an abstract state through the network, ReLU layers are the primary source of imprecision\. For the box domain, given an abstract state for a neuronjjrepresented by the interval\[lj,uj\]\[l\_\{j\},u\_\{j\}\], the abstract interpreter must determine the effect of applying ReLU on the interval\. This requires a case analysis based on the containment of 0 in\[lj,uj\]\[l\_\{j\},u\_\{j\}\], as 0 is the ReLU decision boundary\. Hence, the precision of the abstract interpretation hinges on whether the abstract state of the pre\-activation value of a neuron is sufficient to determine the outcome of its ReLU activation\.

A neuron is considered*stable*\[[4](https://arxiv.org/html/2608.19351#bib.bib5),[25](https://arxiv.org/html/2608.19351#bib.bib7)\]if its pre\-activation interval,\[lj,uj\]\[l\_\{j\},u\_\{j\}\], does*not*cross the ReLU’s decision boundary of 0\. This occurs under two conditions:

- •The interval is entirely non\-negative \(lj≥0l\_\{j\}\\geq 0\), meaning the neuron is*always active*and the ReLU function consistently acts as the identity\.
- •The interval is entirely non\-positive \(uj≤0u\_\{j\}\\leq 0\), meaning the neuron is*always inactive*and the ReLU behaves as the constant zero function\.

In both cases, the activation behavior is fixed across all concrete behaviors represented by the abstract state, hence the term*stability*\.

A neuron is*unstable*if its interval\[lj,uj\]\[l\_\{j\},u\_\{j\}\]has a negative lower bound and a positive upper bound \(lj<0<ujl\_\{j\}<0<u\_\{j\}\)\. For such neurons, the abstract state is too coarse to resolve the sign of the pre\-activation value\. Consequently, a sound abstract transformer for the ReLU function must conservatively account for both outcomes \(an active or inactive neuron\), typically leading to precision loss\. For an abstract stateSkS\_\{k\}, we denote the sets of indices for stable and unstable neurons asStable⁡\(Sk\)\\mathrm\{Stable\}\(S\_\{k\}\)andUnstable⁡\(Sk\)\\mathrm\{Unstable\}\(S\_\{k\}\), respectively\.

##### Induced Partial Orders

The subsumption relation⊑\\sqsubseteqon abstract states \([section3\.1](https://arxiv.org/html/2608.19351#S3.SS1)\) has direct implications for neuron stability\. If a stateQkQ\_\{k\}is subsumed by a templateTkT\_\{k\}, any unstable neuron inQkQ\_\{k\}must also be unstable inTkT\_\{k\}\. This is because the query’s interval\[ljQ,ujQ\]\[l\_\{j\}^\{Q\},u\_\{j\}^\{Q\}\]containing zero implies the necessarily wider template interval\[ljT,ujT\]\[l\_\{j\}^\{T\},u\_\{j\}^\{T\}\]also contains zero\. This yields the following inclusion relation unstable neuron sets:

Qk⊑Tk⟹Unstable⁡\(Qk\)⊆Unstable⁡\(Tk\)Q\_\{k\}\\sqsubseteq T\_\{k\}\\quad\\implies\\quad\\mathrm\{Unstable\}\(Q\_\{k\}\)\\subseteq\\mathrm\{Unstable\}\(T\_\{k\}\)Hence, a template must accommodate all the instabilities present in any query it subsumes\. Similarly, the sets of stable neurons are related by the inclusionStable⁡\(Tk\)⊆Stable⁡\(Qk\)\\mathrm\{Stable\}\(T\_\{k\}\)\\subseteq\\mathrm\{Stable\}\(Q\_\{k\}\)\.

##### Template Generality vs\. Stability Variance

The effectiveness of proof sharing hinges on a trade\-off between template generality and the stability of individual queries\. For a small set of templates to be effective, each template must be general enough to subsume a large number of queries\. But, for a single templateTkT\_\{k\}capable of subsuming a set of queries\{Qki\}i=1m\\\{Q^\{i\}\_\{k\}\\\}\_\{i=1\}^\{m\},Unstable⁡\(Tk\)\\mathrm\{Unstable\}\(T\_\{k\}\)must include the*union*of the unstable neurons of the queries:

⋃iUnstable⁡\(Qki\)⊆Unstable⁡\(Tk\)\\bigcup\_\{i\}\\mathrm\{Unstable\}\(Q^\{i\}\_\{k\}\)\\subseteq\\mathrm\{Unstable\}\(T\_\{k\}\)\(3\)
Hence, a very general template must account for all the instabilities present in the queries it subsumes\. This instability set can grow large if the queries exhibit*diverse*instability patterns, with differing unstable neurons across the abstract states for individual queries\.111In principle, a neuron that is stable in each individual query can still be forced unstable in a template if it is stably active in some queries and stably inactive in others\. We observed no such cases in our experiments\.Such instability variance poses a fundamental challenge to creating a compact and effective set of templates: a template that abstracts over a large number of unstable neurons is likely too imprecise to enable verification of the property of interest\. \(Every unstable ReLU necessitates an over\-approximation, introducing precision loss that compounds layer\-by\-layer, often rendering the final bounds too loose to be conclusive\.\) And, since efficient template computation and matching is required for speedups, this issue cannot be sidestepped by larger template sets or more complex templates\.

### 4\.2Neuron Instability in Practice

Here, we describe a study that shows the limits of proof sharing via templates in practice and the relationship of neuron stability patterns to proof sharing potential\.

MethodologyWe used the MNIST and CIFAR\-10 datasets in our study\. We considered six neural networks for each dataset, varying in training methods\. Alongside standard training, we tested the training methods PGD\[[18](https://arxiv.org/html/2608.19351#bib.bib24)\], SABR\[[22](https://arxiv.org/html/2608.19351#bib.bib26)\], TAPS\[[19](https://arxiv.org/html/2608.19351#bib.bib25)\], CURE\[[13](https://arxiv.org/html/2608.19351#bib.bib33)\], and CertifiedPatchDefense \(CPD\)\[[6](https://arxiv.org/html/2608.19351#bib.bib32)\]\. All the networks used in the limit study consist of 7 fully connected layers, with 200 neurons per layer\.

We considered three perturbation types to generate verification queries from a common input image that yield large number of queries and are amenable to be analyzed via abstract interpretation based verifiers: \(1\) randomL0L\_\{0\}perturbations of 1 to 30 pixels generating 1000 queries, \(2\) localized2×22\\times 2patch perturbations generating 729 queries for MNIST images and 1024 queries for CIFAR\-10 images, and \(3\) composite geometric transformations used in prior work on MNIST\[[2](https://arxiv.org/html/2608.19351#bib.bib4),[10](https://arxiv.org/html/2608.19351#bib.bib3)\]including±2∘\\pm 2^\{\\circ\}rotation,±10%\\pm 10\\%contrast and±1%\\pm 1\\%brightness changes split intorrperturbations\. We presentL0L\_\{0\}perturbations as a representative case; results for patch and geometric perturbations, which exhibit similar trends, are deferred to[Appendix 1](https://arxiv.org/html/2608.19351#Pt0.A1)\.

For each generated query, we propagate the input region with DeepZ and record the abstract stateQkiQ^\{i\}\_\{k\}at each ReLU layerkkwithnkn\_\{k\}neurons\. For a query set\{Qki\}i=1m\\\{Q^\{i\}\_\{k\}\\\}\_\{i=1\}^\{m\},*Jointly Stable Neurons*at percentilep∈\[0,1\]p\\in\[0,1\]is the fraction of neurons stable in at least app\-fraction of the queries:

JointlyStableNeuronsp\(\{Qki\}i=1m\)=\|\{j:\|\{i:j∉Unstable⁡\(Qki\)\}\|m≥p\}\|nk\\mathrm\{JointlyStableNeurons\}\_\{p\}\(\\\{Q^\{i\}\_\{k\}\\\}\_\{i=1\}^\{m\}\)=\\frac\{\\left\|\\left\\\{j:\\dfrac\{\|\\\{i:j\\notin\\mathrm\{Unstable\}\(Q^\{i\}\_\{k\}\)\\\}\|\}\{m\}\\geq p\\right\\\}\\right\|\}\{n\_\{k\}\}\(4\)Atp=1p=1, this is the fraction of neurons outside the union of unstable neurons across all queries at that layer, i\.e\.,1−\|⋃iUnstable⁡\(Qki\)\|/nk1\-\|\\bigcup\_\{i\}\\mathrm\{Unstable\}\(Q^\{i\}\_\{k\}\)\|/n\_\{k\}\. By[eq\.3](https://arxiv.org/html/2608.19351#S4.E3), a smaller value means any template subsuming all queries must contain many unstable neurons\. A steep drop asppincreases indicates that instability is dispersed across queries, so templates covering an increasing fraction of queries must include more unstable neurons, limiting their effectiveness for proof sharing\.

In[figs\.2](https://arxiv.org/html/2608.19351#S4.F2)and[3](https://arxiv.org/html/2608.19351#S4.F3), we plotJointly Stable Neuronsand template subsumption for all the ReLU layers of networks trained on MNIST and CIFAR\-10, respectively, using 100 input images per network; shaded bands indicate variability across images\. The x\-axis gives the percentile thresholdppexpressed as a percentage, and the y\-axis givesJointlyStableNeuronsp​\(\{Qki\}i=1m\)\\mathrm\{JointlyStableNeurons\}\_\{p\}\(\\\{Q^\{i\}\_\{k\}\\\}\_\{i=1\}^\{m\}\)as a percentage of neurons at that layer\. We use one template generated underL∞L\_\{\\infty\}perturbation for subsumption checking; following the template generation technique described in[section3\.2](https://arxiv.org/html/2608.19351#S3.SS2)\.

\(a\)Jointly stable neurons\(b\)Template subsumption rates
Figure 2:Jointly stable neurons and template subsumption rates under random\-L0L\_\{0\}perturbations in MNIST networks\.\(a\)Jointly stable neurons\(b\)Template subsumption rates
Figure 3:Jointly stable neurons and template subsumption rates under random\-L0L\_\{0\}perturbations in CIFAR\-10 networks\.Subsumption RatesFirst, focusing on the template subsumption rates in[figs\.2](https://arxiv.org/html/2608.19351#S4.F2)and[3](https://arxiv.org/html/2608.19351#S4.F3), we see a significant variance across datasets, layers, and training methods\. Consistent with prior observations\[[37](https://arxiv.org/html/2608.19351#bib.bib1)\], later layers consistently have higher subsumption rates, as by that point the networks tend to distill the semantic features of the input, enabling similar queries to yield similar abstract states\.

Training method has a substantial impact on potential subsumption rates\. Networks trained without specific certifiable guarantees, the Standard and PGD trained models, exhibit generally lower subsumption rates: for MNIST this is most pronounced in the earlier layers, while for CIFAR\-10 it persists across all layers\. In contrast, networks trained with certified objectives \(CURE, CPD, SABR, TAPS\) are designed to satisfy worst\-case guarantees against perturbations, and thus tend to emphasize features that remain informative despite variations in the perturbations\. We see these behaviors reflected in generally higher subsumption rates for these training methods across both datasets\.

However, even for certified\-trained networks, the subsumption rates vary significantly across layers, and across datasets\. E\.g\., the subsumption rate at layer 2 on MNIST for TAPS roughly 80% whereas for CPD its less than 60%\. This unpredictability led us to develop the profiling technique for automating template configuration described in[section5](https://arxiv.org/html/2608.19351#S5)\.

Joint Stability[Figures2](https://arxiv.org/html/2608.19351#S4.F2)and[3](https://arxiv.org/html/2608.19351#S4.F3)show that in nearly all cases, greater joint stability across abstract states correlates with higher template subsumption, as expected\. For the majority of the cases, we observe that jointly stable neurons drop quickly asppincreases at the first layer for all networks\. Hence, if a single template were to subsume a majority of these abstract states, it must have a high number of unstable neurons, and hence would be unlikely to enable verification of the desired property\. The very low subsumption rates at the first layer confirm this predicted ineffectiveness\. Conversely, at later layers, the drop in jointly stable neurons is significantly less, indicating that the template will not have to accommodate high instability\. And consequently, we observe higher subsumption at these layers\.

We do observe some interesting exceptions to these trends\. On CIFAR\-10 Standard and PGD in[fig\.3](https://arxiv.org/html/2608.19351#S4.F3), earlier layers exhibit high joint stability across percentile of queries, but subsumption remains low\. These cases indicate that while joint stability captures a key prerequisite for reuse, it does not guarantee that the resulting per\-neuron bounds align tightly enough across queries to be subsumed by a few templates\. Even with similar joint stability, early\-layer abstract states may be insufficiently distilled \(or too high\-variance in interval geometry\)\. Dataset complexity likely plays a role as well\. As MNIST is far less feature\-rich than CIFAR\-10, homogenic semantic structure may emerge earlier in the network, allowing early\-layer templates to be useful\. For example, consider the TAPS and SABR\-trained MNIST networks in[fig\.2](https://arxiv.org/html/2608.19351#S4.F2); unlike their CIFAR\-10 counterparts, they exhibit some subsumption even in the first layer, and joint stability is maintained\.

CURE on MNIST in[fig\.2](https://arxiv.org/html/2608.19351#S4.F2)illustrates a nuanced case\. Although joint stability drops at stricter percentile thresholds, the drop is not severe at the coverage levels relevant to the observed subsumption rates\. In particular, subsumption rates remain around60−80%60\-80\\%starting from layer 2, and the joint stability curves indicate that a large fraction of neurons remain jointly stable for a comparable fraction of queries\. Thus, the low stability at the highest percentiles does not rule out reuse: it says that a single template is unlikely to cover nearly all queries without absorbing additional instability\. Templates can still be effective when targeting a substantial, but not exhaustive, subset of the queries\.

Overall, the results indicate that joint stability effectively explains subsumption rates for template\-based proof sharing\.222Similar trends hold for patch and geometric perturbations; results are deferred to[Appendix 1](https://arxiv.org/html/2608.19351#Pt0.A1)\.The data show that the effectiveness of such proof sharing is highly configuration\-dependent; a fixed policy for where and how to use templates will not generalize across these settings\. In the next section, we describe a new adaptive strategy to automatically adapt to these varying conditions\.

## 5Automatic Configuration of Templates

The practical efficacy of template\-based proof sharing is critically dependent on a combination of factors: the training methodology, the specific property under verification, the cardinality of the template set used, and the choice of layer for reuse\. An uninformed use of templates could actually degrade overall verification performance, a phenomenon we have observed in practice\.

Prior work\[[10](https://arxiv.org/html/2608.19351#bib.bib3),[37](https://arxiv.org/html/2608.19351#bib.bib1)\]largely sidestepped this parameterization challenge, relying on manual, empirical measurements to select a fixed set ofL∞L\_\{\\infty\}\-masked templates, and up to two promising layers for template reuse\. While this methodology has demonstrated viability in constrained settings, manual tuning will not scale to a wide variety of real\-world scenarios; the experiments of[section4\.2](https://arxiv.org/html/2608.19351#S4.SS2)alone \(including the results in[Appendix 1](https://arxiv.org/html/2608.19351#Pt0.A1)\) consider hundreds of combinations of training method, layer choice, and perturbation type\.

Further, there have been significant advances inL0L\_\{0\}verification via techniques like Calzone\[[26](https://arxiv.org/html/2608.19351#bib.bib35)\]and CoverD\[[28](https://arxiv.org/html/2608.19351#bib.bib37)\], makingL0L\_\{0\}verification increasingly practical but posing new challenges for proof sharing\. These methods have expanded verification settings from fixed\-sizett\-pixel perturbations to arbitrarykk\-pixel perturbations wherek\>tk\>t\. Calzone\[[26](https://arxiv.org/html/2608.19351#bib.bib35)\]exploits the observation that robustness for anyk\>tk\>tperturbed pixels implies robustness for everyttsubset\. It predicts a largekkvia dynamic programming and sampling, then uses covering designs to generatekk\-sized queries, submitted to a verifier, refining to smaller sets as needed\. CoverD\[[28](https://arxiv.org/html/2608.19351#bib.bib37)\]advances this covering\-based approach by proposing covering verification designs, an algorithm that selects between candidate coverings without constructing them but rather predicting their block\-size distributions from closed\-form mean/variance, then constructing the chosen covering on\-the\-fly\. The volume and structural complexity of queries generated by such methods can vary dramatically\. Prior work\[[37](https://arxiv.org/html/2608.19351#bib.bib1)\]demonstrates template reusability for random 3\-pixel perturbations, but covering\-design\-based approaches involve verifying perturbations that may alter 100 or more pixels, making them a challenging testbed for template reuse\.

To improve the applicability of template reuse, we introduce a lightweight,*a priori*profiling technique\. This technique provides a principled method to \(i\) identify and prune verification scenarios where using templates is futile, and \(ii\) automatically select a set of advantageous layers and curate a compact set of templates to maximize anticipated performance gain\.

Algorithm 1FastCertLayer and Templates Selection1:Input:Network

NN, image

xx, candidate layers

ℒcand\\mathcal\{L\}\_\{\\mathrm\{cand\}\}, sampling size

PP, candidate template counts

ℳ\\mathcal\{M\}\.

2:Output:Set of pairs

\(k,𝒯k\)\(k,\\mathcal\{T\}\_\{k\}\)of selected layers and their template sets

3:

𝗏𝗂𝖺𝖻𝗅𝖾←\[\]\\mathsf\{viable\}\\leftarrow\[\]
4:foreach

k∈ℒcandk\\in\\mathcal\{L\}\_\{\\mathrm\{cand\}\}do

5:

\(m⋆,ρk⋆,𝒯k⋆\)←None\(m^\{\\star\},\\rho\_\{k\}^\{\\star\},\\mathcal\{T\}\_\{k\}^\{\\star\}\)\\leftarrow\\text\{None\}
6:foreach

m∈ℳm\\in\\mathcal\{M\}do

7:*// Buildmmtemplates at layerkkfrom imagexx*

8:

𝒯k\(m\)←∅\\mathcal\{T\}\_\{k\}^\{\(m\)\}\\leftarrow\\emptyset
9:Generate

mmnumber of

L∞L\_\{\\infty\}m​a​s​k​smasks
10:for

i=1i=1to

mmdo

11:Compute template

TiT\_\{i\}at layer

kkusing

m​a​s​ki\{mask\}\_\{i\}; add

TiT\_\{i\}to

𝒯k\(m\)\\mathcal\{T\}\_\{k\}^\{\(m\)\}
12:endfor

13:*// Estimate subsumption on the set ofPPL0L\_\{0\}queries on imagexx*

14:

c​\_​hit←0c\\\_\{\{\\rm hit\}\}\\leftarrow 0
15:for

j=1j=1to

PPdo

16:Sample a

L0L\_\{0\}query on

xx; compute

QjQ\_\{j\}at layer

kk
17:for

i=1i=1to

mmdo

18:if

Qj⊑TiQ\_\{j\}\\sqsubseteq T\_\{i\}then

19:

c​\_​hit←c​\_​hit\+1c\\\_\{\{\\rm hit\}\}\\leftarrow c\\\_\{\{\\rm hit\}\}\+1break

20:endif

21:endfor

22:endfor

23:

ρk​\(m\)←c​\_​hit/P\\rho\_\{k\}\(m\)\\leftarrow c\\\_\{\{\\rm hit\}\}/P
24:*// Cost\-model viability test*

25:if

ρk​\(m\)≥ρkmin​\(k,m,r\)\\rho\_\{k\}\(m\)\\geq\\rho\_\{k\}^\{\\min\}\(k,m,r\)then

26:*// Keep the best viable\(m,ρ\)\(m,\\rho\)for this layer determined by subsumption*

27:

\(m⋆,ρk⋆,𝒯k⋆\)←\(m,ρk​\(m\),𝒯k\(m\)\)\(m^\{\\star\},\\rho\_\{k\}^\{\\star\},\\mathcal\{T\}\_\{k\}^\{\\star\}\)\\leftarrow\(m,\\rho\_\{k\}\(m\),\\mathcal\{T\}\_\{k\}^\{\(m\)\}\)
28:endif

29:endfor

30:if

\(m⋆,ρk⋆,𝒯k⋆\)≠None\(m^\{\\star\},\\rho\_\{k\}^\{\\star\},\\mathcal\{T\}\_\{k\}^\{\\star\}\)\\neq\\text\{None\}then

31:Append

\(k,ρk⋆,m⋆,𝒯k⋆\)\(k,\\rho\_\{k\}^\{\\star\},m^\{\\star\},\\mathcal\{T\}\_\{k\}^\{\\star\}\)to

𝗏𝗂𝖺𝖻𝗅𝖾\\mathsf\{viable\}
32:endif

33:endfor

34:return

\{\(k,𝒯k⋆\):\(k,⋅,⋅,𝒯k⋆,⋅\)∈𝗏𝗂𝖺𝖻𝗅𝖾\}\\\{\(k,\\mathcal\{T\}\_\{k\}^\{\\star\}\):\(k,\\cdot,\\cdot,\\mathcal\{T\}\_\{k\}^\{\\star\},\\cdot\)\\in\\mathsf\{viable\}\\\}

### 5\.1Layer Selection and Template Set Refinement

In practice, not all layers are equally suitable for template reuse\. Early layers may exhibit low subsumption rates \(see[section4\.2](https://arxiv.org/html/2608.19351#S4.SS2)\), while very late layers offer limited potential savings due to the small residual depth\. And, the number of templates must be balanced against lookup costs, as larger template sets increase both generation and matching overheads\. Identification of a set of layers and template sets that can exhibit the highest potential for subsumption is governed by the performance model from[section3\.3](https://arxiv.org/html/2608.19351#S3.SS3)\. We leverage this model in[algorithm1](https://arxiv.org/html/2608.19351#alg1)to guide the selection of layers and templates forFastCert\. The algorithm takes as input a network, an input image, a set of candidate reuse layersℒcand\\mathcal\{L\}\_\{\\mathrm\{cand\}\}, sampling sizePP, and a set of candidate template countsℳ\\mathcal\{M\}\. It evaluates each layer\-template configuration\(k,m\)\(k,m\)to assess its viability for template reuse, and outputs the set of viable\(k,m\)\(k,m\)configurations\.

At each layer, to achieve a speedupS\>1S\>1, the subsumption fractionρk\\rho\_\{k\}must exceed a minimum thresholdρkmin\\rho\_\{k\}^\{\\min\}that depends on the amortized overheads and the residual network depth,L−kL\-k\. This threshold is derived from[eq\.2](https://arxiv.org/html/2608.19351#S3.E2):

ρkmin=\(λ​mr\+η​mL​ν\)​LL−k\(k<L\)\.\\rho\_\{k\}^\{\\min\}\\;=\\;\\Bigl\(\\lambda\\,\\tfrac\{m\}\{r\}\+\\tfrac\{\\eta\\,m\}\{L\\,\\nu\}\\Bigr\)\\,\\frac\{L\}\{\\,L\-k\\,\}\\qquad\(k<L\)\.
Layers with subsumption fractions below a minimum thresholdρkmin\\rho\_\{k\}^\{\\min\}will not yield sufficient savings to justify the overhead of matching\. In[algorithm1](https://arxiv.org/html/2608.19351#alg1),FastCertevaluates each candidate layerk∈ℒcandk\\in\\mathcal\{L\}\_\{\\mathrm\{cand\}\}and each candidate template countm∈ℳm\\in\\mathcal\{M\}, using an estimation of the subsumption fractionρk​\(m\)\\rho\_\{k\}\(m\)by sampling a set of diverseL0L\_\{0\}queries and computing the fraction subsumed by a set ofmmtemplates\. A layer\-template configuration\(k,m\)\(k,m\)is viable if it meets the thresholdρk​\(m\)≥ρkmin​\(k,m,r\)\\rho\_\{k\}\(m\)\\geq\\rho\_\{k\}^\{\\min\}\(k,m,r\)\.

ℒviable=\{k∈ℒcand:ρk≥ρkmin\},\\mathcal\{L\}\_\{\\mathrm\{viable\}\}=\\\{k\\in\\mathcal\{L\}\_\{\\mathrm\{cand\}\}:\\rho\_\{k\}\\geq\\rho\_\{k\}^\{\\min\}\\\},
If no layer\-template configuration meets the viability threshold, the algorithm returns an empty set and verification proceeds without templates\. This design ensures that template\-based verification is applied only when empirical evidence suggests a net performance gain, gracefully degrading to standard verification when template reuse is unprofitable\.

## 6Methodology

In this section, we describe the methodology used to experimentally validate the effectiveness ofFastCert\.

### 6\.1Configuration

We instantiateFastCertwith verification queries generated by Calzone\[[26](https://arxiv.org/html/2608.19351#bib.bib35)\]and CoverD\[[28](https://arxiv.org/html/2608.19351#bib.bib37)\], two state\-of\-the\-artL0L\_\{0\}robustness verification frameworks\. Both frameworks generate verification queries using covering designs to efficiently explore the space of possible pixel perturbations\. While the original Calzone and CoverD frameworks fall back to complete solvers when search tree over pixel sets is exhausted and reaches leaf nodes, we exclusively use the incomplete verifier for all queries\. This isolates the performance impact of template reuse as an improvement on the core abstract interpretation backend\.

Figure 4:Sampling size vs\. subsumption rate estimates for MNIST PGD with 4 templates\.To create a comprehensive yet tractable evaluation, we generate a total of 750,000 verification queries per network\. This total was derived from 10 images per network\. We instantiate the workload fortt\-pixel perturbation tasks witht=3t=3with Calzone and CoverD\. They employ covering\-design to generate query sets whose perturbed pixel counts,k\>tk\>t, can vary significantly, producing a heterogeneous set of verification problems\. For each image, we cap the workload at 75,000 queries\. To ensure consistent query set across different methods compared, we cache the sampling phase of Calzone/CoverD and reuse across all evaluations\.

To estimate the subsumption rateρk\\rho\_\{k\}at each candidate layer, we perform a brief profiling run on a small sample ofP=200P=200queries per image\. Across networks and layers, subsumption estimates vary substantially for small samples \(up to∼\\sim150 queries\), but stabilize around∼\\sim200 queries\. Importantly, the threshold\-crossing decision is not sensitive to sampling variability beyond this point \(e\.g\.,[fig\.4](https://arxiv.org/html/2608.19351#S6.F4)\)\. We give more data justifying our choice ofPPin[Appendix 2](https://arxiv.org/html/2608.19351#Pt0.A2)\.

To balance template diversity against lookup costs, we consider a set of candidate template set sizes of,ℳ=\{1,2,4\}\\mathcal\{M\}=\\\{1,2,4\\\}\.ℒcand\\mathcal\{L\}\_\{\\mathrm\{cand\}\}includes the layers where the minimum subsumption fractionρkmin\\rho\_\{k\}^\{\\min\}is less than or equal to 1 for at least onem∈ℳm\\in\\mathcal\{M\}, ensuring that only layers with potential for speedup are considered\.

We evaluateFastCerton fully\-connected and convolutional networks trained on MNIST and CIFAR\-10 \(summarized in[table1](https://arxiv.org/html/2608.19351#S6.T1)\)\. The suite includes standard, robust, and certified\-trained models of varied sizes used in prior work\[[26](https://arxiv.org/html/2608.19351#bib.bib35),[28](https://arxiv.org/html/2608.19351#bib.bib37),[10](https://arxiv.org/html/2608.19351#bib.bib3),[37](https://arxiv.org/html/2608.19351#bib.bib1)\]\. As we observed that SABR and TAPS trained networks exhibited substantially lower verifiability under Calzone/CoverD\-generatedL0L\_\{0\}perturbation queries with our incomplete verifier domains, we exclude them from the final evaluation set\.

We base our evaluation usingDeepZ\[[30](https://arxiv.org/html/2608.19351#bib.bib8),[10](https://arxiv.org/html/2608.19351#bib.bib3)\]and Box\[[20](https://arxiv.org/html/2608.19351#bib.bib22)\]abstract domains, and compareFastCertagainst two baseline techniques for both the domains\. The first one is a standard verification approach that does not attempt template\-based proof sharing\. The other one uses a static, hand\-picked reuse strategy described in prior work\. It always enables template reuse with one template \(m=1m=1\) at fixed, pre\-selected layers \(layers 2 and 3\[[10](https://arxiv.org/html/2608.19351#bib.bib3),[37](https://arxiv.org/html/2608.19351#bib.bib1)\]\)\. This allows us to measure the benefit ofFastCert’s layer and template selection strategy over the state\-of\-the\-art policy\.

Table 1:Networks used in theFastCertevaluation\.
### 6\.2Implementation and Environment

FastCertis implemented in Python and extends theDeepZ\[[30](https://arxiv.org/html/2608.19351#bib.bib8),[10](https://arxiv.org/html/2608.19351#bib.bib3)\]verifier\. We integrated the query generation algorithms from Calzone\[[26](https://arxiv.org/html/2608.19351#bib.bib35)\]and CoverD\[[28](https://arxiv.org/html/2608.19351#bib.bib37)\]to create our verification tasks\. All experiments were conducted on a Google Cloud Platform instance equipped with a 12\-core Intel Cascade Lake CPU, 85GB of RAM, and an NVIDIA A100 GPU with 40GB of memory\.

## 7Experimental Evaluation

We conducted an empirical evaluation to validate the efficacy ofFastCert\. The evaluation showed that the naive reuse of existing policy for template\-based proof sharing can be detrimental to performance, and that our automated, profile\-guided approach can both mitigate this pitfall and maximize gains\. Our investigation was structured around the following research questions:

- •RQ1: What is the impact of the previous fixed\-layer template reuse strategy on end\-to\-end verification time forL0L\_\{0\}verification queries?
- •RQ2: In cases where the previous strategy reduces verification performance, canFastCert’s ability to detect when template reuse is futile mitigate the performance reduction? What is the overhead of the profiling process in this scenario?
- •RQ3: In cases where the extant reuse strategy improves verification performance, what further performance gains are obtained fromFastCert’s automated selection of layers and template count?
- •RQ4: DoesFastCertgeneralize across the abstract domains used by incomplete verifiers, in settings where template reuse is applicable?

We answer RQ1 through RQ4 respectively in[sections7\.1](https://arxiv.org/html/2608.19351#S7.SS1),[7\.2](https://arxiv.org/html/2608.19351#S7.SS2),[7\.3](https://arxiv.org/html/2608.19351#S7.SS3)and[7\.4](https://arxiv.org/html/2608.19351#S7.SS4)\. Finally, we discuss limitations in[section7\.5](https://arxiv.org/html/2608.19351#S7.SS5)\.

Table 2:Calzone results \(750K queries, 10 images, t=3\) with DeepZ and Box domains\. V=Verified\(%\), T=Baseline \(No Template\) Time in seconds, Sub=Subsumption rate \(%\), Spd=Speedup, E=Extant Template Reuse Strategy, F=FastCert\.\(a\) MNIST

\(b\) CIFAR\-10

Table 3:CoverD results \(750K queries, 10 images, t=3\) with DeepZ and Box domains\. V=Verified\(%\), T=Baseline \(No Template\) Time in seconds, Sub=Subsumption rate \(%\), Spd=Speedup, E=Extant Template Reuse Strategy, F=FastCert\.\(a\) MNIST

\(b\) CIFAR\-10

### 7\.1Performance of Extant Template Reuse Policy

Extant reuse yields substantial speedups on networks where subsumption is moderately high, but consistently slows verification when subsumption is very low\. From[tables2](https://arxiv.org/html/2608.19351#S7.T2),[3](https://arxiv.org/html/2608.19351#S7.T3)and[5](https://arxiv.org/html/2608.19351#S7.F5), we observe two distinct behaviors,When reuse is viable,extant reuse achieves speedup ranging1\.01×−1\.91×1\.01\\times\-1\.91\\timeson Calzone, and1\.02×−1\.88×1\.02\\times\-1\.88\\timesin CoverD\.When reuse is futile,extant reuse slows down verification by1%−14%1\\%\-14\\%on Calzone and7%−14%7\\%\-14\\%on CoverD\. This performance degradation arises because the overhead of template matching outweighs the negligible savings from subsumption\. The performance degradation in these cases is predicted by the template reuse cost model in[section3\.3](https://arxiv.org/html/2608.19351#S3.SS3), and by the measures of joint stability from[eq\.4](https://arxiv.org/html/2608.19351#S4.E4)presented in[section4](https://arxiv.org/html/2608.19351#S4), particularly in[figs\.2](https://arxiv.org/html/2608.19351#S4.F2)and[3](https://arxiv.org/html/2608.19351#S4.F3)\.

### 7\.2Efficacy of Automated Futility Detection

In scenarios where template reuse is detrimental,FastCert’s automated futility detection effectively avoids slowdowns\. Automated futility detection inFastCertcan identify these scenarios and disable reuse, preventing slowdowns\. Our profiling step figures out quickly that no layers are viable for reuse, returning empty layer\-template configuration set \([algorithm1](https://arxiv.org/html/2608.19351#alg1)\)\. This avoids the added overhead of template matching, resulting in verification times comparable to the baseline without reuse, as seen in[tables2](https://arxiv.org/html/2608.19351#S7.T2)and[3](https://arxiv.org/html/2608.19351#S7.T3)\. The remaining slowdown stems from template creation and matching against 200L0L\_\{0\}queries per image during profiling, but this cost is negligible compared to the 75,000 verification queries per image\.FastCertonly incurs an average slowdown of1\.6%1\.6\\%\(ranging over1%−4%1\\%\-4\\%\), a significant improvement over the10\.1%10\.1\\%\(ranging over1%−14%1\\%\-14\\%\) average slowdown observed with extant template reuse\. This is demonstrated across both Calzone and CoverD in[fig\.5](https://arxiv.org/html/2608.19351#S7.F5), whereFastCertconsistently outperforms extant reuse in futile scenarios\.

### 7\.3Advantage in Favorable Scenarios

In configurations where template reuse is effective,FastCert’s automated selection of reuse layers and template counts improves over extant reuse, ultimately achieving an average of1\.13×\{1\.13\\times\}\(ranging over0\.98×−1\.5×0\.98\\times\-1\.5\\times\) performance gain overall\.

Figure 5:Combined speedup results across all 48 configurations:FastCertoutperforms extant reuse in 46, ties in one, and is slightly slower in one; the overall improvement is statistically significant according to a paired two\-sided Wilcoxon signed\-rank test \(W=4W=4,p=3\.1×10−9p=3\.1\\times 10^\{\-9\}\)\.Overall,FastCertachieves speedups of up to2\.10×2\.10\\timeson MNIST networks \(e\.g\.,CPDBig\) and up to1\.86×1\.86\\timeson CIFAR\-10 networks \(e\.g\.,CPDBig\) compared to no template reuse \([tables2](https://arxiv.org/html/2608.19351#S7.T2),[3](https://arxiv.org/html/2608.19351#S7.T3)and[5](https://arxiv.org/html/2608.19351#S7.F5)\)\. These peak improvements arise becauseFastCert\(i\) identifies layers with higher template subsumption and \(ii\) chooses template counts that increase hit rate while controlling template\-matching overhead\. For example, for a representative MNIST input onCPDMedfor Calzone,FastCertapplies two templates each at layers 2 and 3, and one template each at layers 4 and 5\. In contrast, extant reuse relies on a static, manually chosen configuration;FastCertadapts reuse layers and template counts to the subsumption behavior of each network and dataset\.

In CPDConv the gains are minor since reuse occurs only at late linear layers followed by convolutional layers, which constrains subsumption potential and leaves little room for improvement\[[37](https://arxiv.org/html/2608.19351#bib.bib1)\]\.

### 7\.4Generality Across Abstract Domains

We evaluateFastCertwith both DeepZ and Box, two abstract domains that are compatible with template reuse as identified in prior work\[[10](https://arxiv.org/html/2608.19351#bib.bib3)\]\. We also experimented with another widely used abstract domain, Polyhedra \(with DeepPoly\[[31](https://arxiv.org/html/2608.19351#bib.bib13)\]\), but found them impractically slow at our evaluation scale: for example, onCPDMed\(MNIST\) under CoVerD with 750k queries and no template reuse, DeepPoly is8\.08×8\.08\\timesslower than DeepZ and9\.54×9\.54\\timesslower than Box\. Accordingly, we focus our evaluation on DeepZ and Box\.

From[fig\.5](https://arxiv.org/html/2608.19351#S7.F5), we observe thatFastCertachieves almost similar speedup trends in both domains, with slightly better performance in Box\. Specifically,FastCertachieves0\.98×−1\.29×0\.98\\times\-1\.29\\timesspeedup over extant reuse in DeepZ with an average of1\.10×1\.10\\times, and1\.01×−1\.5×1\.01\\times\-1\.5\\timesspeedup over extant reuse in Box domain with an average of1\.17×1\.17\\timesacross the tools and datasets\. This shows thatFastCertgeneralizes well across both the abstract domains\.

### 7\.5Limitations

We study template reuse for robustness verification in the incomplete\-verifier setting, and instantiateFastCertwith the incomplete verification backends of Calzone and CoVerD\. While these tools may ultimately invoke a complete procedure when the abstract domain cannot discharge a query at the leaf levels,FastCertoperates only on the incomplete backend and is agnostic to any subsequent complete verification step\. Our work is limited to verification queries generated from a single input image \(local robustness\)\. Extending template reuse across multiple inputs; for example, to support global robustness properties or batched/multi\-input settings, is another promising direction\. The performance model used in this work employs a constant per layer cost to derive viability threshold\. Verification cost can depend on the layer type, size and on the abstract domain; although our end\-to\-end measurements capture this variation, extendingFastCertwith a layer\-aware cost model may further improve its configuration decisions\.

## 8Related Work

DNN Verification\.Existing DNN verifiers can be broadly classified as complete or incomplete\[[11](https://arxiv.org/html/2608.19351#bib.bib14),[30](https://arxiv.org/html/2608.19351#bib.bib8),[31](https://arxiv.org/html/2608.19351#bib.bib13),[29](https://arxiv.org/html/2608.19351#bib.bib10),[47](https://arxiv.org/html/2608.19351#bib.bib12),[43](https://arxiv.org/html/2608.19351#bib.bib9),[45](https://arxiv.org/html/2608.19351#bib.bib43),[24](https://arxiv.org/html/2608.19351#bib.bib11),[26](https://arxiv.org/html/2608.19351#bib.bib35),[28](https://arxiv.org/html/2608.19351#bib.bib37)\]\. Incomplete methods trade some precision for scalability, enabling the verification of larger and more complex networks that complete methods struggle to handle\. Most of the prior works on DNN verification is focused onL∞L\_\{\\infty\}verification\[[11](https://arxiv.org/html/2608.19351#bib.bib14),[30](https://arxiv.org/html/2608.19351#bib.bib8),[31](https://arxiv.org/html/2608.19351#bib.bib13)\]\. UnlikeL∞L\_\{\\infty\}robustness,L0L\_\{0\}robustness induces a discrete, combinatorial, non\-convex perturbation space, making scalable certification substantially more challenging\. Calzone\[[26](https://arxiv.org/html/2608.19351#bib.bib35)\]and CoverD\[[28](https://arxiv.org/html/2608.19351#bib.bib37)\]address this challenge with covering designs, reducingtt\-pixel robustness to large collections of variable\-sizekk\-pixel queries withk\>tk\>t; in practice, this can produce tens to hundreds of thousands of related queries per image\. More recent work\[[27](https://arxiv.org/html/2608.19351#bib.bib28)\]advances this line by characterizing the convex hull of anL0L\_\{0\}ball as the intersection of its bounding box and a scaledL1L\_\{1\}\-like polytope\. Prior template\-reuse work demonstrates benefits on much smaller fixed\-sizeL0L\_\{0\}workloads, but none study whether template reuse remains effective in covering\-design setup\.

Incremental Verification\.Incremental verification has improved the scalability of traditional program verification to an industrial scale\[[14](https://arxiv.org/html/2608.19351#bib.bib38),[16](https://arxiv.org/html/2608.19351#bib.bib39),[23](https://arxiv.org/html/2608.19351#bib.bib40),[33](https://arxiv.org/html/2608.19351#bib.bib41)\]\. Incremental program analysis tasks reuse partial results\[[44](https://arxiv.org/html/2608.19351#bib.bib44)\], constraints\[[39](https://arxiv.org/html/2608.19351#bib.bib45)\], and precision information\[[3](https://arxiv.org/html/2608.19351#bib.bib42)\]from previous runs for faster analysis of individual commits\. Program changes typically affect a small, localized part of the code, whereas DNN updates modify weights across many layers without altering control flow\. This key difference makes incremental DNN verification a distinct challenge in comparison to program analysis\.

Similarly, many recent works\[[37](https://arxiv.org/html/2608.19351#bib.bib1),[10](https://arxiv.org/html/2608.19351#bib.bib3),[36](https://arxiv.org/html/2608.19351#bib.bib17),[38](https://arxiv.org/html/2608.19351#bib.bib16),[46](https://arxiv.org/html/2608.19351#bib.bib15)\]have successfully used incremental verification for improving the efficiency of DNN verification\. These works include incremental complete verification\[[36](https://arxiv.org/html/2608.19351#bib.bib17),[46](https://arxiv.org/html/2608.19351#bib.bib15)\], incremental probabilistic verification\[[38](https://arxiv.org/html/2608.19351#bib.bib16)\]and incremental incomplete verification\[[37](https://arxiv.org/html/2608.19351#bib.bib1),[10](https://arxiv.org/html/2608.19351#bib.bib3)\]\. Our work extends this line by systematically analyzing when and how verification effort can be reused effectively, providing both theoretical and automated support for template reuse\.

Wei et al\.\[[40](https://arxiv.org/html/2608.19351#bib.bib2)\]considers incremental incomplete verification of relatively small DNNs with last\-layer perturbation\. Fischer et al\.\[[10](https://arxiv.org/html/2608.19351#bib.bib3)\]introduced proof transfer to reuse verification effort across different input specifications of a single network, achieving up to 2\.9x reduction in verification cost but with limited applicability to convolutional layers\. Complementarily, Ugare et al\.\[[37](https://arxiv.org/html/2608.19351#bib.bib1)\]extended this idea to transfer proofs across approximate networks by introducing a template transformation technique that enables sound and efficient verification for networks with convolutional architectures\. Our work builds on these ideas by conducting a limit study of template effectiveness, identifying conditions where template reuse is counterproductive, and proposing an automated system that decides when, where, and how to apply template reuse efficiently\.

## 9Conclusions

We have presented a study of the limits of template\-based proof sharing for neural network verification\. We showed that certain combinations of networks, training methods, and datasets are fundamentally unsuited to template\-based speedups, due to excessive variance in jointly stable neurons\. Then, we gave a new technique for automatically determining how best to apply templates to a verification task, including automatic detection of when templates should not be used\. We implemented our technique in a toolFastCert, and an experimental evaluation showed that it improves over a state\-of\-the\-art template technique, providing greater speedup in cases where templates work well and significantly reducing slowdown in cases where they are unsuitable\.

## Appendix Appendix 1Joint Stability for Other Perturbations

[Section4\.2](https://arxiv.org/html/2608.19351#S4.SS2)presented trends in joint stability and subsumption rates forL0L\_\{0\}perturbations\. We observed similar joint stability and template subsumption trends across patch and geometric perturbations as well\. In[figs\.6](https://arxiv.org/html/2608.19351#Pt0.A1.F6)and[7](https://arxiv.org/html/2608.19351#Pt0.A1.F7), we plot the jointly stable neurons and template subsumption rates across different2×22\\times 2patch perturbation scenarios in MNIST and CIFAR\-10 networks\. And in[figs\.8](https://arxiv.org/html/2608.19351#Pt0.A1.F8),[9](https://arxiv.org/html/2608.19351#Pt0.A1.F9),[10](https://arxiv.org/html/2608.19351#Pt0.A1.F10)and[11](https://arxiv.org/html/2608.19351#Pt0.A1.F11), we plot the jointly stable neurons and template subsumption rates across geometric perturbations for MNIST networks\. Here,±2∘\\pm 2^\{\\circ\}rotation,±10%\\pm 10\\%contrast and±1%\\pm 1\\%brightness changes are split intor=r=4, 6, 8, and 10 perturbations, respectively resulting in 64, 216, 512 and 1000 queries per image\[[10](https://arxiv.org/html/2608.19351#bib.bib3),[2](https://arxiv.org/html/2608.19351#bib.bib4)\]\. The common trends of earlier layers having lower joint stability and subsumption rates, and later layers having higher joint stability and subsumption rates hold in these perturbation scenarios as well\. The interesting cases observed in[section4\.2](https://arxiv.org/html/2608.19351#S4.SS2); e\.g\., CIFAR\-10 Standard and PGD networks, with earlier layers having higher joint stability but still very low subsumption rates in[fig\.3](https://arxiv.org/html/2608.19351#S4.F3)forL0L\_\{0\}perturbations are also observed in[fig\.7](https://arxiv.org/html/2608.19351#Pt0.A1.F7)for patch perturbations\. Similarly, trends reported for SABR, TAPS, and CURE MNIST networks in[fig\.2](https://arxiv.org/html/2608.19351#S4.F2)remain identical in the patch and geometric perturbation scenarios under[figs\.6](https://arxiv.org/html/2608.19351#Pt0.A1.F6),[8](https://arxiv.org/html/2608.19351#Pt0.A1.F8),[9](https://arxiv.org/html/2608.19351#Pt0.A1.F9),[10](https://arxiv.org/html/2608.19351#Pt0.A1.F10)and[11](https://arxiv.org/html/2608.19351#Pt0.A1.F11)\.

\(a\)Jointly stable neurons\(b\)Template subsumption rates
Figure 6:Jointly stable neurons and template subsumption rates under2×22\\times 2patch perturbations in MNIST networks\.\(a\)Jointly stable neurons\(b\)Template subsumption rates
Figure 7:Jointly stable neurons and template subsumption rates under2×22\\times 2patch perturbations in CIFAR\-10 networks\.\(a\)Jointly stable neurons\(b\)Template subsumption rates
Figure 8:Jointly stable neurons and template subsumption rates under geometric perturbations \(4 splits\) in MNIST networks\.\(a\)Jointly stable neurons\(b\)Template subsumption rates
Figure 9:Jointly stable neurons and template subsumption rates under geometric perturbations \(6 splits\) in MNIST networks\.\(a\)Jointly stable neurons\(b\)Template subsumption rates
Figure 10:Jointly stable neurons and template subsumption rates under geometric perturbations \(8 splits\) in MNIST networks\.\(a\)Jointly stable neurons\(b\)Template subsumption rates
Figure 11:Jointly stable neurons and template subsumption rates under geometric perturbations \(10 splits\) in MNIST networks\.
## Appendix Appendix 2Sampling Sizes for Subsumption Estimation

\(a\)MNIST\(b\)CIFAR\-10
Figure 12:Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 1 template\.\(a\)MNIST\(b\)CIFAR\-10
Figure 13:Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 2 templates\.\(a\)MNIST\(b\)CIFAR\-10
Figure 14:Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 4 templates\.[Figures12](https://arxiv.org/html/2608.19351#Pt0.A2.F12),[13](https://arxiv.org/html/2608.19351#Pt0.A2.F13)and[14](https://arxiv.org/html/2608.19351#Pt0.A2.F14)fully detail our evaluation of how many sampledL0L\_\{0\}queries are needed to reliably estimate layer\-wise subsumption for the algorithm of[section5](https://arxiv.org/html/2608.19351#S5)\. For each network, we select 10 input images \(MNIST/CIFAR\-10\) and sample verification queries by perturbing 5 to 20 randomly chosen pixels\. For each layer, we plot the estimated subsumption rate against a fixed set of templates as a function of the number of sampled queries \(10\-600\)\. For each configuration, we repeat this process 10 times and plot the mean \(as solid lines\) and standard deviation \(as shaded regions\)\. We also plot the minimum subsumption rate required to yield speedup \(dotted\), computed byFastCert’s performance model \([section3\.3](https://arxiv.org/html/2608.19351#S3.SS3)\)\. The plots are generated against different template counts of 1, 2, and 4\.

Across networks and layers, subsumption estimates vary substantially for small samples \(up to∼\\sim150 queries\), but stabilize around∼\\sim200 queries\. Importantly, the threshold\-crossing decision is not sensitive to sampling variability beyond this point \(e\.g\.,[fig\.4](https://arxiv.org/html/2608.19351#S6.F4)\)\. While in rare cases, such as MNIST CPDMed with 2 templates[fig\.13\(a\)](https://arxiv.org/html/2608.19351#Pt0.A2.F13.sf1), at layer 1, estimated subsumption falls very close to the threshold, even with larger samples of 600 queries, the variability remains similar\. In almost all other cases, the gap between the estimated subsumption rate and the threshold to select or skip a layer for template reuse remains clear\.

Thus we conclude that our choice ofP=200P=200queries per image for subsumption estimation strikes a good balance between profiling overhead and reliable layer selection\.

#### Artifact Availability\.

The artifact accompanying this paper, including theFastCertsource code, networks, and experimental scripts, is available on Zenodo \(DOI:[10\.5281/zenodo\.21314767](https://doi.org/10.5281/zenodo.21314767)\)\.

#### Acknowledgments\.

This research was supported in part by the National Science Foundation under grants CCF\-2238079, CCF\-2313028, CCF\-2223825, CCF\-2223826, a gift from Oracle Labs, and a Google Research Award\. The views expressed herein are those of the authors and do not necessarily reflect those of our funders\.

## References

- \[1\]A\. Albarghouthi\(2021\)Introduction to neural network verification\.External Links:2109\.10317,[Link](https://arxiv.org/abs/2109.10317)Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p2.1)\.
- \[2\]M\. Balunovic, M\. Baader, G\. Singh, T\. Gehr, and M\. Vechev\(2019\)Certifying geometric robustness of neural networks\.Advances in Neural Information Processing Systems32\.Cited by:[Appendix Appendix 1](https://arxiv.org/html/2608.19351#Pt0.A1.p1.1),[§2](https://arxiv.org/html/2608.19351#S2.p3.1),[§4\.2](https://arxiv.org/html/2608.19351#S4.SS2.p3.1)\.
- \[3\]D\. Beyer, S\. Löwe, E\. Novikov, A\. Stahlbauer, and P\. Wendler\(2013\)Precision reuse for efficient regression verification\.InProceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering,ESEC/FSE 2013,pp\. 389–399\.External Links:ISBN 9781450322379,[Document](https://dx.doi.org/10.1145/2491411.2491429)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p2.1)\.
- \[4\]E\. Botoeva, P\. Kouvaros, J\. Kronqvist, A\. Lomuscio, and R\. Misener\(2020\)Efficient verification of relu\-based neural networks via dependency analysis\.InProc\. of Advances in Artificial Intelligence \(AAAI\),Cited by:[§4\.1](https://arxiv.org/html/2608.19351#S4.SS1.p3.1)\.
- \[5\]N\. Carlini and D\. A\. Wagner\(2017\)Towards evaluating the robustness of neural networks\.InSymposium on Security and Privacy \(S&P\),Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p1.1)\.
- \[6\]P\. Chiang, R\. Ni, A\. Abdelkader, C\. Zhu, C\. Studer, and T\. Goldstein\(2020\)Certified defenses for adversarial patches\.InProc\. of International Conf\. on Learning Representations \(ICLR\),Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p3.1),[§2](https://arxiv.org/html/2608.19351#S2.p4.1),[§4\.2](https://arxiv.org/html/2608.19351#S4.SS2.p2.1)\.
- \[7\]P\. Cousot and R\. Cousot\(1977\)Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints\.InProc\. of Principles of Programming Languages \(POPL\),Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p5.1)\.
- \[8\]F\. Croce, M\. Andriushchenko, N\. D\. Singh, N\. Flammarion, and M\. Hein\(2022\)Sparse\-RS: A versatile framework for query\-efficient sparse black\-box adversarial attacks\.InThirty\-Sixth AAAI Conference on Artificial Intelligence, AAAI,Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p3.1)\.
- \[9\]K\. Eykholt, I\. Evtimov, E\. Fernandes, B\. Li, A\. Rahmati, C\. Xiao, A\. Prakash, T\. Kohno, and D\. Song\(2018\)Robust physical\-world attacks on deep learning visual classification\.InProceedings of the IEEE conference on computer vision and pattern recognition,pp\. 1625–1634\.Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p3.1)\.
- \[10\]M\. Fischer, C\. Sprecher, D\. I\. Dimitrov, G\. Singh, and M\. Vechev\(2022\)Shared certificates for neural network verification\.InComputer Aided Verification: 34th International Conference, CAV 2022,pp\. 127–148\.External Links:ISBN 978\-3\-031\-13184\-4,[Document](https://dx.doi.org/10.1007/978-3-031-13185-1%5F7)Cited by:[Appendix Appendix 1](https://arxiv.org/html/2608.19351#Pt0.A1.p1.1),[§1](https://arxiv.org/html/2608.19351#S1.p3.1),[§3\.1](https://arxiv.org/html/2608.19351#S3.SS1.p1.1),[§3\.1](https://arxiv.org/html/2608.19351#S3.SS1.p2.1),[§3\.2](https://arxiv.org/html/2608.19351#S3.SS2.p1.1),[§3\.2](https://arxiv.org/html/2608.19351#S3.SS2.p2.1),[§3\.3](https://arxiv.org/html/2608.19351#S3.SS3.p6.1),[§4\.2](https://arxiv.org/html/2608.19351#S4.SS2.p3.1),[§5](https://arxiv.org/html/2608.19351#S5.p2.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p5.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p6.1),[§6\.2](https://arxiv.org/html/2608.19351#S6.SS2.p1.1),[§7\.4](https://arxiv.org/html/2608.19351#S7.SS4.p1.1),[§8](https://arxiv.org/html/2608.19351#S8.p3.1),[§8](https://arxiv.org/html/2608.19351#S8.p4.1)\.
- \[11\]T\. Gehr, M\. Mirman, D\. Drachsler\-Cohen, P\. Tsankov, S\. Chaudhuri, and M\. Vechev\(2018\)Ai2: safety and robustness certification of neural networks with abstract interpretation\.In2018 IEEE Symposium on Security and Privacy \(SP\),pp\. 3–18\.Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[12\]I\. J\. Goodfellow, J\. Shlens, and C\. Szegedy\(2015\)Explaining and harnessing adversarial examples\.In3rd International Conference on Learning Representations, ICLR,Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p1.1),[§1](https://arxiv.org/html/2608.19351#S1.p3.1)\.
- \[13\]E\. Jiang, D\. S\. Cheung, and G\. Singh\(2026\)Towards generalized certified robustness with multi\-norm training\.Trans\. Mach\. Learn\. Res\.2026\.External Links:[Link](https://openreview.net/forum?id=U5U7pazr6X)Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p4.1),[§4\.2](https://arxiv.org/html/2608.19351#S4.SS2.p2.1)\.
- \[14\]K\. Johnson, R\. Calinescu, and S\. Kikuchi\(2013\)An incremental verification framework for component\-based software systems\.InProceedings of the ACM SIGSOFT Symposium on Component\-Based Software Engineering,CBSE ’13,pp\. 33–42\.External Links:ISBN 9781450321228,[Document](https://dx.doi.org/10.1145/2465449.2465456)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p2.1)\.
- \[15\]S\. Kotyan and D\. V\. Vargas\(2022\)Adversarial robustness assessment: why in evaluation bothL0L\_\{0\}andL∞L\_\{\\infty\}attacks are necessary\.PloS one17\(4\),pp\. e0265723\.Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p3.1)\.
- \[16\]Y\. Lakhnech, S\. Bensalem, S\. Berezin, and S\. Owre\(2001\)Incremental verification by abstraction\.InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems,pp\. 98–112\.Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p2.1)\.
- \[17\]L\. Li, T\. Xie, and B\. Li\(2023\)SoK: certified robustness for deep neural networks\.In44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, 22\-26 May 2023,Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p2.1)\.
- \[18\]A\. Madry, A\. Makelov, L\. Schmidt, D\. Tsipras, and A\. Vladu\(2018\)Towards deep learning models resistant to adversarial attacks\.InProc\. International Conference on Learning Representations \(ICLR\),Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p2.1),[§1](https://arxiv.org/html/2608.19351#S1.p3.1),[§2](https://arxiv.org/html/2608.19351#S2.p4.1),[§4\.2](https://arxiv.org/html/2608.19351#S4.SS2.p2.1)\.
- \[19\]Y\. Mao, M\. Müller, M\. Fischer, and M\. Vechev\(2023\)Connecting certified and adversarial training\.Advances in Neural Information Processing Systems36,pp\. 73422–73440\.Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p4.1),[§4\.2](https://arxiv.org/html/2608.19351#S4.SS2.p2.1)\.
- \[20\]M\. Mirman, T\. Gehr, and M\. Vechev\(2018\)Differentiable abstract interpretation for provably robust neural networks\.InProceedings of the 35th International Conference on Machine Learning,Proceedings of Machine Learning Research, Vol\.80,pp\. 3578–3586\.External Links:[Link](https://proceedings.mlr.press/v80/mirman18b.html)Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p2.1),[§2](https://arxiv.org/html/2608.19351#S2.p4.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p6.1)\.
- \[21\]A\. Modas, S\. Moosavi\-Dezfooli, and P\. Frossard\(2019\)Sparsefool: a few pixels make a big difference\.InProceedings of the IEEE Conference on Computer Vision and Pattern Recognition,pp\. 9087–9096\.Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p3.1)\.
- \[22\]M\. N\. Müller, F\. Eckert, M\. Fischer, and M\. Vechev\(2023\)Certified training: small boxes are all you need\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=7oFuxtJtUMH)Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p4.1),[§4\.2](https://arxiv.org/html/2608.19351#S4.SS2.p2.1)\.
- \[23\]P\. W\. O’Hearn\(2018\)Continuous reasoning: scaling the impact of formal methods\.InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018,A\. Dawar and E\. Grädel \(Eds\.\),External Links:[Link](https://doi.org/10.1145/3209108.3209109),[Document](https://dx.doi.org/10.1145/3209108.3209109)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p2.1)\.
- \[24\]H\. Salman, G\. Yang, H\. Zhang, C\. Hsieh, and P\. Zhang\(2019\)A convex relaxation barrier to tight robustness verification of neural networks\.Advances in Neural Information Processing Systems32\.Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[25\]T\. Serra, X\. Yu, A\. Kumar, and S\. Ramalingam\(2021\)Scaling up exact neural network compression by relu stability\.Advances in neural information processing systems34,pp\. 27081–27093\.Cited by:[§4\.1](https://arxiv.org/html/2608.19351#S4.SS1.p3.1)\.
- \[26\]Y\. Shapira, E\. Avneri, and D\. Drachsler\-Cohen\(2023\)Deep learning robustness verification for few\-pixel attacks\.Proc\. ACM Program\. Lang\.7\(OOPSLA1\)\.Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p3.1),[§5](https://arxiv.org/html/2608.19351#S5.p3.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p1.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p5.1),[§6\.2](https://arxiv.org/html/2608.19351#S6.SS2.p1.1),[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[27\]Y\. Shapira and D\. Drachsler\-Cohen\(2026\)Tight robustness certification through the convex hull ofℓ0\\ell\_\{0\}attacks\.Proceedings of the AAAI Conference on Artificial Intelligence40\(44\),pp\. 37913–37922\.External Links:[Document](https://dx.doi.org/10.1609/aaai.v40i44.41128)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[28\]Y\. Shapira, N\. Wiesel, S\. Shabelman, and D\. Drachsler\-Cohen\(2024\)Boosting few\-pixel robustness verification via covering verification designs\.InInternational Conference on Computer Aided Verification,pp\. 377–400\.Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p3.1),[§5](https://arxiv.org/html/2608.19351#S5.p3.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p1.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p5.1),[§6\.2](https://arxiv.org/html/2608.19351#S6.SS2.p1.1),[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[29\]G\. Singh, R\. Ganvir, M\. Püschel, and M\. Vechev\(2019\)Beyond the single neuron convex barrier for neural network certification\.Advances in Neural Information Processing Systems32\.Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[30\]G\. Singh, T\. Gehr, M\. Mirman, M\. Püschel, and M\. Vechev\(2018\)Fast and effective robustness certification\.Advances in Neural Information Processing Systems31,pp\. 10802–10813\.Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p2.1),[§2](https://arxiv.org/html/2608.19351#S2.p5.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p6.1),[§6\.2](https://arxiv.org/html/2608.19351#S6.SS2.p1.1),[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[31\]G\. Singh, T\. Gehr, M\. Püschel, and M\. Vechev\(2019\)An abstract domain for certifying neural networks\.Proceedings of the ACM on Programming Languages3\(POPL\),pp\. 1–30\.Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p2.1),[§2](https://arxiv.org/html/2608.19351#S2.p5.1),[§7\.4](https://arxiv.org/html/2608.19351#S7.SS4.p1.1),[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[32\]G\. Singh, J\. Laurel, S\. Misailovic, D\. Banerjee, A\. Singh, C\. Xu, S\. Ugare, and H\. Zhang\(2025\)Safety and trust in artificial intelligence with abstract interpretation\.Found\. Trends Program\. Lang\.8\(3–4\),pp\. 250–408\.External Links:ISSN 2325\-1107,[Link](https://doi.org/10.1561/2500000062),[Document](https://dx.doi.org/10.1561/2500000062)Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p5.1)\.
- \[33\]B\. Stein, B\. E\. Chang, and M\. Sridharan\(2021\)Demanded abstract interpretation\.InPLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20\-25, 2021,S\. N\. Freund and E\. Yahav \(Eds\.\),pp\. 282–295\.External Links:[Link](https://doi.org/10.1145/3453483.3454044),[Document](https://dx.doi.org/10.1145/3453483.3454044)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p2.1)\.
- \[34\]J\. Su, D\. V\. Vargas, and K\. Sakurai\(2019\)One pixel attack for fooling deep neural networks\.IEEE Trans\. Evol\. Comput\.23\(5\)\.Cited by:[§2](https://arxiv.org/html/2608.19351#S2.p3.1)\.
- \[35\]C\. Szegedy, W\. Zaremba, I\. Sutskever, J\. Bruna, D\. Erhan, I\. J\. Goodfellow, and R\. Fergus\(2014\)Intriguing properties of neural networks\.In2nd International Conference on Learning Representations, ICLR,Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p1.1),[§1](https://arxiv.org/html/2608.19351#S1.p3.1)\.
- \[36\]S\. Ugare, D\. Banerjee, S\. Misailovic, and G\. Singh\(2023\)Incremental verification of neural networks\.Proc\. ACM Program\. Lang\.7\(PLDI\)\.External Links:[Link](https://doi.org/10.1145/3591299),[Document](https://dx.doi.org/10.1145/3591299)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p3.1)\.
- \[37\]S\. Ugare, G\. Singh, and S\. Misailovic\(2022\)Proof transfer for fast certification of multiple approximate neural networks\.Proc\. ACM Program\. Lang\.6\(OOPSLA1\)\.External Links:[Link](https://doi.org/10.1145/3527319),[Document](https://dx.doi.org/10.1145/3527319)Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p3.1),[§3\.1](https://arxiv.org/html/2608.19351#S3.SS1.p1.1),[§3\.1](https://arxiv.org/html/2608.19351#S3.SS1.p2.1),[§3\.2](https://arxiv.org/html/2608.19351#S3.SS2.p1.1),[§3\.2](https://arxiv.org/html/2608.19351#S3.SS2.p2.1),[§3\.3](https://arxiv.org/html/2608.19351#S3.SS3.p6.1),[§4\.2](https://arxiv.org/html/2608.19351#S4.SS2.p6.1),[§5](https://arxiv.org/html/2608.19351#S5.p2.1),[§5](https://arxiv.org/html/2608.19351#S5.p3.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p5.1),[§6\.1](https://arxiv.org/html/2608.19351#S6.SS1.p6.1),[§7\.3](https://arxiv.org/html/2608.19351#S7.SS3.p3.1),[§8](https://arxiv.org/html/2608.19351#S8.p3.1),[§8](https://arxiv.org/html/2608.19351#S8.p4.1)\.
- \[38\]S\. Ugare, T\. Suresh, D\. Banerjee, G\. Singh, and S\. Misailovic\(2024\)Incremental randomized smoothing certification\.InThe Twelfth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=SdeAPV1irk)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p3.1)\.
- \[39\]W\. Visser, J\. Geldenhuys, and M\. B\. Dwyer\(2012\)Green: reducing, reusing and recycling constraints in program analysis\.InProceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering,FSE ’12\.External Links:ISBN 9781450316149,[Document](https://dx.doi.org/10.1145/2393596.2393665)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p2.1)\.
- \[40\]T\. Wei and C\. Liu\(2021\)Online verification of deep neural networks under domain or weight shift\.CoRRabs/2106\.12732\.External Links:2106\.12732Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p4.1)\.
- \[41\]E\. Wong and Z\. Kolter\(2018\)Provable defenses against adversarial examples via the convex outer adversarial polytope\.InInternational conference on machine learning,pp\. 5286–5295\.Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p2.1)\.
- \[42\]H\. Wu, O\. Isac, A\. Zeljić, T\. Tagomori, M\. Daggitt, W\. Kokke, I\. Refaeli, G\. Amir, K\. Julian, S\. Bassan,et al\.\(2024\)Marabou 2\.0: a versatile formal analyzer of neural networks\.InInternational Conference on Computer Aided Verification,pp\. 249–264\.Cited by:[§1](https://arxiv.org/html/2608.19351#S1.p2.1)\.
- \[43\]K\. Xu, Z\. Shi, H\. Zhang, Y\. Wang, K\. Chang, M\. Huang, B\. Kailkhura, X\. Lin, and C\. Hsieh\(2020\)Automatic perturbation analysis for scalable certified robustness and beyond\.Advances in Neural Information Processing Systems33,pp\. 1129–1141\.Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[44\]G\. Yang, M\. B\. Dwyer, and G\. Rothermel\(2009\)Regression model checking\.In2009 IEEE International Conference on Software Maintenance,Vol\.,pp\. 115–124\.External Links:[Document](https://dx.doi.org/10.1109/ICSM.2009.5306334)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p2.1)\.
- \[45\]R\. Yang, J\. Laurel, S\. Misailovic, and G\. Singh\(2023\)Provable defense against geometric transformations\.InThe Eleventh International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=ThXqBsRI-cY)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.
- \[46\]G\. Zhang, Z\. Zhang, H\.M\.N\. D\. Bandara, S\. Chen, J\. Zhao, and Y\. Sui\(2025\)Efficient incremental verification of neural networks guided by counterexample potentiality\.Proc\. ACM Program\. Lang\.9\(OOPSLA1\)\.External Links:[Document](https://dx.doi.org/10.1145/3720417)Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p3.1)\.
- \[47\]H\. Zhang, T\. Weng, P\. Chen, C\. Hsieh, and L\. Daniel\(2018\)Efficient neural network robustness certification with general activation functions\.InAdvances in neural information processing systems,Cited by:[§8](https://arxiv.org/html/2608.19351#S8.p1.1)\.