SMT and MILP Solvers for Verification

January 2026 NNV Guide 14 min read 2,791 words

Zhongkui Ma This guide is based on SoK: Certified Robustness for Deep Neural Networks and Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective. It covers complete verification using SMT and MILP solvers, including encoding theory and QCQP/SDP formulations.

Verification Methods SMT MILP

When you need absolute certainty—definitive answers, no “unknown” results—you need complete verification. SMT (Satisfiability Modulo Theories) and MILP (Mixed-Integer Linear Programming) solvers provide exactly this: they always return either “verified” or a counterexample. These are the workhorses of complete neural network verification, encoding the verification problem as logical constraints or optimization problems that mature solvers can handle.

This guide explores how SMT and MILP solvers work for neural network verification, when to use them, and why they provide the strongest guarantees despite computational costs.

Why Complete Verification Matters

Incomplete methods (bound propagation, abstract interpretation) are fast but sometimes return “unknown.” For safety-critical applications—aviation, medical devices, autonomous vehicles—“unknown” isn’t acceptable. You need definitive answers: either the property holds, or here’s a counterexample proving it doesn’t.

Complete verification guarantees exactly this: given enough time and memory, SMT and MILP solvers will find the answer. The tradeoff is computational cost—these methods have exponential worst-case complexity [Katz et al., 2017, Weng et al., 2018]. But when absolute certainty matters more than speed, complete verification is the right tool.

Complete Verification Guarantee

A complete verification method always returns one of two answers:

• VERIFIED: The property provably holds for all inputs in the specified region

• FALSIFIED: A counterexample exists (and is provided)

Unlike incomplete methods, complete verifiers never return “unknown.” Given sufficient computational resources, they always reach a definitive answer.

SMT-Based Verification

SMT solvers determine satisfiability of logical formulas involving theories beyond pure propositional logic. For neural networks, the relevant theory is linear real arithmetic combined with Boolean logic for modeling ReLU activations.

Encoding Neural Networks as SMT Formulas

A neural network can be encoded as a conjunction of constraints [Katz et al., 2017]:

Linear layers: For weight matrix \(W\), bias \(b\), and layer computation \(z = Wx + b\):

\[z_i = \sum_j W_{ij} x_j + b_i \quad \forall i\]

This is a linear equality constraint, directly expressible in SMT.

ReLU activations: For \(y = \text{ReLU}(z)\), we need to capture the piecewise behavior:

\[\begin{split}y = \begin{cases} z & \text{if } z \geq 0 \\ 0 & \text{if } z < 0 \end{cases}\end{split}\]

This is encoded as a disjunction:

\[(z \geq 0 \land y = z) \lor (z < 0 \land y = 0)\]

Input constraints: For \(\ell_\infty\) perturbation ball with radius \(\epsilon\):

\[x_0 - \epsilon \leq x \leq x_0 + \epsilon\]

Output property: For robustness, require the true class \(y_0\) to score highest:

\[f(x)_{y_0} > f(x)_c \quad \forall c \neq y_0\]

Complete encoding: Combine all constraints:

\[\bigwedge_{\text{layers}} \text{(linear constraints)} \land \bigwedge_{\text{ReLUs}} \text{(ReLU disjunctions)} \land \text{(input constraints)} \land \neg\text{(output property)}\]

The SMT solver searches for a satisfying assignment. If one exists, it’s a counterexample. If none exists (unsatisfiable), the property is verified.

SMT Encoding Strategy

Verification reduces to checking: Is there an input in the allowed region where the property fails?

This is a satisfiability problem: find \(x\) satisfying input constraints and violating the property. If no such \(x\) exists (unsatisfiable), the property holds.

Encoding Theory: Why Complete Verification is Exponential

Understanding why complete verification has exponential complexity requires analyzing the formal encoding structure. The fundamental issue is that ReLU networks partition input space into exponentially many linear regions.

Formal SAT/LP Encoding Definition:

For a ReLU network with \(n\) neurons, the complete encoding requires representing all possible activation patterns—assignments of active/inactive states to each ReLU.

