Reference
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 verification tasks, FastCert achieved an average speedup of 1.3x compared to an extant template-based reuse technique.
BibTeX
@string{SAS = "International Static Analysis Symposium (SAS)"}
@inproceedings{limits-of-proof-sharing-sas26,
author = {Kanak Das and Shubham Ugare and Bor-Yuh Evan Chang and Sasa Misailovic and Gagandeep Singh and Manu Sridharan},
title = {Uncovering the Limits of Proof Sharing for Neural Networks},
booktitle = SAS,
year = {2026},
pages = {35 pages},
}