Intervals: boundlab.ibp#

The idea#

The interval domain represents a value as a center plus a symmetric halfwidth:

\[ x \;\in\; [\,c - w,\; c + w\,] \qquad\Longleftrightarrow\qquad x = \underbrace{\mathrm{Bias}(c)}_{\text{exact}} + \underbrace{\mathrm{Noise}(w)}_{\text{independent}} \]

It is the cheapest domain — every operation is a couple of tensor ops — and the least precise: Noise components are independent, so correlations are lost and x - x is ±2w, not zero. In practice Bias/Noise serve two roles: a stand-alone interval analysis, and the “concrete part” that the richer domains (zonotopes, polynomials) carry alongside their symbolic components. Bias is exact under every linear primitive; Noise maps through absolute values and carries a Reasons provenance tag that blends under addition.

Handling Basic Operators#

Linear operators are exact on Bias and map Noise through absolute values (|A|·w). The monotone activations Relu, Exp, Tanh, Reciprocal (boundlab.ibp.elementwise) are exact as intervals: apply the function to both endpoints and return a fresh Bias + Noise pair — correct range, but a new interval with no memory of the input. MaxWithConst2Relu / MaxWithConstBiased (boundlab.ibp.max) rewrite max(x, c) as relu(x - c) + c, or shift a pure-bias max exactly.

Handling Mul and Matmul#

Products split over components, \((c_1 + e_1)(c_2 + e_2) = c_1 c_2 + c_1 e_2 + e_1 c_2 + e_1 e_2\): the three terms with a constant factor are exact linear maps (MulBiased, MatmulBiased), and only the error-error term needs the interval bound \([-a, a] \cdot [-b, b] \subseteq \pm(ab)\) (MulNoised, MatmulNoise).

Handling Softmax#

Softmax2ExpReciprocal (boundlab.ibp.softmax) decomposes softmax shift-invariantly as \(\sigma_i = 1 / \sum_j e^{\nu_j - \nu_i}\) — pairwise differences, exp, a reduce-sum, one reciprocal — so it reuses whichever exp and reciprocal handlers the enclosing domain registered; the richer domains all share this same handler.

interpret#

The interval interpreter is the base handlers plus everything above:

from boundlab.interp import Interpreter, base
from boundlab.ibp import MatmulBiased, MatmulNoise, MaxWithConst2Relu
from boundlab.ibp import Relu, Exp, Tanh, Reciprocal, Softmax2ExpReciprocal

interpret = Interpreter(
    *base.interpret.values(),      # shared exact operators
    MatmulBiased(), MatmulNoise(), # component-split matmul
    MaxWithConst2Relu(),
    Relu(), Exp(), Tanh(), Reciprocal(),   # endpoint-mapped activations
    Softmax2ExpReciprocal(),
)

No after_each is needed: every result is already a plain Bias + Noise pair.