TiSum: Local Nonlinear Substitution for Bounding Activation Functions

The problem

Bound propagation usually replaces each nonlinear activation with linear symbolic bounds. Those bounds are individually sound and cheap to substitute through the network, but their errors accumulate when the verifier later sums several neuron bounds. In particular, linearization can discard cancellation between terms that depend on the same earlier variables.

This is a different pressure point from WraLU and WraAct. Those works tighten the region used to approximate an activation or a group of activations. TiSum asks what symbolic form should be carried during back-substitution so that useful nonlinear variation is not erased immediately.

The observation

A quadratic symbolic bound can retain squares and cross terms that a linear bound cannot express. When several activation bounds are combined, those terms preserve dependencies and cancellations that would otherwise be replaced by independent worst cases.

The paper instantiates this idea as Tightening Sum (TiSum). It constructs quadratic bounds for activation functions including ReLU, Sigmoid, Tanh, and MaxPool, and uses them when back-substituting a target expression.

Why the substitution is local

Naively composing polynomial bounds across many nonlinear layers makes the degree and number of terms grow quickly. TiSum therefore keeps the nonlinear step local:

1. replace the relevant activation terms with sound quadratic symbolic bounds;
2. substitute those bounds through one adjacent affine layer;
3. soundly relax the resulting square and cross terms back to linear expressions;
4. continue with ordinary linear back-substitution.

The quadratic form is used long enough to capture a local cancellation, then discarded before it becomes an unmanageable global polynomial.

Soundness and scope

The contract is pointwise: each nonlinear symbolic expression must bound the activation over the stated input interval. Substitution then preserves the inequality by transitivity, and the later linearization must also over-approximate the quadratic terms. The nonlinear bounds do not need to be convex because the method does not hand the raw polynomial to a convex solver.

Local nonlinear substitution is not guaranteed to improve every final bound. A later term-wise linearization can erase some or all of the quadratic advantage. The soundness claim survives that loss; the tightness gain depends on the network, the interval, and the expression being bounded.