boundlab.ibp

The interval domain: centers (Bias) plus halfwidths (Noise).

A value is enclosed as

\[x \in [c - w,\; c + w] \quad\Longleftrightarrow\quad x = \mathrm{Bias}(c) + \mathrm{Noise}(w),\]

the cheapest sound abstraction: every transfer function is a couple of tensor ops. Noise components are independent — correlations are dropped, so x - x widens to \(\pm 2w\) instead of cancelling. The richer domains therefore use Bias/Noise as the concrete part they carry alongside their symbolic components, and fall back to intervals only where symbolic structure has run out.

Module Attributes

interpret

The interval interpreter.

Classes

Bias	A deterministic additive component: lb == ub == arr.
MatmulBiased	Peel the Bias centers off both operands.
MatmulNoise	Interval bound for the error-error product: \([-a, a] @ [-b, b] \subseteq \pm(a @ b)\) for \(a, b \ge 0\), with the reasons blended by mass.
MaxWithConst2Relu	max(x, y) = relu(x - y) + y when one side is constant, so max inherits whatever ReLU relaxation the domain registered.
MaxWithConstBiased	Shift the Bias center out first: max(c + i, y) = c + max(i, y - c) — exact, and strictly better than relaxing the whole value.
Noise	An independent symmetric interval \(\pm w\) with provenance.
Softmax2ExpReciprocal	Rewrite softmax as \(1 / \sum_j e^{\nu_j - \nu_i}\) over the last axis.

Modules

matmul	Interval matrix products.
max	Rewrites of max(x, const) into operations the domains already bound.
mul	Interval elementwise products, by the same component split as matmul: (c1 + e1)(c2 + e2) has three exact linear terms and one error-error term bounded by \(\pm(w_1 w_2)\).
softmax	Softmax via the DeepT shift-invariant decomposition.
elementwise	Interval transfer functions for elementwise activations.