Definition (Activation Pattern): For a network with ReLU neurons \(r_1, \ldots, r_n\), an activation pattern \(\sigma \in \{0,1\}^n\) assigns:

\[\begin{split}\sigma_i = \begin{cases} 1 & \text{if ReLU } r_i \text{ is active} \\ 0 & \text{if ReLU } r_i \text{ is inactive} \end{cases}\end{split}\]

Each pattern \(\sigma\) defines a linear region where the network function is piecewise linear.

Theorem (Exponential Number of Activation Patterns): For a ReLU network with \(n\) neurons, there are at most \(2^n\) distinct activation patterns.

Proof:

Each of \(n\) ReLU neurons can be in one of 2 states (active or inactive). By the multiplication principle, there are \(2 \times 2 \times \cdots \times 2 = 2^n\) possible combinations. □

Why 2^n CNF Formulas:

SAT/LP complete encoding must enumerate all activation patterns to find the global optimum (or prove unsatisfiability).

Encoding structure:

For each activation pattern \(\sigma \in \{0,1\}^n\):

\[\Phi_\sigma = \bigwedge_{i=1}^n \left[ \sigma_i = 1 \Rightarrow (y_i = x_i \land x_i \geq 0) \right] \land \left[ \sigma_i = 0 \Rightarrow (y_i = 0 \land x_i < 0) \right]\]

The complete formula is the disjunction over all patterns:

\[\Phi_{\text{complete}} = \bigvee_{\sigma \in \{0,1\}^n} \Phi_\sigma\]

Converting to CNF (Conjunctive Normal Form) for SAT solving yields \(O(2^n)\) clauses in the worst case.

Consequence: SAT/SMT solvers must explore (in the worst case) all \(2^n\) activation patterns to verify a property or find a counterexample. This is the source of exponential complexity.

Connection to Operation Decomposition:

ReLU neurons are unary operations that introduce non-linearity (see Neural Network Decomposition: The Unary-Binary Framework). Each ReLU creates a binary choice (active/inactive), leading to \(2^n\) regions. The binary operations (affine layers) are exact and don’t contribute to exponential complexity—only the unary ReLU operations do.

MILP Big-M Encoding Theory:

MILP avoids explicit enumeration of \(2^n\) patterns by using binary integer variables and big-M constraints.

Encoding: For ReLU neuron \(i\) with pre-activation \(x_i\) and post-activation \(y_i\), introduce binary variable \(\delta_i \in \{0,1\}\):

\[\begin{split}\begin{aligned} y_i &\geq 0 \\ y_i &\geq x_i \\ y_i &\leq x_i - l_i(1 - \delta_i) \\ y_i &\leq u_i \delta_i \end{aligned}\end{split}\]

where \([l_i, u_i]\) are bounds on \(x_i\) (from incomplete methods).

When \(\delta_i = 1\) (active):

\[\begin{split}\begin{aligned} y_i &\geq x_i \\ y_i &\leq x_i - l_i \cdot 0 = x_i \\ y_i &\leq u_i \end{aligned}\end{split}\]

Since \(x_i \in [l_i, u_i]\) and \(y_i \geq 0\), this forces \(y_i = x_i\) (active ReLU).

When \(\delta_i = 0\) (inactive):

\[\begin{split}\begin{aligned} y_i &\geq 0 \\ y_i &\geq x_i \\ y_i &\leq x_i - l_i = x_i + |l_i| \\ y_i &\leq 0 \end{aligned}\end{split}\]

This forces \(y_i = 0\) (inactive ReLU).

Theorem (MILP Encoding Correctness): The big-M encoding above exactly captures the ReLU function: \(y_i = \max(0, x_i)\) for all possible values of \(x_i \in [l_i, u_i]\).

Proof:

Case analysis on \(x_i\):

1. If \(x_i \geq 0\): ReLU should be active (\(y_i = x_i\)). Setting \(\delta_i = 1\) satisfies all constraints with \(y_i = x_i\).

2. If \(x_i < 0\): ReLU should be inactive (\(y_i = 0\)). Setting \(\delta_i = 0\) forces \(y_i = 0\).

The encoding is complete (covers all cases) and sound (forces correct ReLU behavior). □

