boundlab.poly.PolyBoundGate#

class boundlab.poly.PolyBoundGate[source]#

Bases: Expr

Abstract gate bounded pointwise by a pair of linear polytopes on its child.

Represents an elementwise function \(f(x)\) whose output is constrained by

\[\lambda_\ell \odot x - 1 \;\le\; f(x) \;\le\; \lambda_u \odot x + 1,\]

where \(x\) is the child expression and \(\lambda_u, \lambda_\ell\) (upper_lam, lower_lam) are concrete tensors of the same shape as the child.

Backward propagation splits the incoming weight \(w\) by sign element-wise on its materialized Jacobian. For direction "<=":

\[w \cdot f(x) \;\le\; (w_+ \odot \lambda_u + w_- \odot \lambda_\ell)\,x + \sum_j |w_{\cdot j}|,\]

and symmetrically for ">=" with the slopes swapped and the bias negated.

Methods

`__init__`
`all_subnodes`	Return a list of all sub-expressions in the DAG rooted at this expression, in topological order.
`backward`	Perform backward-mode bound propagation through this expression.
`bound_width`	Compute the width of the bounds for this expression.
`bound_width_reasons_breakdown`	Compute the breakdown of the bound width by reason.
`center`	Compute the center of the bounds for this expression.
`diag`
`expand`
`expand_on`
`flatten`
`flip`
`gather`
`get_const`	Return the concrete tensor if self is a pure constant expression, else None.
`is_symmetric_to_0`	Return True if this expression is symmetric about zero, else False.
`lb`	Compute a lower bound for this expression.
`max_bound_width`	Compute the maximum width across all output dimensions.
`mean`
`narrow`
`permute`
`repeat`
`replace_subnode_once`	Return a new expression with the same structure but sub-expressions replaced by replace_fn.
`reshape`
`roll`
`scatter`
`simplify_ops_`	Recursively compute simplified ops for affine expressions.
`split_const`	Decompose this expression into a constant part and a zero-constant part.
`squeeze`
`sum`
`tile`
`to_string`	Return string representation with child strings substituted.
`transpose`
`ub`	Compute an upper bound for this expression.
`ublb`	Compute both an upper bound and a lower bound for this expression.
`uncertainty_reasons`	Compute the breakdown of the bound width by reason, aggregated to total contributions.
`unflatten`
`unsqueeze`
`with_children`	Return a new expression with the same type and flags but new children.
`zeros_set`

__init__(child, upper_lam, lower_lam, *, reason=None)[source]#

property shape: torch.Size#: The shape of the output(s) produced by this expression.

property children: tuple[Expr, ...]#: The child expressions that serve as inputs to this expression.

with_children(*new_children)[source]#

Return a new expression with the same type and flags but new children.

backward(weights, direction)[source]#

Perform backward-mode bound propagation through this expression.

Given an accumulated weight weights (usually a EinsumOp) from the output back to this node, backward propagation derives child weights and a bias:

\[\mathbf{w}^\top f(x_1, \ldots, x_n) \;\square\; b + \sum_i \mathbf{w}_i^\top x_i\]

Parameters:

weights (LinearOp) – A EinsumOp accumulated weight from the root expression to this node.
direction (Literal['>=', '<=', '==']) – Bound direction — ">=" (lower), "<=" (upper), or "==" (exact).

Returns:

A tuple (bias, child_weights) where bias is a torch.Tensor or 0, and child_weights is a list of EinsumOp (one per child). Returns None if this expression cannot contribute to the bound in the given direction.

to_string(child_str)[source]#

Return string representation with child strings substituted.

property T: Expr#: Convenience for transpose of the last two dimensions.

__add__(other)#

__mul__(other)#: Element-wise multiplication (no broadcast).

all_subnodes()#

Return a list of all sub-expressions in the DAG rooted at this expression, in topological order.

bound_width()#

Compute the width of the bounds for this expression.

bound_width_reasons_breakdown()#

Compute the breakdown of the bound width by reason.

center()#

Compute the center of the bounds for this expression.

diag(diagonal=0)#

expand(*sizes)#

expand_on(dim, size)#

flatten(start_dim=0, end_dim=-1)#

flip(dims)#

gather(indices, dim=0)#

get_const()#

Return the concrete tensor if self is a pure constant expression, else None.

Works for ConstVal and any AffineSum that has no symbolic children.

is_symmetric_to_0()#

Return True if this expression is symmetric about zero, else False.

lb()#

Compute a lower bound for this expression.

max_bound_width()#

Compute the maximum width across all output dimensions.

mean(dim=None, keepdim=False)#

narrow(dim, start, length)#

permute(*dims)#

repeat(*sizes)#

replace_subnode_once(replace_fn)#

Return a new expression with the same structure but sub-expressions replaced by replace_fn.

reshape(*shape)#

roll(shifts, dims)#

scatter(indices, output_shape)#

simplify_ops_()#: Recursively compute simplified ops for affine expressions.

split_const()#

Decompose this expression into a constant part and a zero-constant part.

If the expression is symmetric about zero, the constant part is zero. If the expression is a pure constant, the zero-constant part is zero.

Returns:: A tuple (non_const_part, const_part) where exactly one of the two is zero.
Return type:: tuple[Expr | 0, Expr | 0]

squeeze(dim=None)#

sum(dim=None, keepdim=False)#

tile(*sizes)#

transpose(dim0, dim1)#

ub()#

Compute an upper bound for this expression.

ublb()#

Compute both an upper bound and a lower bound for this expression.

uncertainty_reasons()#

Compute the breakdown of the bound width by reason, aggregated to total contributions.

unflatten(dim, sizes)#

unsqueeze(dim)#

zeros_set(output_shape)#

id: int#: Unique identifier for the expression, used for topological sorting.

flags: ExprFlags#: Flags indicating expression properties for optimization.