boundlab.diff.zono3.relu_linearizer#

boundlab.diff.zono3.relu_linearizer(xs, ys, ds)[source]#

Return a DiffZonoBounds for differential ReLU.

x_bounds and y_bounds are standard triangle-relaxation zonotopes. For cases 1–8 the diff reuses the same epsilon variables as x and y, making diff_output = x_output − y_output exactly. For case 9 (both crossing) a fresh epsilon is introduced for the diff component.

Examples

Active/active regime: diff x-weight equals the relu slope (1.0):

>>> import torch
>>> import boundlab.expr as expr
>>> from boundlab.diff.zono3.default.relu import relu_linearizer
>>> x = expr.ConstVal(torch.tensor([2.0])) + 0.5 * expr.LpEpsilon([1])
>>> y = expr.ConstVal(torch.tensor([1.0])) + 0.5 * expr.LpEpsilon([1])
>>> d = x - y
>>> dzb = relu_linearizer(x, y, d)
>>> dzb.x_bounds.input_weights[0].item()
1.0

Crossing/crossing regime is still sound for relu(x) - relu(y):

>>> x = expr.ConstVal(torch.tensor([0.0])) + 0.8 * expr.LpEpsilon([1])
>>> y = expr.ConstVal(torch.tensor([0.1])) + 0.8 * expr.LpEpsilon([1])
>>> d = x - y
>>> dzb = relu_linearizer(x, y, d)
>>> dzb.diff_bounds.bias.shape
torch.Size([1])