Why MILP Avoids Explicit Enumeration:

MILP solvers use branch-and-bound to implicitly explore the \(2^n\) space of \(\delta\) assignments. Instead of enumerating all patterns upfront, the solver:

1. Solves LP relaxation (continuous \(\delta_i \in [0,1]\)) → polynomial time

2. Branches on fractional \(\delta_i\) → creates two subproblems (0 and 1)

3. Bounds each subproblem using LP relaxation → prunes impossible branches

4. Implicit enumeration → only explores promising branches, not all \(2^n\) Worst-case complexity: Still \(O(2^n)\) (must explore all branches if LP relaxation is weak).

Average-case: Much better—commercial solvers (Gurobi, CPLEX) use sophisticated heuristics to prune branches early.

Soundness and Completeness Proofs:

Theorem (SMT/MILP Soundness): If an SMT/MILP verifier returns “VERIFIED”, the property truly holds for all inputs in the specified region.

Proof Sketch:

1. Encoding is sound: Each constraint in the encoding (linear layers, ReLU, input region, property) is a sound over-approximation of the true network behavior (for MILP) or exact logical equivalence (for SMT).

2. Solver is sound: SMT/MILP solvers are mathematically proven to return correct results (satisfiable/unsatisfiable for SMT, feasible/infeasible for MILP).

3. Composition: Sound encoding + sound solver → sound overall verification.

Theorem (SMT/MILP Completeness): If a property truly holds for all inputs, an SMT/MILP verifier will (given sufficient time and memory) return “VERIFIED”.

Proof Sketch:

1. Encoding is complete: The encoding captures all possible behaviors of the network (all \(2^n\) activation patterns are representable).

2. Solver is complete: SMT/MILP solvers are complete decision procedures—they always terminate with a definitive answer (for decidable theories like linear arithmetic).

3. Composition: Complete encoding + complete solver → complete overall verification.

Consequence: SMT/MILP methods are sound and complete. They never give false positives (sound) and never give “unknown” (complete). The cost is exponential worst-case complexity.

SMT Solver Mechanics

Modern SMT solvers like Z3 [De Moura and Bjørner, 2008] use sophisticated algorithms:

DPLL(T): Combines Boolean satisfiability (SAT) solving with theory-specific reasoning. The solver:

1. Abstracts theory constraints to Boolean variables

2. Searches for Boolean satisfying assignment

3. Checks if assignment is consistent with theory

4. Learns conflicts when inconsistent, backtracks

Theory solvers: For linear real arithmetic, use simplex-based solvers. For Boolean structure (ReLU disjunctions), use Boolean reasoning.

Conflict-driven learning: When a branch leads to contradiction, learn a clause preventing similar contradictions. This prunes the search space effectively.

Strengths: SMT solvers are general-purpose, mature, and highly optimized. They handle arbitrary logical combinations of constraints.

Limitations: Exponential worst-case complexity. As network size grows, the number of ReLU disjunctions grows exponentially, making the problem intractable.

MILP-Based Verification

Mixed-Integer Linear Programming formulates verification as optimization with both continuous and integer variables [Tjeng et al., 2019, Cheng et al., 2017].

Encoding Neural Networks as MILP

Linear layers: Same as SMT—linear equalities are native to MILP:

\[z = Wx + b\]

ReLU activations: Use binary indicator variables \(a \in \{0, 1\}\) and big-M constraints:

\[\begin{split}\begin{aligned} y &\geq z \\ y &\geq 0 \\ y &\leq z + M(1 - a) \\ y &\leq Ma \end{aligned}\end{split}\]

When \(a = 1\): \(y \geq z\) and \(y \leq M\) (ReLU active, \(y = z\))

When \(a = 0\): \(y \leq z + M\) and \(y \leq 0\) (ReLU inactive, \(y = 0\))

The big-M constant \(M\) must be large enough to not constrain the active case but small enough for numerical stability.

Objective: Minimize the margin to find adversarial examples:

\[\min \quad f(x)_{y_0} - \max_{c \neq y_0} f(x)_c\]

If the minimum is negative, a counterexample exists. If non-negative, the property holds.

