α-CROWN configuration

This file defines data structures for (\alpha)-optimized CROWN bounds (as in (\alpha)-CROWN / auto_LiRPA): per-neuron relaxation parameters that can be tuned externally to tighten affine relaxations.

This module is optional for the core bound-propagation development; it is grouped under NN/MLTheory/CROWN/Extras/ to keep the main entrypoints smaller.

The design mirrors the practical α-CROWN workflow: Lean stores the relaxation parameters and the resulting transfer functions, while a separate optimizer may tune those parameters before a certificate is replayed.

References:

• Zhang et al., "Efficient Neural Network Robustness Certification with General Activation Functions" (CROWN), NeurIPS 2018.
• Xu et al., "Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond" (auto_LiRPA), NeurIPS 2020.
• Xu et al., "Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers" (α/β-CROWN), ICLR 2021.

structure NN.MLTheory.CROWN.alpha.NeuronAlpha (α : Type) : Type

Per-neuron optimizable alpha parameters.

• lower : α

  Lower-envelope α parameter. For ReLU this is the candidate lower slope.

• upper : α

  Upper-envelope α parameter, used by smooth relaxations that interpolate upper candidates.

structure NN.MLTheory.CROWN.alpha.LayerAlpha (α : Type) [Context α] : Type

Layer-wise alpha configuration.

• dim : ℕ

  Number of neurons in this activation layer.

• alphas : Spec.Tensor (NeuronAlpha α) (Spec.Shape.dim self.dim Spec.Shape.scalar)

  Per-neuron α parameters, indexed by the layer dimension.

structure NN.MLTheory.CROWN.alpha.NetworkAlpha (α : Type) [Context α] : Type

Full network alpha configuration.

• numLayers : ℕ

  Number of activation layers (not counting input/output)

• layers : Array (LayerAlpha α)

  Per-layer alpha values

inductive NN.MLTheory.CROWN.alpha.NeuronStatus : Type

Neuron status based on pre-activation bounds.

• inactive : NeuronStatus
• active : NeuronStatus
• crossing : NeuronStatus
• unknown : NeuronStatus

@[implicit_reducible]

instance NN.MLTheory.CROWN.alpha.instReprNeuronStatus : Repr NeuronStatus

def NN.MLTheory.CROWN.alpha.instReprNeuronStatus.repr : NeuronStatus → ℕ → Std.Format

@[implicit_reducible]

instance NN.MLTheory.CROWN.alpha.instBEqNeuronStatus : BEq NeuronStatus

def NN.MLTheory.CROWN.alpha.instBEqNeuronStatus.beq : NeuronStatus → NeuronStatus → Bool

def NN.MLTheory.CROWN.alpha.neuronStatus {α : Type} [Context α] (l u : α) : NeuronStatus

Determine neuron status from bounds.

def NN.MLTheory.CROWN.alpha.defaultReLUAlpha {α : Type} [Context α] : NeuronAlpha α

Initialize alpha for a crossing ReLU neuron.

The default lower slope is 0, the conservative lower envelope y ≥ 0.

def NN.MLTheory.CROWN.alpha.activeAlpha {α : Type} [Context α] : NeuronAlpha α

Initialize alpha for active neuron (no relaxation needed).

def NN.MLTheory.CROWN.alpha.inactiveAlpha {α : Type} [Context α] : NeuronAlpha α

Initialize alpha for inactive neuron.

def NN.MLTheory.CROWN.alpha.initAlpha {α : Type} [Context α] (l u : α) : NeuronAlpha α

Initialize alpha based on pre-activation bounds [l, u].

