Harnessing Neuron Stability to Improve DNN Verification
Hai Duong Dong Xu ThanhVu Nguyen Matthew B. Dwyer
Deep Neural Networks (DNN) have emerged as an effective approach to tackling
real-world problems. However, like human-written software, DNNs are susceptible
to bugs and attacks. This has generated significant interests in developing
effective and scalable DNN verification techniques and tools. In this paper, we
present VeriStable, a novel extension of recently proposed DPLL-based
constraint DNN verification approach. VeriStable leverages the insight that
while neuron behavior may be non-linear across the entire DNN input space, at
intermediate states computed during verification many neurons may be
constrained to have linear behavior - these neurons are stable. Efficiently
detecting stable neurons reduces combinatorial complexity without compromising
the precision of abstractions. Moreover, the structure of clauses arising in
DNN verification problems shares important characteristics with industrial SAT
benchmarks. We adapt and incorporate multi-threading and restart optimizations
targeting those characteristics to further optimize DPLL-based DNN
verification. We evaluate the effectiveness of VeriStable across a range of
challenging benchmarks including fully-connected feedforward networks (FNNs),
convolutional neural networks (CNNs) and residual networks (ResNets) applied to
the standard MNIST and CIFAR datasets. Preliminary results show that VeriStable
is competitive and outperforms state-of-the-art DNN verification tools,
including $\alpha$-$\beta$-CROWN and MN-BaB, the first and second performers of
the VNN-COMP, respectively.