Why Nonlinear Substitution Has to Stay Local

If quadratic symbolic bounds can retain information that linear bounds lose, the tempting next step is to carry them through the whole network. That is also the step that breaks scalability.

The useful question is not “linear or nonlinear?” It is: how long must a nonlinear expression remain alive to capture the cancellation we care about? For TiSum, the answer is one local linear–activation pair.

Why unrestricted substitution explodes

Take a quadratic bound $q(x)$ for an activation. If the variables in $x$ are themselves replaced by quadratic expressions from the previous nonlinear layer, then terms such as $x_i x_j$ become products of quadratics. Degree two becomes degree four. Repeat the process and both degree and term count grow quickly.

Even when the network is sparse, a dense affine layer mixes variables before the next activation. Cross terms proliferate, and the verifier would have to store and bound an expanding polynomial rather than the compact symbolic form that makes bound propagation attractive.

So “use quadratic bounds everywhere” is not the method. The quadratic form has a deliberately short lifetime.

The local substitution pipeline

Start from a target linear expression

$$L(y) = c^\top y + d,$$

where $y$ contains activation outputs. For each coefficient, choose a sound quadratic lower or upper bound for the corresponding activation. Substitution produces a quadratic expression $Q(x)$ in the pre-activation variables.

Those variables came from an adjacent affine layer, $x = Wu + b$. Substitute that layer once. The result is still degree two in $u$, although it now contains square and cross terms:

$$Q(Wu+b) = u^\top A u + r^\top u + s.$$

Now stop. Soundly relax $u_i^2$ and $u_i u_j$ over their known ranges back to linear expressions. After that down-relaxation, ordinary linear back-substitution continues through earlier layers.

The flow is therefore:

$$\begin{gathered} \text{linear target} \\ \downarrow \\ \text{quadratic activation bounds} \\ \downarrow \\ \text{one affine substitution} \\ \downarrow \\ \text{linearized quadratic terms} \\ \downarrow \\ \text{linear back-substitution}. \end{gathered}$$

The nonlinear bound is applied at most once across that adjacent pair. Degree never exceeds two.

The soundness contract is pointwise

Convexity is useful when a solver must optimize an expression directly. It is not the requirement here. Let $I$ be the current interval. For a lower bound,

$$q(x) \leq \sigma(x) \quad \forall x \in I.$$

Replacing an activation with $q$ in the correct coefficient direction preserves the target inequality. Substituting the exact affine relation preserves it again. Finally, replacing each square or cross term with a valid linear bound preserves it once more. The proof is inequality transitivity, stage by stage.

This separation matters. A nonlinear symbolic bound need not be convex to be sound in substitution, because it is not left as a raw nonlinear constraint for the final solver. What must be checked is the direction and domain of every local inequality.

Where precision can still disappear

Locality controls cost; it does not promise that every quadratic detour ends tighter. Linearizing terms one by one can lose correlations among those terms, including some of the structure the quadratic activation bounds just captured. For a particular neuron, interval, or coefficient pattern, the final linear bound may equal or even underperform the ordinary linear route.

That is a precision caveat, not a soundness caveat. Every relaxation still contains the concrete behaviour. The evaluated question is whether enough useful cancellation occurs before down-relaxation to improve verification in practice.

Whether enough of that cancellation survives is therefore an empirical question for a particular network, interval, and specification. This note stops at the method and its guarantees; the public abstract records the paper’s evaluation scope and headline results.

For the failure that motivates this pipeline, read Why Linear Bounds Lose Cancellation When They Are Summed. The project page for TiSum keeps the method, scope, and research lineage in one place.