Tighter encoding [Tjeng et al., 2019]: Use bounds from incomplete methods to tighten big-M values, reducing the feasible region and speeding up solving.

MILP Solver Mechanics

MILP solvers like Gurobi use branch-and-bound:

LP relaxation: Relax integer constraints (\(a \in [0, 1]\) instead of \(a \in \{0, 1\}\)), solve linear program efficiently.

Branching: Select fractional integer variable, create two subproblems (fixing \(a = 0\) and \(a = 1\)).

Bounding: Use LP relaxation to bound optimal value. Prune branches where bound is worse than best-known solution.

Cutting planes: Add linear inequalities (cuts) that tighten the LP relaxation without removing integer solutions.

Strengths: MILP is well-studied with commercial-grade solvers. Supports optimization objectives (find minimum adversarial perturbation).

Limitations: Integer variables (one per ReLU) create exponential branching. Scales poorly to large networks.

Table 25 SMT vs MILP for Verification

Aspect	SMT	MILP
Encoding	Logical formulas (disjunctions)	Linear inequalities + binary variables
Solver Type	DPLL(T) with theory solvers	Branch-and-bound with LP relaxation
Objective Support	Satisfiability only	Optimization (minimize margin)
Maturity	General-purpose SMT solvers (Z3)	Commercial MILP solvers (Gurobi)
Scalability	Hundreds of neurons	Hundreds of neurons
Main Challenge	ReLU disjunctions	Integer variables per ReLU

QCQP and SDP Encodings: Non-Linear Relaxations

Beyond linear encodings (SMT, MILP), we can use non-linear relaxations that provide tighter bounds at the cost of increased computational complexity. Quadratically Constrained Quadratic Programming (QCQP) and Semidefinite Programming (SDP) offer such relaxations.

QCQP Encoding for ReLU

Quadratic Constraint Encoding:

Instead of linear big-M constraints, QCQP encodes ReLU using quadratic equality constraints [Raghunathan et al., 2018]:

For \(y = \max(0, x)\) with bounds \(x \in [l, u]\) where \(l < 0 < u\):

\[\begin{split}\begin{aligned} y &\geq 0 \\ y &\geq x \\ y(y - x) &= 0 \end{aligned}\end{split}\]

Interpretation:

The quadratic constraint \(y(y - x) = 0\) forces either:

• \(y = 0\) (inactive ReLU), OR

• \(y = x\) (active ReLU)

This is exact for unstable ReLUs without requiring integer variables!

Problem: The quadratic equality constraint is non-convex. QCQP with non-convex constraints is NP-hard (no easier than MILP).

Solution: Relax the equality to an inequality:

\[y(y - x) \leq 0\]

This creates a convex QCQP. However, it’s no longer exact—it’s an over-approximation.

Theorem (QCQP Convex Relaxation Tightness): The convex QCQP relaxation is tighter than the linear triangle relaxation but looser than the exact ReLU constraint.

Proof Sketch:

1. Tighter than triangle: The quadratic constraint \(y(y-x) \leq 0\) captures curvature information that linear constraints cannot.

2. Looser than exact: The relaxation allows points where \(0 < y(y-x) < 0\), which are not on the true ReLU curve.

SDP Encoding: Semidefinite Programming

Semidefinite Relaxation:

SDP provides an even tighter relaxation by lifting the problem to a higher-dimensional space and enforcing positive semidefiniteness [Raghunathan et al., 2018].

Matrix Lifting:

Introduce matrix variable \(X \succeq 0\) (positive semidefinite) where:

\[\begin{split}X = \begin{bmatrix} 1 & z^T \\ z & Z \end{bmatrix}\end{split}\]

Here \(z\) is the vector of neuron activations, and \(Z\) represents second-order moments (outer products).

ReLU Constraints in SDP:

For \(y = \max(0, x)\), SDP encoding adds linear matrix inequalities (LMIs):

\[\begin{split}\begin{aligned} y &\geq 0 \\ y &\geq x \\ y &\leq \frac{u}{u - l}(x - l) \quad \text{(triangle upper bound)} \\ \text{plus } & \text{second-order cone constraints on } X \end{aligned}\end{split}\]

