Mlp

CROWN/DeepPoly-style propagation for MLPs (vector in/out) using TorchLean tensors.

This file is a compact implementation that sits on top of:

• NN.MLTheory.CROWN.Core (Box, AffineVec, and IBP.linear), and
• TorchLean’s typed tensor layer (Spec.Tensor).

What is implemented:

• Per-neuron ReLU linear relaxations derived from pre-activation bounds (ReLU.relax_scalar*).
• A basic IBP forward pass for common activations (ReLU/sigmoid/tanh/etc.).
• A 2-layer ReLU MLP wrapper MLP2 with a simple end-to-end bounding API.

Scope boundaries in this MLP-focused module:

• General computation graphs. Use NN.MLTheory.CROWN.Graph for the graph-level certificate checker and NN.MLTheory.CROWN.Proofs.GraphCrownCertSoundness for the corresponding end-to-end soundness theorem.
• Objective-dependent / backward CROWN slope optimization. The certificate infrastructure for alpha-CROWN and alpha/beta-CROWN artifacts lives under NN.MLTheory.CROWN.Cert.AlphaCROWN and NN.MLTheory.CROWN.Cert.AlphaBetaCROWN.

References:

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

PyTorch analogues:

• torch.nn.Linear: https://pytorch.org/docs/stable/generated/torch.nn.Linear.html
• torch.nn.ReLU: https://pytorch.org/docs/stable/generated/torch.nn.ReLU.html

structure NN.MLTheory.CROWN.ReLURelax (α : Type) : Type

Parameters of a scalar linear relaxation used for bounding ReLU.

Typical shape (for crossing intervals l <= 0 < u) is an upper line y <= slope * x + bias with slope ∈ [0, 1] and bias >= 0.

• slope : α

  Linear coefficient (often written α in the CROWN literature).

• bias : α

  Constant offset (often written β).

def NN.MLTheory.CROWN.ReLU.relaxScalar {α : Type} [Context α] (l u : α) : ReLURelax α

Compute a standard (upper) linear relaxation for scalar ReLU on an interval [l, u].

This matches the classic CROWN/DeepPoly choice:

• If u <= 0, ReLU is identically 0.
• If l >= 0, ReLU is the identity.
• If l < 0 < u, use the upper chord through (l, 0) and (u, u).

def NN.MLTheory.CROWN.ReLU.relaxScalarLower {α : Type} [Context α] (l u : α) : ReLURelax α

Compute a basic (lower) linear relaxation for scalar ReLU on [l, u].

For the crossing case l <= 0 < u, we choose either:

• y >= 0 (slope 0), or
• y >= x (slope 1), depending on which yields the tighter lower bound for the downstream objective.

def NN.MLTheory.CROWN.ReLU.relaxVector {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.Tensor (ReLURelax α) (Spec.Shape.dim n Spec.Shape.scalar)

Apply relax_scalar elementwise to vector bounds (lo, hi).

def NN.MLTheory.CROWN.ReLU.relaxVectorLower {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.Tensor (ReLURelax α) (Spec.Shape.dim n Spec.Shape.scalar)

Apply relax_scalar_lower elementwise to vector bounds (lo, hi).

def NN.MLTheory.CROWN.ReLU.propagateAffine {α : Type} [Context α] {inDim hidDim : ℕ} (relax : Spec.Tensor (ReLURelax α) (Spec.Shape.dim hidDim Spec.Shape.scalar)) (aff : AffineVec α inDim hidDim) : AffineVec α inDim hidDim

Propagate an affine form through ReLU using a fixed per-neuron relaxation.

This is the "forward" DeepPoly-style propagation: given an affine bound on z, we produce an affine bound on relu(z) by scaling rows and adjusting the constant term.

def NN.MLTheory.CROWN.matColScaleSpec {α : Type} [Context α] {m n : ℕ} (A : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (v : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))

Column-wise scaling of a matrix by a vector: scale each column j by v[j].

def NN.MLTheory.CROWN.matPosSpec {α : Type} [Context α] {m n : ℕ} (A : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))

Elementwise positive part of a matrix: replace negative entries by 0.

def NN.MLTheory.CROWN.matNegSpec {α : Type} [Context α] {m n : ℕ} (A : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))

Elementwise negative part of a matrix: replace positive entries by 0.

