Revisiting Differential Verification: Equivalence Verification with Confidence
When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning on differences between NNs: On the one hand, our paper proposes a novel abstract domain for differential verification admitting more efficient reasoning about equivalence. On the other hand, we investigate empirically and theoretically which equivalence properties are (not) efficiently solved using differential reasoning. Based on the gained insights, and following a recent line of work on confidence-based verification, we propose a novel equivalence property that is amenable to Differential Verification while providing guarantees for large parts of the input space instead of small-scale guarantees constructed w.r.t. predetermined input points. We implement our approach in a new tool called VeryDiff and perform an extensive evaluation on numerous old and new benchmark families, including new pruned NNs for particle jet classification in the context of CERN's LHC where we observe median speedups >300x over the State-of-the-Art verifier alpha,beta-CROWN.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
NeuroDiff: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation
As neural networks make their way into safety-critical systems, where misbehavior can lead to catastrophes, there is a growing interest in certifying the equivalence of two structurally similar neural networks. For examp…
DiffRNN: Differential Verification of Recurrent Neural Networks
Recurrent neural networks (RNNs) such as Long Short Term Memory (LSTM) networks have become popular in a variety of applications such as image processing, data classification, speech recognition, and as controllers in au…
speech-recognitionSpeech RecognitionPAC Learning-Based Verification and Model Synthesis
We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning a regular model of the set of feasible paths in a program, and testing whether this model con…
modelPAC learningGeometric Path Enumeration for Equivalence Verification of Neural Networks
As neural networks (NNs) are increasingly introduced into safety-critical domains, there is a growing need to formally verify NNs before deployment. In this work we focus on the formal verification problem of NN equivale…
Physics-Aware Neural Dynamic Equivalence of Power Systems
This letter devises Neural Dynamic Equivalence (NeuDyE), which explores physics-aware machine learning and neural-ordinary-differential-equations (ODE-Net) to discover a dynamic equivalence of external power grids while …