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 (TorchLean.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.
• The IBP forward rule for ReLU; other activations use Runtime.Ops.IBP directly.
• 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, with and without ReLU phases, lives under NN.MLTheory.CROWN.Cert.AlphaCROWN and NN.MLTheory.CROWN.Cert.PhasedCROWN.

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} [TorchLean.Storage α] [Context α] {m n : ℕ} (A : TorchLean.Tensor α [m, n]) (v : TorchLean.Tensor α [n]) : TorchLean.Tensor α [m, n]

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

def NN.MLTheory.CROWN.reluRelaxSlopeVec {α : Type} [TorchLean.Storage α] {n : ℕ} (relax : TorchLean.Tensor (Runtime.Ops.ReLURelax α) [n]) : TorchLean.Tensor α [n]

Extract the slope vector from a tensor of ReLU relaxations.

def NN.MLTheory.CROWN.reluRelaxBiasVec {α : Type} [TorchLean.Storage α] {n : ℕ} (relax : TorchLean.Tensor (Runtime.Ops.ReLURelax α) [n]) : TorchLean.Tensor α [n]

Extract the bias vector from a tensor of ReLU relaxations.

Interval Bound Propagation (IBP) for the vector-shaped ReLU used by TwoLayerMLP.

This is an executable transfer function. Its soundness theorem instantiates the scalar type with ℝ.

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

def NN.MLTheory.CROWN.IBP.relu {α : Type} [TorchLean.Storage α] [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)].

structure NN.MLTheory.CROWN.TwoLayerMLP (α : Type) [TorchLean.Storage α] (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 : TorchLean.Tensor α [hidDim, inDim]

  First layer weight matrix.

• hiddenBias : TorchLean.Tensor α [hidDim]

  First layer bias vector.

• outputWeight : TorchLean.Tensor α [outDim, hidDim]

  Second layer weight matrix.

• outputBias : TorchLean.Tensor α [outDim]

  Second layer bias vector.

def NN.MLTheory.CROWN.forward {α : Type} [TorchLean.Storage α] [Context α] {inDim hidDim outDim : ℕ} (net : TwoLayerMLP α inDim hidDim outDim) (x : TorchLean.Tensor α [inDim]) : TorchLean.Tensor α [outDim]

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

def NN.MLTheory.CROWN.boundIbp {α : Type} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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. Exact backends use the two-layer algebraic formula. Rounded backends share the graph engine's directed coefficient propagation, which has no coefficient transfer for ReLU: the hidden layer is consumed through its IBP box, so the input coefficients are zero and the result is the IBP bound of the output layer. No theorem covers the rounded branch.

def NN.MLTheory.CROWN.boundAffineCrown {α : Type} [TorchLean.Storage α] [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)

Affine (CROWN/DeepPoly-style) bounds for the 2-layer ReLU MLP.

Rounded scalar backends use the same directed arithmetic as the general graph CROWN API.

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_vector_pointwise_upper_real {n : ℕ} (lo hi x : TorchLean.Tensor ℝ [n]) (hIn : { lo := lo, hi := hi }.contains x) (i : Fin n) : have li := lo.getScalar i; have ui := hi.getScalar i; have xi := x.getScalar i; 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.relaxScalar 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 : TorchLean.Tensor ℝ [m, n]) (xB : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (bB : Box ℝ (Spec.Shape.dim m Spec.Shape.scalar)) (x : TorchLean.Tensor ℝ [n]) (b : TorchLean.Tensor ℝ [m]) (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 : TorchLean.Tensor ℝ [inDim]) (hx : xB.contains x) : (boundIbp net xB).contains (forward net x)

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