Bound Propagation: Intervals, Symbolic Bounds, and Lost Dependencies

Bound propagation replaces a set of possible values with a representation that is easier to transform. The required contract is containment: after each operation, the represented set must contain every value that operation can produce from the preceding set.

Tightness asks how much extra behaviour is included. Soundness asks whether any real behaviour has been excluded. Improving one is not permission to violate the other.

Interval propagation through an affine layer

This is interval bound propagation (IBP), and it is the cheapest domain in per-layer cost: one interval per coordinate, so the work is linear in the layer’s width, against a polytope or zonotope that grows with the number of constraints. As presented by Singh et al. (2019) in the DeepPoly framework, and earlier as the abstract-interpretation system of Singh et al. (2018), it replaces a set of reachable values with an interval per coordinate.

Let a layer input satisfy $l\le x\le u$ componentwise, and let $z=Wx+b$. Define $W^+=\max(W,0)$ and $W^-=\min(W,0)$ elementwise. Then

A positive weight takes its lower contribution from $l$; a negative weight takes it from $u$. This sign choice is the derivation, not a convention to memorise.

import numpy as np

def affine_bounds(W, b, lower, upper):
    W = np.asarray(W, dtype=float)
    b = np.asarray(b, dtype=float)
    lower = np.asarray(lower, dtype=float)
    upper = np.asarray(upper, dtype=float)
    if W.ndim != 2 or lower.shape != (W.shape[1],):
        raise ValueError("Incompatible matrix and input bounds")
    if upper.shape != lower.shape or b.shape != (W.shape[0],):
        raise ValueError("Incompatible upper bound or bias")
    if not all(np.isfinite(a).all() for a in (W, b, lower, upper)):
        raise ValueError("All inputs must be finite")
    if np.any(lower > upper):
        raise ValueError("An interval has lower > upper")
    pos, neg = np.maximum(W, 0), np.minimum(W, 0)
    return pos @ lower + neg @ upper + b, pos @ upper + neg @ lower + b

This is the real-arithmetic formula evaluated numerically for demonstration. Plain NumPy rounding is not a general proof that all returned machine intervals are outward-rounded.

For a dense matrix with $n$ output and $m$ input coordinates, the matrix-vector work is $O(nm)$, not $O(n)$ per layer independent of width. Special operators may have a different structure to exploit.

ReLU: stable and unstable intervals

For $y=\operatorname{ReLU}(z)$, interval propagation gives $[\max(0,l_z),\max(0,u_z)]$. If the interval is nonnegative, $y=z$; if it is nonpositive, $y=0$.

An interval crossing zero requires a relaxation to retain the relationship between $z$ and $y$. For $l<0<u$, use

These inequalities describe the scalar graph hull. Omitting $y\ge z$ gives a looser set, not that exact hull.

The dependency that intervals forget

If $v_1=x$ and $v_2=x$ for $x\in[-1,1]$, the true value of $v_1-v_2$ is zero. Treating the intervals independently gives $[-2,2]$.

The problem is not inaccurate scalar bounds: both bounds were exact. It is the missing relation $v_1=v_2$. Describing the loss as “twice the true width” is invalid because the true width is zero.

Symbolic bounds retain expressions involving shared variables. Back-substitution can simplify such expressions before concretising them to numbers. When a coefficient is negative, a lower bound on the whole expression uses the corresponding upper bound on that variable. This sign rule is essential.

CROWN, introduced by Zhang et al. (2018), is one family of methods built around propagating bounds through activation surrogates. It should not be described as automatically recovering all dependencies or uniformly improving by a fixed exponential factor.

Compare three answers on one network

Use

The true value is always $1/4$. Independent intervals give $h_1,h_2\in[0,1]$, then $g\in[-7/4,9/4]$.

Retaining $x,h_1,h_2$ and both triangle hulls gives a smaller LP feasible set. Its minimum and maximum for $g$ are $-1/4$ and $3/4$. At the minimum, $x=0,h_1=0,h_2=1/2$ is feasible in the relaxation but not in the network.

This is a comparison for one explicitly defined instance, not a ranking of all implementations of these methods.

Where zonotopes fit

A zonotope has the form $Z=\{c+G\eta:\eta\in[-1,1]^p\}$. Its affine image under $Wx+b$ is exactly $\{Wc+b+WG\eta\}$, preserving the shared generator coefficients.

A standard zonotope is centrally symmetric. Adding generators does not make it exactly represent a nondegenerate triangle. Nonlinear transformers may introduce slack, and generator reduction may discard dependencies. These choices matter when comparing an actual zonotope analysis with a symbolic-bound analysis.

Do not infer a universal comparison between DeepPoly (Singh et al., 2019) and CROWN (Zhang et al., 2018) and every zonotope method from the expressive power of unrestricted polyhedra. A representation class, the implemented transformers and the chosen optimisation routine are different objects.

Key Takeaways

Intervals can lose relations even when each scalar bound is exact. Shared dependence is information, not just interval width.

The ReLU triangle has three relation inequalities. State the input interval and every required facet.

A relaxed bad point is not a network counterexample. Test it against the original activations before interpreting it.

Compare explicit methods under explicit conditions. Avoid a total precision order over labels that mix domains and solvers.