Harnessing Neuron Stability to Improve DNN Verification

TL;DR

This work tackles the scalability challenge in DNN verification by extending the NeuralSAT DPLL(T) framework with state-sensitive neuron stability, parallel search, and restart strategies. VeriStable computes which neurons are effectively linear under a given partial activation pattern and fixes their status to reduce branching; it also performs parallel exploration of activation-pattern branches and restarts to escape stagnation, yielding substantial performance gains. Empirical results show VeriStable achieving up to a 12x improvement over NeuralSAT and attaining state-of-the-art performance on multiple benchmark families, including ACAS Xu, MNISTFC, CIFAR2020, and ResNet-style networks, as measured by VNN-COMP scores. The work advances practical DNN verification by delivering an open-source tool, scalable techniques, and robust evaluation on diverse architectures, which can impact safety-critical deployments and verification-driven debugging and training.

Abstract

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 $α$-$β$-CROWN and MN-BaB, the first and second performers of the VNN-COMP, respectively.

Figures (9)

• Figure 1: The tree of activation patterns computed by NeuralSAT (left) and VeriStable (right) at corresponding points during a verification run.
• Figure 2: An FNN with ReLU.
• Figure 3: NeuralSAT Architecture
• Figure 4: VeriStable Architecture
• Figure 5: Performance of VeriStable with different optimization settings in comparison to NeuralSAT on the MNIST_GDVB benchmark with 900 second timeout, where: "N" is the base case (NeuralSAT), "P" enables Parallelism, "R" enables Restarts, and "S" enables Stabilization.