Skip to main content
Phase 1: Foundations Guide 6

Verification Taxonomy: A Systematic View

A comprehensive taxonomy of verification methods, including scalability measures and tightness rankings.

Real problem: You pick a verification tool and it says “unknown.” So you find another tool and it succeeds. Why? Different methods make different tradeoffs. This guide helps you understand those choices.

Three Core Tradeoffs

Every verification method answers three questions differently:

  1. Exactness: Do I always give definitive answers, or sometimes “I don’t know”?
  2. Certainty: Do I provide absolute guarantees, or probabilistic ones?
  3. Computation: Do I propagate bounds layer-by-layer (fast), or solve optimization (slower)?

Understand these axes, and you can predict which method fits your constraints.

Taxonomy Benefits

A well-organized taxonomy helps:

  • Researchers: Identify open problems and unexplored method combinations
  • Practitioners: Choose verification methods matching their constraints
  • Students: Build mental models of the verification landscape
  • Tool builders: Position new methods relative to existing work

Axis 1: Exact vs Approximate Answers

Exact methods search exhaustively, always give YES/NO/counterexample. Slow. Work for small networks.

Approximate methods run fast, but sometimes say “unknown.” Scale to large networks.

Why? Exhaustive search takes exponential time. For real networks, you need the speed trade-off.

Axis 2: Absolute vs Probabilistic Guarantees

Absolute guarantee: “For 100% of inputs, robustness holds.” Conservative, but certain.

Probabilistic guarantee: “With 99% confidence, robustness holds.” Tighter bounds, but statistical.

Trade-off: Absolute methods are slower. Probabilistic methods scale better but require confidence in statistics instead of absolute proof.

Axis 3: Propagation vs Optimization

Layer-by-layer propagation: Follow bounds through network quickly. Fast, but may be loose.

Optimization formulation: Model as math problem, solve for tightest bounds. Slow, but tight.

Hybrid (refine when needed): Start fast. If result is “unknown,” partition input space and refine. Combines both speeds.

Which Method When?

Exact solvers (small networks, absolute answers needed):

  • Formulate as constraint problem, solve exhaustively
  • Works: up to ~1000 neurons
  • Takes: minutes to hours
  • Use: safety-critical, need proof

Fast propagation (large networks, speed critical):

  • Layer-by-layer bound propagation
  • Works: millions of neurons
  • Takes: seconds
  • Use: production systems, rapid iteration
  • Caveat: sometimes says “unknown”

Optimization solvers (medium networks, tight bounds):

  • Formulate as optimization problem (linear, quadratic, etc.)
  • Works: thousands to tens of thousands neurons
  • Takes: minutes
  • Use: research, need tighter bounds

Probabilistic methods (any size, accept statistics):

  • Add noise, estimate bounds statistically
  • Works: unlimited network size
  • Takes: depends on confidence level
  • Use: large networks, probabilistic guarantee acceptable

Refinement (adaptive, balance):

  • Start with fast propagation
  • If “unknown,” partition space and refine
  • Works: hybrid of above
  • Use: practical systems needing flexibility

The Impossible Triangle

Three things you want: tight bounds, fast computation, scales to big networks.

Pick two. That’s the rule.

  • Tight + Fast: Nope. NP-hardness blocks you.
  • Tight + Scalable: Yes (probabilistic methods sacrifice certainty).
  • Fast + Scalable: Yes (loose bounds, trade tightness).

No method gets all three simultaneously.

Simple Decision Flowchart

Network size?

  • Small: Use exact solver. Precise answers, can afford longer computation.
  • Medium: Use propagation with refinement. Fast initially, refine if unsure.
  • Large: Use fast propagation or probabilistic. Accept “unknown” results or statistical confidence.

What matters most?

  • Need absolute proof: Small networks + exact solvers.
  • Need speed: Fast propagation, accept looser bounds.
  • Need tightness: Optimization or probabilistic methods.
  • Need to scale: Probabilistic or fast propagation only.

Key insight: Your constraints determine which tradeoff to accept. Choose accordingly, don’t chase the impossible.

What Doesn’t Fit

Open frontiers:

Scaling. Verification handles modest networks. Real systems are far larger. The gap persists.

Modern architectures. ReLU is simple. Transformers, attention, modern activations are harder. Verification lags behind.

Real-world robustness. We verify mathematical bounds. But real attacks are semantic (rotations, transformations). Need different approaches.

Practical accuracy. Certified networks lose accuracy. Balancing robustness and utility remains challenging.

These are where future work lies.

Next Guide

Continue to Theoretical Barriers to understand the fundamental mathematical limits and complexity barriers in neural network verification.

← Back to Guides