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 L0-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 I∞(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 I0(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.
Figure 2: Jointly stable neurons and template subsumption rates under random- L0 perturbations in MNIST networks.
Figure 3: Jointly stable neurons and template subsumption rates under random- L0 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 × 200 linear layers
1400
CPDBig
9 × 500 linear layers
4500
CURE
9 × 500 linear layers
4500
PGD
6 × 500 linear layers
3000
Standard
6 × 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×10−9 ).
Appendix figures & tables9 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 6: Jointly stable neurons and template subsumption rates under 2×2 patch perturbations in MNIST networks.
Figure 7: Jointly stable neurons and template subsumption rates under 2×2 patch perturbations in CIFAR-10 networks.
Figure 8: Jointly stable neurons and template subsumption rates under geometric perturbations (4 splits) in MNIST networks.
Figure 9: Jointly stable neurons and template subsumption rates under geometric perturbations (6 splits) in MNIST networks.
Figure 10: Jointly stable neurons and template subsumption rates under geometric perturbations (8 splits) in MNIST networks.
Figure 11: Jointly stable neurons and template subsumption rates under geometric perturbations (10 splits) in MNIST networks.
Figure 12: Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 1 template.
Figure 13: Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 2 templates.
Figure 14: Comparing predicted minimum subsumption thresholds with observed subsumption rates across different sampling sizes with 4 templates.
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.
Annelot Bosman, Minghao Liu, Marta Kwiatkowska +2
Leiden Institute of Advanced Computer Science, Leiden · University of Oxford, United Kingdom · Chair for AI Methodology, RWTH Aachen University, Germany +1
Neural network verification is often used as a core component within larger analysis procedures, which generate sequences of closely related verification queries over the same network. In existing neural network verifiers, each query is typically solved independently, and information learned during previous runs is discarded, leading to repeated exploration of the same infeasible regions of the search space. In this work, we aim to expedite verification by reducing this redundancy. We propose an incremental verification technique that reuses learned conflicts across related verification queries. The technique can be added on top of any branch-and-bound-based neural network verifier. During verification, the verifier records conflicts corresponding to learned infeasible combinations of activation phases, and retains them across runs. We formalize a refinement relation between verification queries and show that conflicts learned for a query remain valid under refinement, enabling sound conflict inheritance. Inherited conflicts are handled using a SAT solver to perform consistency checks and propagation, allowing infeasible subproblems to be detected and pruned early during search. We implement the proposed technique in the Marabou verifier and evaluate it on three verification tasks: local robustness radius determination, verification with input splitting, and minimal sufficient feature set extraction. Our experiments show that incremental conflict reuse reduces verification effort and yields speedups of up to 1.9× over a non-incremental baseline.
Raya Elsaleh, Liam Davis, Haoze Wu +1
Hebrew University of Jerusalem, Jerusalem, Israel · Amherst College, Amherst, USA
Progress in machine learning cannot outpace our ability to verify it. With an explosion in papers today, every scientific claim rests initially on trust in the trainer, leading to uneven evaluation, baselines, and forestalling of reliable progress. Traditionally, the burden of verification falls on the reader, who must reproduce expensive training runs. This strategy is impractical due to an explosion in slop contributions, diversity of methods, and the sheer compute required. We put the burden of proof where it belongs, on the trainer, and in the process also cut the overall cost of verification significantly. We introduce Witnesses, a method for certifying training, data usage and evaluation in a neural network training run. Our key insight is that fast behavioral fingerprints with occasional replay challenges are sufficient for auditing neural network training. Our method is applicable at scale with minimal overhead to the trainer, is cheap for the verifier, rejects bad training runs with amplifiable probability, and allows for exact queries of both data inclusion and exclusion. We test our method on language model training runs from 100M to 2B scales, across DDP and FSDP, and demonstrate this minimal overhead. We also introduce a self-regulating leaderboard of "auto-certified" training runs that enables shared baselines and progress. We invite the community to participate in the leaderboard to improve reproducibility in machine learning.