boundlab.zono.relu_linearizer#

boundlab.zono.relu_linearizer(expr)[source]#

Triangle relaxation of ReLU for zonotope abstract interpretation.

For each neuron with input bounds [lb, ub]:

  • Dead (ub <= 0): output is 0, no contribution.

  • Active (lb >= 0): output equals input exactly.

  • Crossing (lb < 0 < ub): triangle relaxation with slope = ub / (ub - lb), bias = -ub * lb / (2 * (ub - lb)), error = -ub * lb / (2 * (ub - lb)).