A Guide to Neural Network Verification

Why verification matters, threat models, problem formulation, and theoretical fundamentals.

1. 1.1What Does a Neural Network Verifier Prove?One question with three parts, three answers that do not substitute for each other, and what soundness and completeness each license.
2. 1.2Why Neural Network Verification?Understanding adversarial attacks and the motivation for formal verification of neural networks.
3. 1.3The Verification Problem: Properties, Margins, and CounterexamplesFormulate a neural-network property, negate it into a counterexample query, and distinguish a valid bound from an actual violating input.
4. 1.4Threat Models in Neural Network VerificationThreat model formulations including ℓₚ norms, semantic perturbations, and attack specifications for neural network verification.
5. 1.5Soundness, Completeness, and UNKNOWNTwo independent properties, three outputs with different force, and why a sound method reports UNKNOWN on a robust network.
6. 1.6Verification Taxonomy: A Systematic ViewA comprehensive taxonomy of verification methods, including scalability measures and tightness rankings.
7. 1.7Complexity and Relaxation Limits: What the Barriers Actually SaySeparate worst-case complexity, incomplete relaxations, and practical solver limitations without treating any of them as an impossibility of verification.

Core verification techniques including bound propagation, LP, SMT/MILP, and specialized methods.

1. 2.1Neural Network Decomposition: The Unary-Binary FrameworkThe foundational unary-binary operation decomposition that enables neural network verification, explaining why activation functions drive computational complexity.
2. 2.2Bound Propagation: Intervals, Symbolic Bounds, and Lost DependenciesCompute interval bounds, construct a ReLU relaxation, and use a small network to see what information each representation loses.
3. 2.3Beyond ReLU: Modern Activation FunctionsHow activation function choices impact neural network verification, from ReLU's optimal convex hull to the challenges of GeLU, Swish, and other modern activations.
4. 2.4Linear Programming for VerificationLP formulations for neural network verification, including triangle relaxation, duality theory, complexity analysis, and comparison with other bound propagation methods.
5. 2.5Lipschitz Bounds and Curvature-Based VerificationLipschitz-based verification methods including Lipschitz constant computation, LipSDP, spectral normalization, and curvature-based approaches for robustness certification.
6. 2.6Semidefinite Relaxations: Lifting Without a Universal RankingSet up a lifted semidefinite relaxation, and separate what a PSD constraint, a moment constraint and a rank-one constraint each say -- because the third is the one that gets dropped.
7. 2.7SMT and MILP Solvers for VerificationComplete verification using SMT and MILP solvers, including encoding theory, QCQP/SDP formulations, and the exponential complexity of ReLU activation patterns.
8. 2.8Branch-and-Bound VerificationHow branch-and-bound combines incomplete and complete verification methods for scalable neural network verification, including the alpha-beta-CROWN algorithm.
9. 2.9Marabou and Reluplex: Extended Simplex for VerificationThe Reluplex algorithm and Marabou verifier for complete neural network verification using extended simplex methods specialized for ReLU networks.
10. 2.10Single-Neuron, Multivariate, and Multi-Neuron RelaxationsDistinguish the objects being relaxed and understand why exact local hulls can still miss joint neural-network behaviour.

Practical applications including robustness testing, certified training, benchmarks, and specifications.

1. 3.1Robustness Testing GuideA practical guide to testing neural network robustness using both empirical attacks and formal verification
2. 3.2Writing and Checking a VNN-LIB SpecificationTranslate a property into a satisfiability query and check its domain, output direction, and intended interpretation.
3. 3.3Falsifiers and VerifiersThe spectrum between adversarial attacks (falsifiers) and formal verification (verifiers), and how to combine them effectively
4. 3.4Verification BenchmarksVerification benchmarks including VNN-COMP and standard datasets used to evaluate verification tools
5. 3.5Certified Adversarial TrainingCertified adversarial training methods that provide provable robustness guarantees during training, including IBP, CROWN, and TRADES variants
6. 3.6Regularization-Based Robust TrainingRegularization-based training techniques including Lipschitz regularization, margin maximization, TRADES, and stability-based approaches

Cutting-edge research including scalability challenges, diverse architectures, and certified defenses.

1. 4.1Verification ScalabilityScalability challenges in neural network verification, including the scalability-tightness tradeoff and practical scaling techniques
2. 4.2Verifying Diverse ArchitecturesVerification challenges across diverse architectures including RNNs, Transformers, Graph Neural Networks, and hybrid models
3. 4.3Training Robust NetworksTraining methods for building robust networks, including adversarial training, certified training, architecture choices, and the training-verification loop
4. 4.4Certified Defenses and Randomized SmoothingRandomized smoothing and other probabilistic certified defenses that scale to large networks
5. 4.5Beyond ℓₚ: Alternative Threat ModelsExtensions to threat models beyond ℓₚ norms, including semantic adversaries, patch adversaries, sparse perturbations, and distributional attacks
6. 4.6Real-World ApplicationsReal-world applications of neural network verification across domains like autonomous vehicles, medical systems, cybersecurity, and financial systems