Supplemental Activation Operators

This file defines additional activation functions and transfer rules intended for CROWN/IBP-style bound propagation:

• Leaky ReLU: f(x) = max(αx, x) (typically 0 < α < 1)
• ELU: f(x) = x if x > 0, else α (exp(x) - 1)
• Softplus: f(x) = log(1 + exp(x))
• Mish: f(x) = x * tanh(softplus(x))
• SiLU/Swish: f(x) = x * sigmoid(x)

Soundness status

A few helpers in this file use low-order Taylor approximations (exp_approx, log_approx, tanh_approx, sigmoid_approx). These are executable approximations, not theorem-backed enclosures of the true transcendental functions. Bounds derived from them should only be used under an explicit checker/oracle assumption, not as part of the unconditional CROWN soundness core.

If you need enclosure-sound bounds for transcendentals, prefer validated enclosure backends (e.g. Arb-backed intervals in NN/Floats) or restrict to the operator subset covered by the main soundness theorems.

References

Activations:

• ELU: Clevert, Unterthiner, Hochreiter, "Fast and Accurate Deep Network Learning by Exponential Linear Units (ELUs)", ICLR 2016: https://arxiv.org/abs/1511.07289
• Swish/SiLU: Ramachandran, Zoph, Le, "Searching for Activation Functions", 2017: https://arxiv.org/abs/1710.05941
• Mish: Misra, "Mish: A Self Regularized Non-Monotonic Activation Function", 2019: https://arxiv.org/abs/1908.08681

Bound propagation context:

• CROWN: Zhang et al., "Efficient Neural Network Robustness Certification with General Activation Functions", 2018: https://arxiv.org/abs/1811.00866
• auto_LiRPA: Xu et al., "Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond", NeurIPS 2020: https://arxiv.org/abs/2002.12920

Approximation Helpers

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

Low-order Taylor approximation of exp. This is executable, not an enclosure theorem.

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

Low-order approximation of log(1 + y) around y = 0; not an enclosure theorem.

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

Executable softplus approximation computed via logApprox (1 + expApprox x).

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

Executable sigmoid approximation computed via expApprox.

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

Low-order approximation of tanh; not an enclosure theorem.

Leaky ReLU

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

Leaky ReLU: f(x) = x if x ≥ 0, αx if x < 0.

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

IBP for Leaky ReLU on scalars.

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

IBP for Leaky ReLU on boxes.

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

Affine bounds for Leaky ReLU. Unlike ReLU, both branches are linear so relaxation is easier.

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

Derivative bounds for Leaky ReLU (for Lyapunov).

ELU (Exponential Linear Unit)

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

ELU: f(x) = x if x > 0, α(exp(x) - 1) if x ≤ 0.

def NN.MLTheory.CROWN.Operators.Activations.ibpEluScalar {α : Type} [Context α] (scale l u : α) : α × α

IBP for ELU on scalars.

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

IBP for ELU on boxes.

def NN.MLTheory.CROWN.Operators.Activations.affElu {α : Type} [Context α] (scale l u : α) : α × α × α × α

Affine bounds for ELU. Positive branch is linear, negative branch is nonlinear (exp).

def NN.MLTheory.CROWN.Operators.Activations.derivElu {α : Type} [Context α] (scale l u : α) : α × α

Derivative bounds for ELU.

Softplus

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

Softplus: f(x) = log(1 + exp(x)). Using approximation since Numbers.log may not be available.

def NN.MLTheory.CROWN.Operators.Activations.ibpSoftplusScalar {α : Type} [Context α] (l u : α) : α × α

IBP for Softplus. Softplus is monotone increasing.

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

IBP for Softplus on boxes.

SiLU/Swish

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

SiLU/Swish: f(x) = x · sigmoid(x).

def NN.MLTheory.CROWN.Operators.Activations.ibpSiluScalar {α : Type} [Context α] (l u : α) : α × α

IBP for SiLU. Not monotone, has global minimum around x ≈ -1.28.

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

IBP for SiLU on boxes.

Mish

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

Mish: f(x) = x · tanh(softplus(x)).

def NN.MLTheory.CROWN.Operators.Activations.ibpMishScalar {α : Type} [Context α] (l u : α) : α × α

IBP for Mish. Similar behavior to SiLU.

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

IBP for Mish on boxes.

theorem NN.MLTheory.CROWN.Operators.Activations.Theorems.leaky_relu_def {α : Type} [Context α] (negSlope x : α) : leakyRelu negSlope x = if x > Numbers.zero then x else negSlope * x

Leaky ReLU definition structure.

theorem NN.MLTheory.CROWN.Operators.Activations.Theorems.elu_def {α : Type} [Context α] (scale x : α) : elu scale x = if x > Numbers.zero then x else scale * (expApprox x - Numbers.one)

ELU definition structure.

theorem NN.MLTheory.CROWN.Operators.Activations.Theorems.softplus_def {α : Type} [Context α] (x : α) : softplus x = softplusApprox x

Softplus definition structure.

theorem NN.MLTheory.CROWN.Operators.Activations.Theorems.ibp_leaky_relu_scalar_pair {α : Type} [Context α] (negSlope l u : α) : ∃ (lo : α) (hi : α), ibpLeakyReluScalar negSlope l u = (lo, hi)

IBP for leaky ReLU returns a pair.

theorem NN.MLTheory.CROWN.Operators.Activations.Theorems.ibp_elu_scalar_pair {α : Type} [Context α] (scale l u : α) : ∃ (lo : α) (hi : α), ibpEluScalar scale l u = (lo, hi)

IBP for ELU returns a pair.