Verified Neural Network Propagation

This file defines neural network layers and provides verified interval propagation, enabling robustness verification for neural networks.

Main definitions

• Layer - A dense layer with weights and bias
• forwardInterval - Interval propagation through a layer
• forwardReal - Real-valued forward pass

Main theorems

• mem_layerForwardInterval - Soundness of single layer propagation

Design Notes

We keep the network definition simple by using lists. Dimension compatibility is checked at runtime and encoded in theorem hypotheses. This avoids complex dependent types while still providing verified soundness.

structure LeanCert.ML.Layer : Type

A dense layer: y = ReLU(W·x + b) weights is a list of rows, each row has inputDim elements bias has outputDim elements (= number of rows in weights)

• weights : List (List ℚ)

  Weight matrix (outputDim × inputDim), stored as list of rows

• bias : List ℚ

  Bias vector (outputDim elements)

def LeanCert.ML.instReprLayer.repr : Layer → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.ML.instReprLayer : Repr Layer

Equations

• LeanCert.ML.instReprLayer = { reprPrec := LeanCert.ML.instReprLayer.repr }

def LeanCert.ML.Layer.inputDim (l : Layer) : ℕ

Input dimension (number of columns in weight matrix)

Equations

• l.inputDim = match l.weights with | [] => 0 | row :: tail => row.length

def LeanCert.ML.Layer.outputDim (l : Layer) : ℕ

Output dimension (number of rows in weight matrix)

Equations

• l.outputDim = l.weights.length

def LeanCert.ML.Layer.WellFormed (l : Layer) : Prop

A layer is well-formed if all rows have the same length and bias matches output

Equations

• l.WellFormed = ((∀ row ∈ l.weights, row.length = l.inputDim) ∧ l.bias.length = l.outputDim)

def LeanCert.ML.Layer.forwardReal (l : Layer) (x : List ℝ) : List ℝ

Forward pass through a layer (real values): y = ReLU(W·x + b)

Equations

• l.forwardReal x = List.map (fun (y : ℝ) => max 0 y) (LeanCert.Engine.IntervalVector.realAddBias (LeanCert.Engine.IntervalVector.realMatVecMul l.weights x) l.bias)

def LeanCert.ML.Layer.forwardInterval (l : Layer) (x : IntervalVector) (prec : ℤ := -53) : IntervalVector

Forward pass through a layer (interval arithmetic)

Equations

• l.forwardInterval x prec = LeanCert.ML.IntervalVector.reluVector ((LeanCert.Engine.IntervalVector.matVecMul l.weights x prec).addBias l.bias prec)

theorem LeanCert.ML.Layer.forwardReal_length (l : Layer) (x : List ℝ) : (l.forwardReal x).length = min l.outputDim l.bias.length

Length of real forward pass output

theorem LeanCert.ML.Layer.forwardInterval_length (l : Layer) (x : IntervalVector) (prec : ℤ) : List.length (l.forwardInterval x prec) = min l.outputDim l.bias.length

Length of interval forward pass output

theorem LeanCert.ML.Layer.mem_forwardInterval {l : Layer} {xs : List ℝ} {Is : IntervalVector} (hwf : l.WellFormed) (hdim : l.inputDim = List.length Is) (hxlen : xs.length = List.length Is) (hmem : ∀ (i : ℕ) (hi : i < List.length Is), xs[i] ∈ Is[i]) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) (i : ℕ) (hi : i < min l.outputDim l.bias.length) : (l.forwardReal xs)[i] ∈ (l.forwardInterval Is prec)[i]

Soundness of layer forward pass. If x ∈ I (component-wise), then forwardReal(x) ∈ forwardInterval(I).

structure LeanCert.ML.TwoLayerNet : Type

A two-layer network for simple examples

• layer1 : Layer
• layer2 : Layer

def LeanCert.ML.TwoLayerNet.forwardReal (net : TwoLayerNet) (x : List ℝ) : List ℝ

Forward pass through two layers

Equations

• net.forwardReal x = net.layer2.forwardReal (net.layer1.forwardReal x)

def LeanCert.ML.TwoLayerNet.forwardInterval (net : TwoLayerNet) (x : IntervalVector) (prec : ℤ := -53) : IntervalVector

Interval forward pass through two layers

Equations

• net.forwardInterval x prec = net.layer2.forwardInterval (net.layer1.forwardInterval x prec) prec

def LeanCert.ML.TwoLayerNet.WellFormed (net : TwoLayerNet) : Prop

Network is well-formed if layers are well-formed and dimensions match

Equations

• net.WellFormed = (net.layer1.WellFormed ∧ net.layer2.WellFormed ∧ net.layer2.inputDim = min net.layer1.outputDim net.layer1.bias.length)

theorem LeanCert.ML.TwoLayerNet.mem_forwardInterval {net : TwoLayerNet} {xs : List ℝ} {Is : IntervalVector} (hwf : net.WellFormed) (hdim : net.layer1.inputDim = List.length Is) (hxlen : xs.length = List.length Is) (hmem : ∀ (i : ℕ) (hi : i < List.length Is), xs[i] ∈ Is[i]) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) (i : ℕ) (hi : i < min net.layer2.outputDim net.layer2.bias.length) : (net.forwardReal xs)[i] ∈ (net.forwardInterval Is prec)[i]

Soundness theorem for two-layer network