boundlab.expr#

Symbolic Expression Framework for Bound Propagation

This module provides the foundational expression classes and operators for constructing and manipulating symbolic representations of neural network computations in BoundLab. These expressions serve as the basis for computing sound over-approximations of reachable sets through bound propagation.

Consider a zonotope, a commonly used abstract domain for neural network verification, expressed in the canonical form:

\[Z = c + \mathbf{G} \boldsymbol{\epsilon}, \quad \boldsymbol{\epsilon} \in [-1, 1]^m\]

where \(c \in \mathbb{R}^n\) denotes the center, \(\mathbf{G} \in \mathbb{R}^{n \times m}\) is the generator matrix, and \(\boldsymbol{\epsilon}\) represents the noise symbols.

A key feature of this framework is structural sharing: multiple expressions may reference the same subexpression. When two zonotopes \(Z_1\) and \(Z_2\) share common error terms, the framework preserves these dependencies, enabling tighter bound computation through correlation tracking.

The module implements backward-mode bound propagation, which computes linear relaxations by propagating weight matrices from outputs to inputs.

Examples

Build center + epsilon and query bounds:

>>> import torch
>>> import boundlab.expr as expr
>>> x = expr.ConstVal(torch.tensor([0.5, -1.0])) + expr.LpEpsilon([2])
>>> ub, lb = x.ublb()
>>> torch.allclose(ub, torch.tensor([1.5, 0.0]))
True
>>> torch.allclose(lb, torch.tensor([-0.5, -2.0]))
True

Functions

`expr_pretty_print`	Pretty print an expression in SSA form.
`Add`	Construct an affine sum with unit coefficients.

Classes

`Expr`	Abstract base class for all symbolic expressions in BoundLab.
`ExprFlags`	Flags indicating expression properties for optimization.
`ConstVal`	Expression representing a constant tensor value.
`AffineSum`	An expression representing a sum of linear operations applied to children.
`LpEpsilon`	A noise symbol bounded by the \(\ell_p\)-norm constraint.
`Cat`	Expression for concatenating child expressions along a dimension.
`Stack`	Expression for stacking child expressions along a new dimension.