Why Linear Bounds Lose Cancellation When They Are Summed

Bound propagation makes a neural network tractable by replacing each nonlinear activation with something easier to substitute. The standard choice is a pair of linear symbolic bounds. Each bound can be perfectly sound and the final answer can still be disappointingly weak.

The gap appears when the verifier stops asking about one activation and asks about a sum of them. The separate bounds remember what every term may do, but not how their errors depend on the same earlier variables.

Sound pieces can make a loose sum

Suppose an activation output $y_i = \sigma(z_i)$ has lower and upper bounds

$$\ell_i(z_i) \leq y_i \leq u_i(z_i).$$

For a target expression $c^\top y + d$, back-substitution chooses the lower or upper bound for each $y_i$ according to the sign of $c_i$. This step is sound. It is also local: every activation is handled as though its worst approximation error could occur independently of every other one.

That independence is usually false. The pre-activations are affine expressions of shared earlier variables. When one relaxation is loose above the true curve, another may be loose in the opposite direction at the same input. The true sum can cancel those deviations; a sum of separate linear worst cases cannot.

This is the sum-relaxation problem: minimizing each term’s bound error in isolation is not the same as minimizing the error of the linear combination the property actually asks about.

The running example

The TiSum paper isolates the issue in a small ReLU network with $x_1,x_2 \in [-1,1]$. Its output is

$$x_9 = -x_6 + x_7 - x_8 + \frac{5}{2}.$$

The verification property is $x_9 \geq 0$. Ordinary linear relaxation and back-substitution derive the lower bound

$$x_9 \geq -\frac{1}{2},$$

so the verifier cannot prove the property. Local quadratic relaxation instead derives

$$x_9 \geq \frac{1}{2},$$

which proves it.

The difference is not that the linear bounds were unsound. They admitted combinations of relaxation error that cannot happen together. The quadratic expressions kept enough shared-variable structure for the positive and negative terms to cancel before the remaining uncertainty was linearized.

What a quadratic term remembers

A linear symbolic expression can preserve first-order dependence such as $a x_1 + b x_2 + c$. It cannot express curvature or interaction. A quadratic expression can additionally retain

$$x_1^2, \qquad x_2^2, \qquad x_1x_2.$$

Those terms are useful because the activations being summed are not unrelated scalars; they are different nonlinear views of the same earlier state. When a coefficient later subtracts one activation from another, quadratic terms can cancel algebraically before any interval worst case is taken.

This is the important ordering. Linearize every activation first and the relationship is gone. Combine the nonlinear symbolic expressions first and some of it can disappear by exact algebra rather than by approximation.

Tighter does not mean globally nonlinear

Keeping a polynomial expression through the whole network would replace one scalability problem with another. TiSum only asks the nonlinear form to survive one local substitution. After the relevant terms have been combined, the square and cross terms are soundly relaxed back to linear expressions and ordinary back-substitution resumes.

That design also states the limitation cleanly. A later term-wise linearization may erase the gain, so a quadratic path is not guaranteed to beat a good linear path for every neuron and interval. What it guarantees is soundness. What it offers is an opportunity for cancellation before the information needed for that cancellation is discarded.

The companion note, Why Nonlinear Substitution Has to Stay Local, follows that opportunity through the back-substitution pipeline and explains how the polynomial degree is kept under control.