The key advantage: SDP can encode correlations between multiple neurons through the matrix \(Z\), capturing multi-neuron dependencies.

Theorem (SDP Tightness Hierarchy):

For single-neuron ReLU relaxation:

\[\text{Triangle (Linear)} \sqsubseteq \text{QCQP} \sqsubseteq \text{SDP} \sqsubseteq \text{Exact}\]

where \(\sqsubseteq\) denotes “looser than or equal to.”

Proof:

SDP relaxation includes all linear constraints (triangle relaxation) plus additional semidefinite constraints. By including more constraints, the feasible region is smaller (tighter). □

Multi-Neuron SDP:

SDP’s real power is multi-neuron analysis. For \(k\) neurons, the matrix \(X\) is \((k+1) \times (k+1)\), capturing correlations:

\[X_{ij} \approx z_i \cdot z_j \quad \text{(second-order moment)}\]

This allows SDP to reason about joint distributions of neuron activations, something linear and MILP methods cannot do efficiently.

Complexity Analysis:

Method	Variables	Constraints	Complexity (per iteration)	Complete?
SMT/SAT	\(O(n)\) Boolean + continuous	\(O(n)\) disjunctions	Exponential (worst-case)	Yes
MILP	\(O(n)\) binary + continuous	\(O(n)\) linear	\(O(2^n)\) (branch-and-bound)	Yes
QCQP	\(O(n)\) continuous	\(O(n)\) quadratic	\(O(n^{3.5})\) (interior-point)	No (relaxation)
SDP	\(O(n^2)\) matrix entries	\(O(n^2)\) LMI	\(O(n^6)\) (interior-point)	No (relaxation)

Why SDP is Exponentially Slower than LP:

SDP solvers use interior-point methods operating on the matrix space \(\mathbb{R}^{n \times n}\):

• Each iteration: \(O(n^6)\) (matrix operations + eigenvalue decomposition)

• Number of iterations: \(O(\log(1/\epsilon))\) (for \(\epsilon\)-optimal solution)

Compare to LP: \(O(n^{2.5})\) per iteration.

Practical Implication:

• LP: Networks with thousands of neurons (tractable)

• SDP: Networks with tens of neurons (already challenging)

SDP is orders of magnitude slower than LP, limiting it to very small networks or local analysis.

When to Use QCQP/SDP:

Use QCQP/SDP when:

1. Need tighter bounds than LP: Triangle relaxation too loose for verification

2. Multi-neuron correlations matter: Network has strong neuron dependencies

3. Network is tiny: <100 neurons (SDP tractable)

4. Research setting: Exploring tightness frontiers

Don’t use when:

1. Network is large: >100 neurons for SDP, >1000 for QCQP

2. Need complete verification: QCQP/SDP are incomplete (relaxations)

3. Speed matters: LP-based methods are 10-1000× faster

4. Standard benchmarks: CROWN/DeepPoly already sufficient

Tightness vs Completeness Tradeoff:

\[\begin{split}\begin{aligned} &\text{Incomplete Methods} \quad &&\text{Complete Methods} \\ &\text{(Tightness hierarchy)} \quad &&\text{(Exactness)} \\ &\text{Interval} < \text{LP} < \text{QCQP} < \text{SDP} \quad &&\text{SMT/MILP (Exact)} \\ &\uparrow \text{Tighter, slower} \quad &&\uparrow \text{Complete, exponential} \end{aligned}\end{split}\]

Connection to Theoretical Barriers:

Single-neuron linear relaxation (LP triangle) is optimal within the linear constraint class (see Theoretical Barriers in Neural Network Verification). QCQP/SDP overcome this barrier by using non-linear constraints, achieving tightness beyond the convex barrier at the cost of increased complexity.

Practical Considerations

When to Use Complete Methods

Use SMT/MILP when:

• Network is small (hundreds to low thousands of neurons)

• Absolute certainty is required (safety-critical applications)

• Finding tight counterexamples is valuable (adversarial training)

• Computational budget allows hours or days per property

• Regulatory compliance demands complete verification

