TY - GEN
T1 - Shared Certificates for Neural Network Verification
AU - Fischer, Marc
AU - Sprecher, Christian
AU - Dimitrov, Dimitar Iliev
AU - Singh, Gagandeep
AU - Vechev, Martin
N1 - Publisher Copyright:
© 2022, The Author(s).
PY - 2022
Y1 - 2022
N2 - Existing neural network verifiers compute a proof that each input is handled correctly under a given perturbation by propagating a symbolic abstraction of reachable values at each layer. This process is repeated from scratch independently for each input (e.g., image) and perturbation (e.g., rotation), leading to an expensive overall proof effort when handling an entire dataset. In this work, we introduce a new method for reducing this verification cost without losing precision based on a key insight that abstractions obtained at intermediate layers for different inputs and perturbations can overlap or contain each other. Leveraging our insight, we introduce the general concept of shared certificates, enabling proof effort reuse across multiple inputs to reduce overall verification costs. We perform an extensive experimental evaluation to demonstrate the effectiveness of shared certificates in reducing the verification cost on a range of datasets and attack specifications on image classifiers including the popular patch and geometric perturbations. We release our implementation at https://github.com/eth-sri/proof-sharing.
AB - Existing neural network verifiers compute a proof that each input is handled correctly under a given perturbation by propagating a symbolic abstraction of reachable values at each layer. This process is repeated from scratch independently for each input (e.g., image) and perturbation (e.g., rotation), leading to an expensive overall proof effort when handling an entire dataset. In this work, we introduce a new method for reducing this verification cost without losing precision based on a key insight that abstractions obtained at intermediate layers for different inputs and perturbations can overlap or contain each other. Leveraging our insight, we introduce the general concept of shared certificates, enabling proof effort reuse across multiple inputs to reduce overall verification costs. We perform an extensive experimental evaluation to demonstrate the effectiveness of shared certificates in reducing the verification cost on a range of datasets and attack specifications on image classifiers including the popular patch and geometric perturbations. We release our implementation at https://github.com/eth-sri/proof-sharing.
KW - Adversarial Robustness
KW - Local Verification
KW - Neural Network Verification
UR - http://www.scopus.com/inward/record.url?scp=85135800874&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85135800874&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-13185-1_7
DO - 10.1007/978-3-031-13185-1_7
M3 - Conference contribution
AN - SCOPUS:85135800874
SN - 9783031131844
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 127
EP - 148
BT - Computer Aided Verification - 34th International Conference, CAV 2022, Proceedings
A2 - Shoham, Sharon
A2 - Vizel, Yakir
PB - Springer
T2 - 34th International Conference on Computer Aided Verification, CAV 2022
Y2 - 7 August 2022 through 10 August 2022
ER -