Uncovering the Limits of Proof Sharing for Neural Networks

Kanak Das; Shubham Ugare; Bor-Yuh Evan Chang; Sasa Misailovic; Gagandeep Singh; Manu Sridharan

cs.LGAug 19, 2026

Uncovering the Limits of Proof Sharing for Neural Networks

Authors: Kanak Das, Shubham Ugare, Bor-Yuh Evan Chang, Sasa Misailovic, Gagandeep Singh, Manu Sridharan

Organizations: University of California, Riverside · University of Illinois Urbana-Champaign · University of Colorado Boulder & Amazon

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 present FastCert, 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 based $L_0$ -verification tasks, FastCert achieved an average speedup of 1.13x over an extant template-based reuse technique.

Figures & tables

Figure 1: Template reuse in a 4-layer network. From an input image

x

, we first verify an initial query under

\mathcal{I}_{\infty}(x)

, then build a layer-

k{=}2

template 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

\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.

Panel of Figure 2 — Figure 2: Jointly stable neurons and template subsumption rates under random- $L_{0}$ perturbations in MNIST networks.

Panel of Figure 3 — Figure 3: Jointly stable neurons and template subsumption rates under random- $L_{0}$ perturbations in CIFAR-10 networks.

Figure 4: Sampling size vs. subsumption rate estimates for MNIST PGD with 4 templates.

Dataset	Model	Architecture	#Neurons
MNIST, CIFAR-10	CPDMed	7 $\times$ 200 linear layers	1400
	CPDBig	9 $\times$ 500 linear layers	4500
	CURE	9 $\times$ 500 linear layers	4500
	PGD	6 $\times$ 500 linear layers	3000
	Standard	6 $\times$ 500 linear layers	3000
	CPDConv	4 Conv layers, 4 linear layers	8448

Table 1: Networks used in the FastCert evaluation.

	DeepZ						Box
Net	V	T	Sub		Spd		V	T	Sub		Spd
	(%)	(s)	E	F	E	F	(%)	(s)	E	F	E	F
CPDMed	92.4	5293	57.8	85.2	1.28	1.41	94.6	4310	28.7	92.0	1.02	1.40
CPDBig	88.4	6309	87.0	98.6	1.91	2.10	92.8	4966	62.9	98.7	1.39	2.00
CPDConv	84.5	4781	68.4	72.0	1.08	1.06	84.5	8752	52.6	68.4	0.99	1.00
CURE	44.5	4704	43.7	85.3	1.12	1.24	31.5	2890	33.0	82.9	1.03	1.10

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 .

	DeepZ						Box
Net	V	T	Sub		Spd		V	T	Sub		Spd
	(%)	(s)	E	F	E	F	(%)	(s)	E	F	E	F
CPDMed	89.9	4768	59.7	85.8	1.24	1.35	91.7	3850	32.2	91.2	1.07	1.45
CPDBig	87.5	5842	89.2	98.7	1.88	2.04	90.8	4916	60.1	98.8	1.33	2.00
CPDConv	84.9	4530	69.3	72.3	1.02	1.02	84.3	8602	53.7	70.1	1.04	1.05
CURE	43.3	4321	53.4	89.8	1.12	1.24	30.3	2925	41.8	78.8	1.08	1.14

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 .

Figure 5: Combined speedup results across all 48 configurations: FastCert outperforms 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=4

p=3.1\times 10^{-9}

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 6 — Figure 6: Jointly stable neurons and template subsumption rates under $2\times 2$ patch perturbations in MNIST networks.

Panel of Figure 7 — Figure 7: Jointly stable neurons and template subsumption rates under $2\times 2$ patch perturbations in CIFAR-10 networks.

Panel of Figure 8 — Figure 8: Jointly stable neurons and template subsumption rates under geometric perturbations (4 splits) in MNIST networks.

Panel of Figure 9 — Figure 9: Jointly stable neurons and template subsumption rates under geometric perturbations (6 splits) in MNIST networks.

Panel of Figure 10 — Figure 10: Jointly stable neurons and template subsumption rates under geometric perturbations (8 splits) in MNIST networks.

Panel of Figure 11 — Figure 11: Jointly stable neurons and template subsumption rates under geometric perturbations (10 splits) in MNIST networks.

Panel of Figure 12 — Figure 12: Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 1 template.

Panel of Figure 13 — Figure 13: Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 2 templates.

Panel of Figure 14 — Figure 14: Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 4 templates.

Abstract Interpretation

See all 8 papers

Exploring Solver-Level Warmstarting for Neural Network Verification
Sep 22, 2026Annelot Bosman, Minghao Liu, Marta Kwiatkowska +2Neural Network Verification
Leiden Institute of Advanced Computer Science, Leiden · University of Oxford, United Kingdom · Chair for AI Methodology, RWTH Aachen University, Germany +1
Incremental Neural Network Verification via Learned Conflicts
Mar 12, 2026Raya Elsaleh, Liam Davis, Haoze Wu +1Neural Network Verification Neural Network Robustness
Hebrew University of Jerusalem, Jerusalem, Israel · Amherst College, Amherst, USA
Training Witnesses: Trusting the Training without Trusting the Trainer
Sep 27, 2026Houjun Liu, Pratyusha SharmaLLM Auditing ML Reproducibility
Microsoft Research

Sep 22, 2026J/K move · Enter open · S save

Exploring Solver-Level Warmstarting for Neural Network Verification

Annelot Bosman, Minghao Liu, Marta Kwiatkowska, Holger Hoos+1

Leiden Institute of Advanced Computer Science, Leiden · University of Oxford, United Kingdom · Chair for AI Methodology, RWTH Aachen University, Germany+1

Neural Network Verification

Open paper AskPDF arXiv

Neural network verification has become a key tool for providing formal guarantees on the behaviour of neural networks. However, many verification problems remain computationally intractable in the worst case: even for common adversarial robustness specifications, verification is NP-complete. Here, we explore the application of solver-level warmstarting for neural network verification to exploit information from previous solutions. We study the effect on running time as several properties are modified, including perturbation radii, input data and the networks themselves, using a pipeline that is generalisable and potentially adaptable to state-of-the-art verifiers. Our results show that warmstarting can significantly reduce verification time in most cases. Moreover, warmstarting enables the successful verification of instances that could not be solved from scratch within the given time limit.

Abstract

Abstract Interpretation

Explore similar work

Exploring Solver-Level Warmstarting for Neural Network Verification

Incremental Neural Network Verification via Learned Conflicts

Training Witnesses: Trusting the Training without Trusting the Trainer