Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A DPLL(T) Framework for Verifying Deep Neural Networks

Hai Duong, ThanhVu Nguyen, Matthew Dwyer

TL;DR

NeuralSAT presents an SMT-inspired verifier for deep neural networks by adapting the DPLL(T) framework with conflict-driven clause learning and search restarts to tackle the combinatorial complexity of ReLU networks. It uses a Boolean abstraction of neuron activations together with a domain-specific theory solver based on linear real arithmetic and LiRPA-style bounds, enabling aggressive theory propagation and clause learning. Empirical results on standard benchmarks show that NeuralSAT is competitive with state-of-the-art verifiers, offering notable gains from CDCL and restarts, particularly on large networks; it remains open-source and extensible. The work demonstrates the practical viability of integrating CDCL-based SMT techniques into DNN verification, with implications for scalability, proof generation, and potential for further optimizations and debugging capabilities.

Abstract

Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, like human-written software, DNNs can have bugs and can be attacked. To address this, research has explored a wide-range of algorithmic approaches to verify DNN behavior. In this work, we introduce NeuralSAT, a new verification approach that adapts the widely-used DPLL(T) algorithm used in modern SMT solvers. A key feature of SMT solvers is the use of conflict clause learning and search restart to scale verification. Unlike prior DNN verification approaches, NeuralSAT combines an abstraction-based deductive theory solver with clause learning and an evaluation clearly demonstrates the benefits of the approach on a set of challenging verification benchmarks.

A DPLL(T) Framework for Verifying Deep Neural Networks

TL;DR

NeuralSAT presents an SMT-inspired verifier for deep neural networks by adapting the DPLL(T) framework with conflict-driven clause learning and search restarts to tackle the combinatorial complexity of ReLU networks. It uses a Boolean abstraction of neuron activations together with a domain-specific theory solver based on linear real arithmetic and LiRPA-style bounds, enabling aggressive theory propagation and clause learning. Empirical results on standard benchmarks show that NeuralSAT is competitive with state-of-the-art verifiers, offering notable gains from CDCL and restarts, particularly on large networks; it remains open-source and extensible. The work demonstrates the practical viability of integrating CDCL-based SMT techniques into DNN verification, with implications for scalability, proof generation, and potential for further optimizations and debugging capabilities.

Abstract

Deep Neural Networks (DNNs) have emerged as an effective approach to tackling real-world problems. However, like human-written software, DNNs can have bugs and can be attacked. To address this, research has explored a wide-range of algorithmic approaches to verify DNN behavior. In this work, we introduce NeuralSAT, a new verification approach that adapts the widely-used DPLL(T) algorithm used in modern SMT solvers. A key feature of SMT solvers is the use of conflict clause learning and search restart to scale verification. Unlike prior DNN verification approaches, NeuralSAT combines an abstraction-based deductive theory solver with clause learning and an evaluation clearly demonstrates the benefits of the approach on a set of challenging verification benchmarks.
Paper Structure (53 sections, 4 theorems, 6 equations, 19 figures, 4 tables, 3 algorithms)

This paper contains 53 sections, 4 theorems, 6 equations, 19 figures, 4 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Satisfiability and DPLL(T)
  4. DPLL
  5. DPLL(T)
  6. The DNN verification problem
  7. DNN Verification
  8. Example
  9. Abstraction
  10. Overview of NeuralSAT
  11. Illustration
  12. Boolean Abstraction
  13. DPLL(T) Iterations
  14. The search tree of NeuralSAT
  15. The NeuralSAT Approach
  16. ...and 38 more sections

Key Result

Lemma A.1

If $\emptyset \parallel F \Longrightarrow^* M \parallel G$, then the following hold:

Figures (19)

  • Figure 1: Original DPLL Algorithm.
  • Figure 2: An FNN with ReLU.
  • Figure 3: NeuralSAT.
  • Figure 4: Search tree explored by NeuralSAT (a) and other verifiers (b) during a verification run. The notation $\{...\}$ indicates learned clauses; red is infeasibility; white is feasibility; yellow is BCP application; and blue is current consideration. The search tree of NeuralSAT is smaller than the tree of the other techniques because NeuralSAT was able to prune various branches, e.g., through BCPs (e.g., ${v_3}$ and $\overline{v_5}$) and non-chronological backtracks (e.g., $\overline{v_3}$).
  • Figure 6: Abstractions for ReLU: (a) interval, (b) zonotope, and (c-d) polytopes. Notice that ReLU is a non-convex region (red line) while all abstractions are convex regions. Note that (c) and (d) are both polytopes.
  • ...and 14 more figures

Theorems & Definitions (4)

  • Lemma A.1
  • Lemma A.2
  • Theorem A.3: Termination
  • Theorem A.4