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 using the canonical Runtime.Ops.ReLU.relaxScalar and Runtime.Ops.ReLU.relaxScalarLower definitions.
• IBP forward rules for ReLU, sigmoid, tanh, and Leaky ReLU.
• A two-layer ReLU MLP wrapper TwoLayerMLP 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

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].

@[reducible, inline]

abbrev 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.

@[reducible, inline]

abbrev 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 (Runtime.Ops.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 (Runtime.Ops.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 executable transfer functions. Their soundness theorems instantiate the scalar type with ℝ and use the corresponding monotonicity or activation-specific proof.

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, including the zero kink on crossing intervals.

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

Two-layer MLP payload used by this file.

Semantics: y = outputWeight * relu(hiddenWeight * x + hiddenBias) + outputBias.

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

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

  First layer weight matrix.

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

  First layer bias vector.

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

  Second layer weight matrix.

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

  Second layer bias vector.

def NN.MLTheory.CROWN.forward {α : Type} [Context α] {inDim hidDim outDim : ℕ} (net : TwoLayerMLP α 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 TwoLayerMLP (used to state soundness theorems).

def NN.MLTheory.CROWN.ofLinearSpecs {α : Type} {inDim hidDim outDim : ℕ} (hiddenLayer : Spec.LinearSpec α inDim hidDim) (outputLayer : Spec.LinearSpec α hidDim outDim) : TwoLayerMLP α inDim hidDim outDim

Build a TwoLayerMLP from two LinearSpec records.

def NN.MLTheory.CROWN.boundIbp {α : Type} [Context α] {inDim hidDim outDim : ℕ} [BoundOps α] (net : TwoLayerMLP α 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, when BoundOps α supplies sound outward endpoint operations, typically looser than CROWN/DeepPoly affine bounds.

def NN.MLTheory.CROWN.affineCrownForms {α : Type} [Context α] {inDim hidDim outDim : ℕ} [BoundOps α] (net : TwoLayerMLP α inDim hidDim outDim) (xB : Box α (Spec.Shape.dim inDim Spec.Shape.scalar)) : AffineVec α inDim outDim × AffineVec α inDim outDim

The lower and upper affine CROWN forms for this two-layer ReLU MLP.

The returned pair is (lower, upper). boundAffineCrown evaluates these forms on the input box and takes the lower and upper endpoints.

def NN.MLTheory.CROWN.boundAffineCrown {α : Type} [Context α] {inDim hidDim outDim : ℕ} [BoundOps α] (net : TwoLayerMLP α 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 path is only the direct two-layer MLP version. The graph-level code is still the general CROWN API.

def NN.MLTheory.CROWN.boundAffine {α : Type} [Context α] {inDim hidDim outDim : ℕ} [BoundOps α] (net : TwoLayerMLP α 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. Its enclosure guarantee depends on the selected BoundOps implementation; boundAffineCrown is the direct two-layer ReLU affine implementation.

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 := Runtime.Ops.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 := Runtime.Ops.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 : TwoLayerMLP ℝ 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 : TwoLayerMLP ℝ 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 wrapper 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.crownTwoLayerMlpBounds {α : Type} [Context α] {inDim hidDim outDim : ℕ} [BoundOps α] (hiddenLayer : Spec.LinearSpec α inDim hidDim) (outputLayer : 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 two-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.