def NN.MLTheory.CROWN.alpha.initLayerAlpha {α : Type} [Context α] (n : ℕ) (preB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : LayerAlpha α

Initialize layer alpha from pre-activation bounds box.

def NN.MLTheory.CROWN.alpha.projectReLUAlpha {α : Type} [Context α] (a : NeuronAlpha α) : NeuronAlpha α

Project alpha to valid range [0, 1] for ReLU.

def NN.MLTheory.CROWN.alpha.reluLowerWithAlpha {α : Type} [Context α] (_l _u alphaLo : α) : α × α

Compute a ReLU lower-envelope candidate using an optimized alpha.

For a crossing neuron with bounds [l, u], the candidate is y = α * x. A sound replay theorem should pair this executable rule with the usual α-range condition for the chosen scalar backend.

def NN.MLTheory.CROWN.alpha.reluUpperFixed {α : Type} [Context α] (l u : α) : α × α

Compute the fixed triangular ReLU upper bound.

The line is y = (u/(u-l)) * x - (u*l)/(u-l) for a crossing interval [l,u].

def NN.MLTheory.CROWN.alpha.reluWithAlpha {α : Type} [Context α] (l u : α) (alphas : NeuronAlpha α) : α × α × α × α

Apply alpha-parameterized ReLU relaxation to get affine bounds. Returns (slope_lo, bias_lo, slope_hi, bias_hi).

structure NN.MLTheory.CROWN.alpha.AlphaGradient (α : Type) : Type

Gradient of output bounds w.r.t. alpha (for optimization). For ReLU: ∂bound/∂α = x for lower bound (where y = αx).

• grad_lower : α

  Gradient for lower alpha

• grad_upper : α

  Gradient for upper alpha

structure NN.MLTheory.CROWN.alpha.LayerAlphaGrad (α : Type) [Context α] : Type

Layer-wise alpha gradients.

• dim : ℕ

  Number of neurons in the activation layer.

• grads : Spec.Tensor (AlphaGradient α) (Spec.Shape.dim self.dim Spec.Shape.scalar)

  Per-neuron gradients of the bound objective with respect to α parameters.

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

Local sigmoid approximation: σ(x) = 1 / (1 + exp(-x)) Using polynomial approximation for the Context typeclass.

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

Local tanh approximation: tanh(x) = (exp(x) - exp(-x)) / (exp(x) + exp(-x))

def NN.MLTheory.CROWN.alpha.sigmoidWithAlpha {α : Type} [Context α] (l u : α) (alphas : NeuronAlpha α) : α × α × α × α

Sigmoid relaxation with interpolation alpha. α ∈ [0,1] interpolates between tangent and secant for lower/upper.

def NN.MLTheory.CROWN.alpha.tanhWithAlpha {α : Type} [Context α] (l u : α) (alphas : NeuronAlpha α) : α × α × α × α

Tanh relaxation with interpolation alpha.

structure NN.MLTheory.CROWN.alpha.AlphaOptConfig : Type

Configuration for alpha optimization.

• learningRate : Float

  Learning rate for alpha updates

• numIterations : ℕ

  Number of optimization iterations

• optimizeLower : Bool

  Whether to optimize lower alphas

• optimizeUpper : Bool

  Whether to optimize upper alphas (for smooth activations)

structure NN.MLTheory.CROWN.alpha.OptimizedAlpha (α : Type) [Context α] : Type

Result of alpha optimization.

• alphas : NetworkAlpha α

  Optimized network alpha configuration

• finalBound : α

  Final bound achieved

• iterations : ℕ

  Number of iterations used

theorem NN.MLTheory.CROWN.alpha.Theorems.relu_lower_alpha_zero {α : Type} [Context α] (l u : α) : match reluLowerWithAlpha l u Numbers.zero with | (slope, bias) => slope = Numbers.zero ∧ bias = Numbers.zero

ReLU lower with alpha=0 gives zero slope.

theorem NN.MLTheory.CROWN.alpha.Theorems.relu_lower_alpha_one {α : Type} [Context α] (l u : α) : match reluLowerWithAlpha l u Numbers.one with | (slope, snd) => slope = Numbers.one

ReLU lower with alpha=1 gives unit slope.

theorem NN.MLTheory.CROWN.alpha.Theorems.default_relu_alpha_lower {α : Type} [Context α] : defaultReLUAlpha.lower = Numbers.zero

Default ReLU alpha has zero lower slope.

theorem NN.MLTheory.CROWN.alpha.Theorems.default_relu_alpha_upper {α : Type} [Context α] : defaultReLUAlpha.upper = Numbers.one

Default ReLU alpha has unit upper value.

theorem NN.MLTheory.CROWN.alpha.Theorems.active_alpha_unit {α : Type} [Context α] : activeAlpha.lower = Numbers.one ∧ activeAlpha.upper = Numbers.one

Active alpha has unit slope for both.

theorem NN.MLTheory.CROWN.alpha.Theorems.inactive_alpha_zero {α : Type} [Context α] : inactiveAlpha.lower = Numbers.zero ∧ inactiveAlpha.upper = Numbers.zero

Inactive alpha has zero slope for both.

theorem NN.MLTheory.CROWN.alpha.Theorems.init_layer_alpha_dim {α : Type} [Context α] (n : ℕ) (preB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : (initLayerAlpha n preB).dim = n

Init layer alpha preserves dimension.