Don’t use when:

• Network has millions of parameters (incomplete methods required)

• Rapid iteration is needed (complete methods too slow)

• “Unknown” is acceptable (incomplete methods suffice)

• Only need robustness estimates, not proofs

Improving Performance

Preprocessing with incomplete methods: Use bound propagation [Gowal et al., 2019, Singh et al., 2019, Weng et al., 2018, Zhang et al., 2018] to compute bounds on activations. These tighten big-M constants in MILP and prune branches in SMT.

Incremental solving: When verifying multiple similar properties, reuse solver state. Many SMT solvers support incremental mode where learned clauses carry over.

Parallelization: Verify multiple properties in parallel. Each property is independent, allowing trivial parallelization.

Timeout and best-effort: Set timeouts. If complete verification times out, fall back to incomplete methods or partial results.

Hybrid approaches [Wang et al., 2021]: Use complete methods only on small uncertain regions identified by incomplete methods. Incomplete methods handle bulk verification, complete methods resolve edge cases.

Limitations and Challenges

Scalability barrier: The fundamental NP-completeness [Katz et al., 2017, Weng et al., 2018] means exponential worst-case complexity is unavoidable. No algorithmic breakthrough can make complete verification polynomial-time (unless P=NP).

Network size: Current complete verifiers handle networks with thousands of neurons. Modern production networks have millions to billions of parameters—orders of magnitude beyond current capabilities.

Numerical issues: MILP requires careful tuning of big-M values. Too large causes numerical instability; too small gives incorrect results. Bounds from incomplete methods help but don’t eliminate the issue.

Memory consumption: Branch-and-bound explores exponentially many branches. Each branch requires memory. Large networks exhaust memory before finding answers.

Scalability Reality Check

Complete verification works well for small networks (e.g., ACAS Xu [Katz et al., 2017] with ~300 neurons). For larger networks, expect:

• Networks with thousands of neurons: feasible with good hardware and patience

• Networks with tens of thousands: very challenging, often timeout

• Networks with millions: currently intractable for complete methods

Comparison with Incomplete Methods

Incomplete methods [Gowal et al., 2019, Singh et al., 2019, Weng et al., 2018, Zhang et al., 2018] (bound propagation, abstract interpretation) trade completeness for scalability:

Advantages of incomplete methods:

• Polynomial time complexity (scale to large networks)

• Fast verification (seconds to minutes)

• GPU acceleration available [Xu et al., 2020]

Advantages of complete methods:

• Definitive answers (no “unknown”)

• Find tight counterexamples

• Required for regulatory compliance in some domains

Hybrid is often best [Wang et al., 2021, Zhang et al., 2022]: Use incomplete methods for initial screening, complete methods for critical cases. This balances speed and certainty.

Current State and Tools

Available tools:

• Marabou [Katz et al., 2019]: SMT-based verifier with specialized ReLU handling (Reluplex algorithm)

• Gurobi/CPLEX: Commercial MILP solvers, require encoding network as MILP

• Z3 [De Moura and Bjørner, 2008]: General-purpose SMT solver, requires manual encoding

Research directions:

• Tighter encodings that reduce solver search space

• Specialized solvers exploiting network structure (convolution, residual connections)

• Better preprocessing with incomplete methods to guide complete solvers

• Parallelization and distributed solving for large instances

Final Thoughts

SMT and MILP solvers provide the gold standard for neural network verification: complete, definitive answers. When you need absolute certainty—for safety-critical systems, regulatory compliance, or finding counterexamples—complete verification is essential.

The cost is computational. Complete methods scale to small networks but struggle with large ones. Understanding this tradeoff helps you choose appropriately: use complete methods where certainty matters and network size permits, use incomplete methods where scale matters more than completeness.

As verification research advances, the boundary between tractable and intractable shifts. Better encodings, faster solvers, and hybrid approaches push complete verification to larger networks. But the fundamental NP-completeness barrier remains—complete verification will always involve exponential worst-case complexity.

Further Reading

This guide provides comprehensive coverage of SMT and MILP approaches to complete neural network verification. For readers interested in diving deeper, we recommend the following resources organized by topic:

