boundlab.zono.linearizers#

Sound affine enclosures of scalar non-linearities.

A linearizer maps elementwise input bounds \([l, u]\) to a LinearBounds \((\lambda, \mu, \beta)\) certifying

\[\lambda x + \mu - \beta \;\le\; f(x) \;\le\; \lambda x + \mu + \beta \qquad \text{for all } x \in [l, u].\]

Applying it keeps the input’s symbolic structure — x * slope + bias is a linear map — and pays only the residual \(\pm\beta\) as fresh Noise. Each linearizer below chooses \(\lambda\) to (approximately) minimize \(\beta\), which for a fixed slope is half the range of \(f(x) - \lambda x\) over \([l, u]\) (the Chebyshev center of the residual).

Functions

linearizer_fn

Wrap a bounds function (lb, ub) -> LinearBounds as the zonotope handler for op; also callable directly on bounds (and optionally an expression) for reuse by other domains.

Classes

Exp

Chord-slope enclosure of \(e^x\).

LinearBounds

A sound enclosure f(x) ∈ slope·x + bias ± error over the queried box.

MaxWithConst2Relu

max(x, c) = relu(x - c) + c when one operand is constant, so max inherits the domain's ReLU relaxation.

Reciprocal

Tangent-line enclosure of \(1/x\) on positive intervals.

Relu

Triangle relaxation of ReLU.

Tanh

Minimal-derivative enclosure of \(\tanh\) (DeepZ-style).