Leaky-ReLU Bounds

Interval, affine, and derivative transfer rules for leakyRelu negSlope x = if x > 0 then x else negSlope * x.

The formulas cover positive, zero, and negative branch slopes. In particular, when a non-positive slope crosses zero, the interval rule includes the value at the kink instead of considering only the two endpoints.

Reference: Zhang et al., "Efficient Neural Network Robustness Certification with General Activation Functions", NeurIPS 2018, arXiv:1811.00866.

def NN.MLTheory.CROWN.Operators.Activations.leakyRelu {α : Type} [Context α] (negSlope x : α) : α

Leaky ReLU with slope negSlope on the non-positive branch.

def NN.MLTheory.CROWN.Operators.Activations.min2 {α : Type} [Context α] (x y : α) : α

Minimum of two values using the executable scalar order.

def NN.MLTheory.CROWN.Operators.Activations.max2 {α : Type} [Context α] (x y : α) : α

Maximum of two values using the executable scalar order.

def NN.MLTheory.CROWN.Operators.Activations.ibpLeakyReluScalar {α : Type} [Context α] (negSlope lo hi : α) : α × α

Exact endpoint-and-kink interval propagation for scalar Leaky ReLU.

def NN.MLTheory.CROWN.Operators.Activations.ibpLeakyRelu {α : Type} [Context α] (n : ℕ) (negSlope : α) (box : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Apply ibpLeakyReluScalar coordinatewise to a vector box.

def NN.MLTheory.CROWN.Operators.Activations.affLeakyRelu {α : Type} [Context α] (negSlope lo hi : α) : α × α × α × α

Lower and upper affine forms for Leaky ReLU on [lo, hi], returned as (lowerSlope, lowerBias, upperSlope, upperBias).

For a crossing interval the function is convex when negSlope ≤ 1 and concave when negSlope > 1; the secant and branch support exchange roles accordingly.

def NN.MLTheory.CROWN.Operators.Activations.derivLeakyRelu {α : Type} [Context α] (negSlope lo hi : α) : α × α

Range of the two branch derivatives over an interval.