SMT-Based Verification:

The foundational work on SMT-based verification established both the approach and its limitations. Reluplex [Katz et al., 2017] extended the simplex algorithm to handle ReLU constraints directly, providing the first practical SMT-based verifier for neural networks. The same work proved NP-completeness of ReLU network verification, establishing fundamental computational barriers. Z3 [De Moura and Bjørner, 2008] provides a general-purpose SMT solver capable of encoding neural network verification problems.

MILP-Based Verification:

MILP formulations [Tjeng et al., 2019, Cheng et al., 2017] encode neural networks as mixed-integer programs, leveraging mature commercial solvers. The key challenge is encoding ReLU activations with binary variables and big-M constraints while maintaining numerical stability and tight bounds. Preprocessing with incomplete methods [Weng et al., 2018, Zhang et al., 2018] tightens big-M values, significantly improving MILP solver performance.

Complexity and Limitations:

The NP-completeness result [Katz et al., 2017, Weng et al., 2018] proves that complete verification has worst-case exponential time complexity. This isn’t an engineering limitation—it’s a fundamental mathematical barrier. Understanding this complexity helps set realistic expectations about what complete methods can achieve.

Incomplete Methods for Comparison:

Complete methods are often contrasted with incomplete approaches. Bound propagation [Gowal et al., 2019, Weng et al., 2018, Zhang et al., 2018] and abstract interpretation [Singh et al., 2019] trade completeness for polynomial-time complexity, scaling to large networks by accepting “unknown” results. These methods are often used to preprocess and guide complete solvers.

Hybrid Approaches:

State-of-the-art verification combines complete and incomplete methods. α-β-CROWN [Wang et al., 2021, Zhang et al., 2022] uses incomplete bound propagation for initial verification, applying branch-and-bound (a complete method) selectively where needed. This hybrid strategy balances the strengths of both approaches. GPU acceleration [Xu et al., 2020] enables practical implementation of these hybrid strategies.

Specialized Complete Verifiers:

Marabou [Katz et al., 2019] extends Reluplex with additional features and optimizations, representing the current state-of-the-art in SMT-based neural network verification. It handles networks with thousands of neurons through careful encoding and pruning strategies.

Related Topics:

For understanding the theoretical foundations that SMT and MILP methods are built upon, see The Verification Problem: Mathematical Formulation. For the guarantees that complete methods provide, see Soundness and Completeness. For specialized handling of ReLU constraints, see Marabou and Reluplex: Extended Simplex for Verification. For hybrid approaches combining complete and incomplete methods, see Branch-and-Bound Verification.

Next Guide

Continue to Marabou and Reluplex: Extended Simplex for Verification to learn about the Reluplex algorithm, a specialized SMT solver optimized for ReLU neural networks.

[1] (1,2)

Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In International Symposium on Automated Technology for Verification and Analysis, 251–268. Springer, 2017.

[2] (1,2,3)

Leonardo De Moura and Nikolaj Bjørner. Z3: an efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, 337–340. Springer, 2008.

[3] (1,2,3)

Sven Gowal, Krishnamurthy Dj Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In Proceedings of the IEEE International Conference on Computer Vision, 4842–4851. 2019.

[4] (1,2,3,4,5,6)

Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: an efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, 97–117. Springer, 2017.

[5] (1,2)

Guy Katz, Derek A Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, and others. The marabou framework for verification and analysis of deep neural networks. In International Conference on Computer Aided Verification, 443–452. Springer, 2019.

[6] (1,2)

Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems, 10877–10887. 2018.

[7] (1,2,3)

Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems, 15072–15083. 2019.

[8] (1,2,3)

Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations. 2019.

[9] (1,2,3)

Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 2021.

[10] (1,2,3,4,5,6,7)

Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for relu networks. In International Conference on Machine Learning, 5276–5285. 2018.

[11] (1,2)

Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 2020.

[12] (1,2)

Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. General cutting planes for bound-propagation-based neural network verification. arXiv preprint arXiv:2208.05740, 2022.

[13] (1,2,3,4)

Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in neural information processing systems, 4939–4948. 2018.