How Can Bounds Travel Through a Network? Neural Network Certification, Part 3

On this page

Certification Series

How can we follow every allowed input at once?

In Part 2, we proved that April’s output margin remains positive when either input feature changes by at most $0.1$. The proof bounded two hidden neurons by hand. A larger network needs the same reasoning applied systematically across every layer.

To scale that proof, we follow whole ranges of April’s feature values through every neuron. Attach a lower and upper bound to each input, then calculate new bounds after every network operation. One pass through the network can cover the entire allowed set.

Give each input a lower and upper bound

An interval $[\underline v,\overline v]$ summarizes every value $v$ satisfying

\[\underline v\leq v\leq\overline v.\]

For April’s reference input $x_0=(0.5,0.5)$ and radius $0.1$, the $\ell_\infty$ input set is

\[x_1\in[0.4,0.6],\qquad x_2\in[0.4,0.6].\]

These two intervals describe the same square used in Part 2. We now propagate them through the fixed classifier:

\[\begin{aligned} z_1 &= x_1+x_2-0.5, & h_1 &= \operatorname{ReLU}(z_1),\\ z_2 &= x_1-x_2, & h_2 &= \operatorname{ReLU}(z_2),\\ f_{\mathrm{cat}} &= 0.2+h_1+h_2, & f_{\mathrm{other}} &= 2h_2. \end{aligned}\]

Carry the bounds through an affine layer

Start with $z_1=x_1+x_2-0.5$. Its smallest value uses both lower input bounds, and its largest value uses both upper bounds:

\[z_1\in [0.4+0.4-0.5,\;0.6+0.6-0.5] =[0.3,0.7].\]

The subtraction in $z_2=x_1-x_2$ reverses which endpoint of $x_2$ we use. To make $z_2$ small, choose a small $x_1$ and a large $x_2$. To make it large, choose a large $x_1$ and a small $x_2$:

\[z_2\in [0.4-0.6,\;0.6-0.4] =[-0.2,0.2].\]

These endpoint choices handle any affine neuron. To compute the lower output bound, use the lower input endpoint for a positive weight and the upper input endpoint for a negative weight. Reverse those choices for the upper output bound, then add the bias.

Carry the bounds through ReLU

Because ReLU is monotone, applying it to an interval gives

\[v\in[\underline v,\overline v] \quad\Longrightarrow\quad \operatorname{ReLU}(v) \in[\max(0,\underline v),\max(0,\overline v)].\]

The interval’s position relative to zero determines which of three cases applies:

• If $\overline v\leq0$, the neuron is always inactive and its output is $[0,0]$.
• If $\underline v\geq0$, the neuron is always active and keeps the interval $[\underline v,\overline v]$.
• If $\underline v<0<\overline v$, the ReLU is unstable: it may be active or inactive, and its output interval is $[0,\overline v]$.

For April’s first neuron, $z_1\in[0.3,0.7]$ is always positive. Therefore,

\[h_1\in[0.3,0.7].\]

The second interval $z_2\in[-0.2,0.2]$ crosses zero, so this ReLU is unstable:

\[h_2\in[0,0.2].\]

Why combine the scores before bounding them?

We could bound each score separately. Using $h_1\in[0.3,0.7]$ and $h_2\in[0,0.2]$ gives

\[f_{\mathrm{cat}}=0.2+h_1+h_2\in[0.5,1.1], \qquad f_{\mathrm{other}}=2h_2\in[0,0.4].\]

Subtracting these two intervals would produce

\[m\in[0.5-0.4,\;1.1-0]=[0.1,1.1].\]

That interval contains every possible margin, but it has forgotten that both scores use the same $h_2$. Its lower endpoint combines the smallest cat score, which uses $h_2=0$, with the largest other score, which uses $h_2=0.2$. One hidden value cannot take both values at once.

The property depends directly on the score difference, so we first combine the two final-layer formulas into that shared expression:

\[\begin{aligned} m &=f_{\mathrm{cat}}-f_{\mathrm{other}}\\ &=(0.2+h_1+h_2)-2h_2\\ &=0.2+h_1-h_2. \end{aligned}\]

Now propagate the hidden intervals directly into this margin:

\[m\in[0.2+0.3-0.2,\;0.2+0.7-0]=[0.3,0.9].\]

This algebraic merge of the final linear layer with the desired score difference is called last-layer elision. It preserves the layer’s effect by rewriting that layer together with the property before computing bounds. Here, the rewrite raises the margin’s lower bound from $0.1$ to $0.3$.

Every possible margin is therefore at least $0.3$. The model predicts cat for every input in $S_\infty(x_0,0.1)$, which recovers the certificate derived by hand in Part 2.

Applying these interval calculations layer by layer is called interval bound propagation, or IBP. Each operation encloses every value that operation can produce from the preceding intervals. The input intervals contain every allowed input, and each sound propagation step preserves that containment. Repeating the argument layer by layer makes the final interval contain every possible margin. This induction is why a positive lower margin bound is a sound certificate.

Last-layer elision and the use of IBP bounds in training are studied in On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. We will revisit that use in Part 6.

IBP succeeds on April’s radius-$0.1$ square. To see when independent intervals lose useful relationships, keep the network fixed and enlarge only the allowed input region.

Increase the radius: the bound becomes inconclusive

Now expand the allowed change for each feature from $0.1$ to $0.2$:

\[x_1,x_2\in[0.3,0.7].\]

The propagation rules do not change. Applying them to the larger square gives

Quantity	Interval at radius $0.2$
$z_1=x_1+x_2-0.5$	$[0.1,0.9]$
$h_1=\operatorname{ReLU}(z_1)$	$[0.1,0.9]$
$z_2=x_1-x_2$	$[-0.4,0.4]$
$h_2=\operatorname{ReLU}(z_2)$	$[0,0.4]$
$f_{\mathrm{cat}}$	$[0.3,1.5]$
$f_{\mathrm{other}}$	$[0,0.8]$
Margin from separate score intervals	$[-0.5,1.5]$
Margin after last-layer elision	$[-0.1,1.1]$

Last-layer elision improves the lower bound from $-0.5$ to $-0.1$, but even the tighter margin interval crosses zero. The interval alone supplies no concrete input with a negative margin, so it cannot falsify the property. It also cannot prove that every margin is positive. This IBP run must report unknown.

We can locate where information disappeared. The lower endpoint $h_1=0.1$ is attained at $x_1=x_2=0.3$. The upper endpoint $h_2=0.4$ is attained at $x_1=0.7$ and $x_2=0.3$. No single input produces both extremes. Combining the intervals in the margin calculation therefore allows the two hidden values to vary as if they were independent.

Each neuron is summarized by two endpoints. This fixed-size bookkeeping scales to networks of any depth, while the same summary can discard relationships between neurons. We can now state the calculation as an algorithm.

Turn the calculation into the IBP algorithm

IBP follows the same four steps for a network of any depth:

1. Put a lower and upper bound on every input coordinate.
2. For each affine layer, choose endpoints according to the signs of its weights.
3. For each ReLU, replace $[\underline v,\overline v]$ with $[\max(0,\underline v),\max(0,\overline v)]$.
4. Combine the final linear layer with the required score difference, then bound that margin directly. This is last-layer elision.

If the resulting margin lower bound is positive, the property is verified. A nonpositive lower bound cannot certify the property. Falsification still requires a concrete allowed input that violates it.

IBP scales the proof but can lose relationships

At radius $0.1$, interval propagation and last-layer elision carry April’s entire input square through the network and prove $m\geq0.3$. At radius $0.2$, the same method combines hidden-neuron extremes that come from different inputs and returns unknown.

Part 4 asks: why do simple bounds lose this information? We will answer by preserving linear relationships between neuron values.