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.
Recent developments in DNN verification have highlighted the potential of constraint-solving approaches
that combine abstraction techniques with SAT solving. Abstraction approaches are effective at precisely
encode neuron behavior when it is linear, but they lead to overapproximation and combinatorial scaling when
behavior is non-linear. SAT approaches in DNN verification have incorporated standard DPLL techniques, but
have overlooked important optimizations found in modern SAT solvers that help them scale on industrial
benchmarks.
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.
more »
« less
This content will become publicly available on July 12, 2025
Harnessing Neuron Stability to Improve DNN Verification
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 interest in developing effective and scalable DNN verification techniques and tools. Recent developments in DNN verification have highlighted the potential of constraint-solving approaches that combine abstraction techniques with SAT solving. Abstraction approaches are effective at precisely encoding neuron behavior when it is linear, but they lead to overapproximation and combinatorial scaling when behavior is non-linear. SAT approaches in DNN verification have incorporated standard DPLL techniques, but have overlooked important optimizations found in modern SAT solvers that help them scale on industrial benchmarks. In this paper, we present VeriStable, a novel extension of the 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.
more » « less- Award ID(s):
- 2129824
- PAR ID:
- 10530883
- Publisher / Repository:
- ACM
- Date Published:
- Journal Name:
- Proceedings of the ACM on Software Engineering
- Volume:
- 1
- Issue:
- FSE
- ISSN:
- 2994-970X
- Page Range / eLocation ID:
- 859 to 881
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Finkbeiner, Bernd ; Kovacs, Laura (Ed.)With the growing use of deep neural networks(DNN) in mis- sion and safety-critical applications, there is an increasing interest in DNN verification. Unfortunately, increasingly complex network struc- tures, non-linear behavior, and high-dimensional input spaces combine to make DNN verification computationally challenging. Despite tremen- dous advances, DNN verifiers are still challenged to scale to large ver- ification problems. In this work, we explore how the number of stable neurons under the precondition of a specification gives rise to verifica- tion complexity. We examine prior work on the problem, adapt it, and develop several novel approaches to increase stability. We demonstrate that neuron stability can be increased substantially without compromis- ing model accuracy and this yields a multi-fold improvement in DNN verifier performance.more » « less
-
Deep learning techniques have been widely adopted in daily life with applications ranging from face recognition to recommender systems. The substantial overhead of conventional error tolerance techniques precludes their widespread use, while approaches involving median filtering and invariant generation rely on alterations to DNN training that may be difficult to achieve for larger networks on larger datasets. To address this issue, this paper presents a novel approach taking advantage of the statistics of neuron output gradients to identify and suppress erroneous neuron values. By using the statistics of neurons’ gradients with respect to their neighbors, tighter statistical thresholds are obtained compared to the use of neuron output values alone. This approach is modular and is combined with accurate, low-overhead error detection methods to ensure it is used only when needed, further reducing its cost. Deep learning models can be trained using standard methods and our error correction module is fit to a trained DNN, achieving comparable or superior performance compared to baseline error correction methods while incurring comparable hardware overhead without needing to modify DNN training or utilize specialized hardware architectures.more » « less
-
Deep learning techniques have been widely adopted in daily life with applications ranging from face recognition to recommender systems. The substantial overhead of conventional error tolerance techniques precludes their widespread use, while approaches involving median filtering and invariant generation rely on alterations to DNN training that may be difficult to achieve for larger networks on larger datasets. To address this issue, this paper presents a novel approach taking advantage of the statistics of neuron output gradients to identify and suppress erroneous neuron values. By using the statistics of neurons’ gradients with respect to their neighbors, tighter statistical thresholds are obtained compared to the use of neuron output values alone. This approach is modular and is combined with accurate, low-overhead error detection methods to ensure it is used only when needed, further reducing its cost. Deep learning models can be trained using standard methods and our error correction module is fit to a trained DNN, achieving comparable or superior performance compared to baseline error correction methods while incurring comparable hardware overhead without needing to modify DNN training or utilize specialized hardware architectures.more » « less
-
Silva, Alexandra ; Leino, K. Rustan (Ed.)Neural Networks (NNs) have increasingly apparent safety implications commensurate with their proliferation in real-world applications: both unanticipated as well as adversarial misclassifications can result in fatal outcomes. As a consequence, techniques of formal verification have been recognized as crucial to the design and deployment of safe NNs. In this paper, we introduce a new approach to formally verify the most commonly considered safety specifications for ReLU NNs -- i.e. polytopic specifications on the input and output of the network. Like some other approaches, ours uses a relaxed convex program to mitigate the combinatorial complexity of the problem. However, unique in our approach is the way we use a convex solver not only as a linear feasibility checker, but also as a means of penalizing the amount of relaxation allowed in solutions. In particular, we encode each ReLU by means of the usual linear constraints, and combine this with a convex objective function that penalizes the discrepancy between the output of each neuron and its relaxation. This convex function is further structured to force the largest relaxations to appear closest to the input layer; this provides the further benefit that the most ``problematic'' neurons are conditioned as early as possible, when conditioning layer by layer. This paradigm can be leveraged to create a verification algorithm that is not only faster in general than competing approaches, but is also able to verify considerably more safety properties; we evaluated PEREGRiNN on a standard MNIST robustness verification suite to substantiate these claims.more » « less
