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.
Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
University of Oxford, Oxford, United Kingdom（牛津大学）；Radboud University, Nijmegen, the Netherlands（拉德博德大学）；Lund University, Lund, Sweden（隆德大学）；University of Copenhagen, Copenhagen, Denmark（哥本哈根大学）；Ruhr-University Bochum, Bochum, Germany（波鸿鲁尔大学）
Safe Reach Set Computation via Neural Barrier Certificates
University of Oxford（牛津大学）；Newcastle University（纽卡斯尔大学）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；Università di Roma “La Sapienza”（罗马第一大学）