def NN.MLTheory.CROWN.reluRelaxSlopeVec {α : Type} {n : ℕ} (relax : Spec.Tensor (ReLURelax α) (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)

Extract the slope vector from a tensor of ReLU relaxations.

def NN.MLTheory.CROWN.reluRelaxBiasVec {α : Type} {n : ℕ} (relax : Spec.Tensor (ReLURelax α) (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)

Extract the bias vector from a tensor of ReLU relaxations.

Interval Bound Propagation (IBP) utilities for vector-shaped activations.

These are correctness-first helpers: they are intended to be sound for any Context α backend that implements the scalar operations used by Activation.Math.*_spec.

The linear-layer bound helper IBP.linear lives in NN.MLTheory.CROWN.Core.

def NN.MLTheory.CROWN.IBP.relu {α : Type} [Context α] {n : ℕ} (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Interval bounds for ReLU on a vector.

This is the standard elementwise interval evaluation: relu([l,u]) = [relu(l), relu(u)].

@[reducible, inline]

abbrev NN.MLTheory.CROWN.IBP.mapMinmax {α : Type} [Context α] {n : ℕ} (f : α → α) (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Re-export of the runtime-only monotone-activation IBP helper.

We keep this file compact and Mathlib-friendly for proofs, but we do not want to maintain two copies of the same computational rule. Canonical implementation lives in: NN.MLTheory.CROWN.Runtime.Ops.IBP.map_minmax.

Semantics (per component): given an interval [l,u], this returns [min(f(l), f(u)), max(f(l), f(u))] (intended for monotone f).

@[reducible, inline]

abbrev NN.MLTheory.CROWN.IBP.sigmoid {α : Type} [Context α] {n : ℕ} (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Interval bounds for sigmoid.

@[reducible, inline]

abbrev NN.MLTheory.CROWN.IBP.tanh {α : Type} [Context α] {n : ℕ} (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Interval bounds for tanh.

def NN.MLTheory.CROWN.IBP.leakyRelu {α : Type} [Context α] {n : ℕ} (αₗ : α) (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Interval bounds for leaky-ReLU.

Sound when the negative slope αₗ is nonnegative.

def NN.MLTheory.CROWN.IBP.elu {α : Type} [Context α] {n : ℕ} (alpha : α) (xB : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n Spec.Shape.scalar)

Interval bounds for ELU.

Sound for alpha > 0.

structure NN.MLTheory.CROWN.MLP2 (α : Type) (inDim hidDim outDim : ℕ) : Type

2-layer MLP payload used by this file.

Semantics: y = W2 * relu(W1 * x + b1) + b2.

PyTorch analogue: torch.nn.Sequential(Linear(inDim,hidDim), ReLU(), Linear(hidDim,outDim)).

• W1 : Spec.Tensor α (Spec.Shape.dim hidDim (Spec.Shape.dim inDim Spec.Shape.scalar))

  First layer weight matrix.

• b1 : Spec.Tensor α (Spec.Shape.dim hidDim Spec.Shape.scalar)

  First layer bias vector.

• W2 : Spec.Tensor α (Spec.Shape.dim outDim (Spec.Shape.dim hidDim Spec.Shape.scalar))

  Second layer weight matrix.

• b2 : Spec.Tensor α (Spec.Shape.dim outDim Spec.Shape.scalar)

  Second layer bias vector.

def NN.MLTheory.CROWN.forward {α : Type} [Context α] {inDim hidDim outDim : ℕ} (net : MLP2 α inDim hidDim outDim) (x : Spec.Tensor α (Spec.Shape.dim inDim Spec.Shape.scalar)) : Spec.Tensor α (Spec.Shape.dim outDim Spec.Shape.scalar)

Forward semantics for MLP2 (used to state soundness theorems).

def NN.MLTheory.CROWN.ofLinearSpecs {α : Type} {inDim hidDim outDim : ℕ} (l1 : Spec.LinearSpec α inDim hidDim) (l2 : Spec.LinearSpec α hidDim outDim) : MLP2 α inDim hidDim outDim

Build an MLP2 from two LinearSpec records.

def NN.MLTheory.CROWN.boundIbp {α : Type} [Context α] {inDim hidDim outDim : ℕ} (net : MLP2 α inDim hidDim outDim) (xB : Box α (Spec.Shape.dim inDim Spec.Shape.scalar)) : Box α (Spec.Shape.dim outDim Spec.Shape.scalar)

Compute an output interval box via pure IBP.

This is fast and always sound, but typically looser than CROWN/DeepPoly affine bounds.

def NN.MLTheory.CROWN.boundAffineCrown {α : Type} [Context α] {inDim hidDim outDim : ℕ} (net : MLP2 α inDim hidDim outDim) (xB : Box α (Spec.Shape.dim inDim Spec.Shape.scalar)) : Box α (Spec.Shape.dim outDim Spec.Shape.scalar)

Single-pass affine (CROWN/DeepPoly-style) bounds for the 2-layer ReLU MLP.

This constructs upper and lower affine forms by combining:

• pre-activation intervals from IBP,
• per-neuron ReLU relaxations, and
• sign-splitting of the second-layer weights.

Note: this is the direct MLP-specialized implementation; the graph-level engine in NN.MLTheory.CROWN.Graph is the long-term home for fully-general CROWN.

def NN.MLTheory.CROWN.boundAffine {α : Type} [Context α] {inDim hidDim outDim : ℕ} (net : MLP2 α inDim hidDim outDim) (xB : Box α (Spec.Shape.dim inDim Spec.Shape.scalar)) : Box α (Spec.Shape.dim outDim Spec.Shape.scalar)

End-to-end bound API exposed by this file.

This API returns the IBP bound (sound for all backends); bound_affine_crown is kept as a reference implementation for the 2-layer ReLU case.

Theorems inspired by CROWN (Zhang et al., 2018, arXiv:1811.00866)

We record soundness properties of the relaxations and bound propagation. Proofs below require elementary order reasoning and case splits on signs, plus properties of mat-vec interval arithmetic.

theorem NN.MLTheory.CROWN.Theorems.relu_relax_scalar_upper_real (l u x : ℝ) (hlx : l ≤ x) (hxu : x ≤ u) : have rp := ReLU.relaxScalar l u; Activation.Math.reluSpec x ≤ rp.slope * x + rp.bias

Scalar ReLU relaxation soundness over ℝ (upper bound).

If x ∈ [l, u] and rp := ReLU.relax_scalar l u, then: relu(x) <= rp.slope * x + rp.bias.

This is the standard CROWN/DeepPoly upper chord construction (arXiv:1811.00866).

theorem NN.MLTheory.CROWN.Theorems.relu_relax_vector_pointwise_upper_real {n : ℕ} (lo hi x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hIn : { lo := lo, hi := hi }.contains x) (i : Fin n) : have li := match lo, hIn with | Spec.Tensor.dim flo, hIn => match flo i with | Spec.Tensor.scalar v => v; have ui := match hi, hIn with | Spec.Tensor.dim fhi, hIn => match fhi i with | Spec.Tensor.scalar v => v; have xi := match x, hIn with | Spec.Tensor.dim fx, hIn => match fx i with | Spec.Tensor.scalar v => v; have rp := ReLU.relaxScalar li ui; Activation.Math.reluSpec xi ≤ rp.slope * xi + rp.bias

Vectorized ReLU relaxation (pointwise upper bound) over ℝ.

If x ∈ [lo, hi] and rp := ReLU.relax_vector lo hi, then for every component i we have relu(xᵢ) ≤ rpᵢ.slope * xᵢ + rpᵢ.bias.

theorem NN.MLTheory.CROWN.Theorems.ibp_linear_sound_real {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)) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (b : Spec.Tensor ℝ (Spec.Shape.dim m Spec.Shape.scalar)) (hx : xB.contains x) (hb : bB.contains b) : (IBP.linear W xB bB).contains (Spec.linearSpec { weights := W, bias := b } x)

Soundness of IBP.linear over ℝ.

If x ∈ xB and b ∈ bB, then W*x + b lies in the interval box computed by IBP.linear W xB bB.

theorem NN.MLTheory.CROWN.Theorems.bound_ibp_sound {inDim hidDim outDim : ℕ} (net : MLP2 ℝ inDim hidDim outDim) (xB : Box ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (x : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (hx : xB.contains x) : (boundIbp net xB).contains (forward net x)

Soundness of pure IBP bounds for a 2-layer MLP over ℝ.

theorem NN.MLTheory.CROWN.Theorems.bound_affine_sound {inDim hidDim outDim : ℕ} (net : MLP2 ℝ inDim hidDim outDim) (xB : Box ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (x : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (hx : xB.contains x) : (boundAffine net xB).contains (forward net x)

Soundness of the affine-bound entrypoint for a 2-layer MLP over ℝ.

In this module bound_affine delegates to the IBP implementation, so this theorem is a direct corollary of bound_ibp_sound.

def NN.MLTheory.CROWN.Examples.crownMlp2Bounds {α : Type} [Context α] {inDim hidDim outDim : ℕ} (l1 : Spec.LinearSpec α inDim hidDim) (l2 : Spec.LinearSpec α hidDim outDim) (x_center : Spec.Tensor α (Spec.Shape.dim inDim Spec.Shape.scalar)) (eps : α) : Box α (Spec.Shape.dim outDim Spec.Shape.scalar) × Box α (Spec.Shape.dim outDim Spec.Shape.scalar)

Compute both IBP bounds and affine-CROWN bounds for a 2-layer MLP around an ε-box.

The input set is the axis-aligned box centered at x_center with radius eps in each coordinate.

def NN.MLTheory.CROWN.Classify.getVec {α : Type} {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (i : Fin n) : α

Extract the scalar component t[i] from a vector-shaped tensor.

def NN.MLTheory.CROWN.Classify.lowerAt {α : Type} {n : ℕ} (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) (i : Fin n) : α

Lower endpoint at index i from a vector box.

def NN.MLTheory.CROWN.Classify.upperAt {α : Type} {n : ℕ} (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) (i : Fin n) : α

Upper endpoint at index i from a vector box.

def NN.MLTheory.CROWN.Classify.maxCompetitorUpper {α : Type} [Context α] {n : ℕ} (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) (c : Fin n) : α

Maximum upper bound among competitors k ≠ c.

def NN.MLTheory.CROWN.Classify.certifiedMargin {α : Type} [Context α] {n : ℕ} (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) (c : Fin n) : α

Certified margin lower bound: lowerAt c - maxCompetitorUpper c.

def NN.MLTheory.CROWN.Classify.isCertifiedClass {α : Type} [Context α] {n : ℕ} (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) (c : Fin n) : Bool

Decide whether class c is certified by a positive margin.

def NN.MLTheory.CROWN.Classify.argmax? {α : Type} [Context α] {n : ℕ} (y : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Option (Fin n)

Return the argmax index of a concrete output vector (when n > 0), otherwise none.

This is a utility for pairing certified bounds with a predicted class.