Sign-splitting linear bounds (IBP helper) #
For a linear layer y = W x + b with input interval x ∈ [lo, hi],
we can compute output bounds using the standard sign-splitting trick:
W⁺ = max(W, 0)(elementwise)W⁻ = min(W, 0)(elementwise)
Then:
y_lo = W⁺·lo + W⁻·hi + b_loy_hi = W⁺·hi + W⁻·lo + b_hi
This is algebraically equivalent to the per-weight min/max rule, but it makes it
easy to cache W⁺/W⁻ and matches the common LiRPA/CROWN implementation style.
def
NN.MLTheory.CROWN.IBP.matPos
{α : Type}
[Context α]
{m n : ℕ}
(W : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
:
Positive part of a weight matrix: W⁺ = max(W, 0) (elementwise).
Instances For
def
NN.MLTheory.CROWN.IBP.matNeg
{α : Type}
[Context α]
{m n : ℕ}
(W : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
:
Negative part of a weight matrix: W⁻ = min(W, 0) (elementwise).
Instances For
def
NN.MLTheory.CROWN.IBP.linearSignSplit
{α : Type}
[Context α]
{m n : ℕ}
(W : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(xB : Box α (Spec.Shape.dim n Spec.Shape.scalar))
(bB : Box α (Spec.Shape.dim m Spec.Shape.scalar))
:
Linear IBP bounds computed via sign-splitting (W⁺/W⁻).