α-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

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

@[implicit_reducible]

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

@[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 with respect to $\alpha$.

For the ReLU lower bound $y=\alpha x$, the derivative is $\partial\,\mathrm{bound}/\partial\alpha=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.

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