Phase 2: Core Verification Techniques

Phase 2: Core Verification Techniques

Methods for Certifying Robustness

1 min read · 288 words

Building on the foundations, this phase provides comprehensive coverage of the core algorithmic approaches to neural network verification. You’ll learn the unary-binary decomposition framework that underlies all methods, understand how activation functions affect verification complexity, master bound propagation techniques, explore incomplete methods (LP relaxations, multi-neuron relaxations, SDP, Lipschitz bounds), and study complete verification approaches (SMT, MILP, branch-and-bound). This phase focuses on the technical depth of verification algorithms.

What You’ll Learn

This phase covers core verification algorithms: from the fundamental decomposition framework and bound propagation to incomplete methods (LP, SDP, Lipschitz) and complete approaches (SMT, MILP, branch-and-bound).

Guides in This Phase

1️⃣ Operation Decomposition

The unary-binary framework foundation for all verification methods

Neural Network Decomposition: The Unary-Binary Framework
2️⃣ Activation Functions

How different activations affect verification and their approximation techniques

Beyond ReLU: Modern Activation Functions
3️⃣ Bound Propagation

IBP, CROWN, DeepPoly, and other core incomplete verification techniques

Bound Propagation Approaches
4️⃣ LP Verification

LP relaxation, dual formulation, and triangle relaxation

Linear Programming for Verification
5️⃣ PRIMA Verification

Capturing neuron correlations with product-based relaxations

Multi-Neuron Relaxation and PRIMA
6️⃣ SDP Verification

Semi-definite programming relaxations and nuclear norm approaches

SDP-Based Verification: Semi-Definite Programming for Tighter Bounds
7️⃣ Lipschitz Verification

Lipschitz constant estimation and spectral normalization

Lipschitz Bounds and Curvature-Based Verification
8️⃣ SMT/MILP Verification

Constraint solving with SAT/SMT and mixed-integer linear programming

SMT and MILP Solvers for Verification
9️⃣ Marabou & Reluplex

Specialized complete verification using the Reluplex algorithm

Marabou and Reluplex: Extended Simplex for Verification
🔟 Branch and Bound

Hybrid approaches combining branching with bound propagation (α-β-CROWN)

Branch-and-Bound Verification

Next Phase

After mastering the core techniques, move on to Phase 3: Robust Training & Practical Implementation to learn about robust training and practical implementation.