Verification Taxonomy: A Systematic View

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:

Exactness: Do I always give definitive answers, or sometimes “I don’t know”?
Certainty: Do I provide absolute guarantees, or probabilistic ones?
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 and give a YES/NO/counterexample. They work for small networks, where “small” is a resource statement rather than a property of the method — and the exact solver can also be the fast option there, which is why “exact means slow” is not a definition but an observation about the instances people run.

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: on small networks; the reachable size depends on the solver, its settings and the property
Takes: grows quickly with size, and a run stopped by a timeout has concluded nothing
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

Three Axes That Are Not One Tradeoff

Three things get asked of a verifier: how tight a bound, how long it takes, and how large a network it handles. These are worth separating before they are traded off, because two of them describe a method and the third describes a relationship between a method and a machine. It is tempting to line these up as a menu where you may pick two, and to conclude from NP-hardness that tightness and speed cannot coexist.

Both moves need fixing, because they mix three different kinds of statement.

The three are not the same kind of object. Tightness and speed are properties of a method, so they are comparable and the pair is a real engineering tradeoff. Scale is a property of a problem instance relative to a method’s resources, so “scalable” is not a property of a method at all until it is attached to a resource budget and a hardware claim. “Scalable” without those two qualifiers is not a statement that can be true or false.

NP-hardness does not say tight and fast cannot coexist. NP-hardness of the general problem says that no algorithm solves every instance in polynomial time in the worst case. That is compatible with a method being both tighter and faster than another on every instance anyone actually runs. A relaxation that returns the exact maximum on a small network is tight and fast: the spurious-point example in the soundness chapter settles its property by partitioning the domain, and exact solving on a small network can be milliseconds, which that chapter says outright. The correct statement is conditional — a method that is both tight and fast on your network class exists, and finding it is the research problem, not a prohibition on the combination.

What the hardness result does rule out is one method that is tight, fast, and complete on arbitrary networks of unbounded size. That is a claim about the worst case, and it is a real constraint on what a benchmark can promise.

Simple Decision Flowchart

Network size? Size picks a starting point, not a guarantee, and the thresholds below are where the tractable frontier tends to sit rather than a law.

Small: an exact or optimization-based method is affordable, so tighter or complete answers are within reach.
Medium: propagation with refinement. Cheap first pass, refinement where it matters.
Large: fast propagation, or a probabilistic certificate. Accept UNKNOWN or a statistical claim, and say which one you are accepting.

What matters most?

Need a claim about every input: a sound method, which may still return UNKNOWN. Completeness is a separate decision, taken about the network in hand rather than about the method.
Need speed: fast propagation, accepting looser bounds or UNKNOWN in exchange.
Need tightness: optimization-based bounds, or refinement, accepting a longer runtime.
Need to scale: fast propagation, or a probabilistic certificate — and note that a probabilistic certificate is a claim of a different kind, not a tighter version of the same one.

Key insight: these are three questions asked separately. “Pick two” replaces them with one, and the reader loses the ability to tell which one they are actually trading away.

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.

Key Takeaways

Two families, and the split is about the answer, not the method. Incomplete methods return a region that contains the reachable set; complete methods return yes or no. Relaxation methods compute a tighter over-approximation; search methods split the input region until the answer is determined. Most real verifiers combine both.

Choose by what you need to do with the result. A region you can train against or explain to a reviewer is enough for many uses. A definitive yes or no is required when you have to certify a single instance, and that is the expensive case.

Soundness is not negotiable. An unsound verifier is worse than none, because a false “safe” is worse than an admitted “unknown”. Every method described in this series, incomplete ones included, is sound; that is the property to check when you evaluate a tool.

Certification is not a certificate of intent. A network can be verifiably robust to $\ell_\infty$ and still fail entirely to a rotation, a patch, or a change in the input distribution. What you certify is a property you chose, so choose it against the threat you actually face.