Prior reading: What Are Formal Methods? | Linear Algebra Proofs of Optimality

The Core Question

Given a neural network $f$ and an input region $\mathcal{X}$, what is the set of all possible outputs $f(\mathcal{X})$?

If we can bound this set, we can prove properties like "no input in this region produces a harmful output."

Why This Is Hard

Neural networks are piecewise-linear (ReLU) or worse (sigmoid, softmax). The number of linear regions grows exponentially with depth. Exact reachability is NP-hard.

Linear Relaxations

The key insight: replace the hard non-linear problem with a tractable linear over-approximation.

  • CROWN: Propagate linear bounds layer by layer
  • Alpha-CROWN: Optimize the relaxation tightness
  • Beta-CROWN: Add branch-and-bound for precision
  • Alpha-beta-CROWN: Combine both — state of the art in VNN-COMP

What You Get

A sound over-approximation of the output set. If the bounded region is safe, the network is provably safe for those inputs. If it's not, you might have a real violation or a loose bound.

Practical Limitations

  • Scales to networks with millions of parameters, but gets looser with depth
  • Tightness depends heavily on network architecture
  • Only handles properties expressible as input-output constraints

Connection to Safety

This is the workhorse of neural network verification. Every other formal method for NNs either uses reachability internally or competes with it.