Closed MLP Model Facts

Small rational MLP examples belong in the proof layer. The forward composition law is already proved generally by Examples.mlp_spec_forward_eq; the facts below state a deterministic backward calculation as coordinate-level Lean theorems.

@[reducible, inline]

abbrev NN.Proofs.Models.Mlp.exInDim : ℕ

Input width of the worked example: two features.

@[reducible, inline]

abbrev NN.Proofs.Models.Mlp.exHidDim : ℕ

Hidden width of the worked example: three ReLU units.

@[reducible, inline]

abbrev NN.Proofs.Models.Mlp.exOutDim : ℕ

Output width of the worked example: one scalar prediction.

def NN.Proofs.Models.Mlp.exampleHiddenWeight : TorchLean.Tensor ℚ [exHidDim, exInDim]

Hidden weight matrix, with entries chosen as small rationals.

Everything in this file is over ℚ, so the numbers below are exact and the examples at the end of the file close by simp alone. The same computation in Float would only be true up to rounding, which is the point of keeping the closed-form check separate from the runtime.

def NN.Proofs.Models.Mlp.exampleHiddenBias : TorchLean.Tensor ℚ [exHidDim]

Hidden bias of the worked example.

def NN.Proofs.Models.Mlp.exampleOutputWeight : TorchLean.Tensor ℚ [exOutDim, exHidDim]

Output weight row of the worked example. All entries are positive, so the single output unit is active and the backward pass exercises the interesting branch of reluDerivSpec.

def NN.Proofs.Models.Mlp.exampleOutputBias : TorchLean.Tensor ℚ [exOutDim]

Output bias of the worked example.

def NN.Proofs.Models.Mlp.exampleHiddenLayer : Spec.LinearSpec ℚ exInDim exHidDim

The hidden layer, packaging its weight and bias.

def NN.Proofs.Models.Mlp.exampleOutputLayer : Spec.LinearSpec ℚ exHidDim exOutDim

The output layer, packaging its weight and bias.

def NN.Proofs.Models.Mlp.exInput : TorchLean.Tensor ℚ [exInDim]

The single input vector used by every example below.

def NN.Proofs.Models.Mlp.exNet : Spec.Module.Chain ℚ (Spec.Shape.dim exInDim Spec.Shape.scalar) (Spec.Shape.dim exOutDim Spec.Shape.scalar)

The two-layer network as a Chain, built by the general mlpSpec constructor.

def NN.Proofs.Models.Mlp.exOutput : TorchLean.Tensor ℚ [exOutDim]

Output obtained by running the chain, that is, by the generic module forward pass.

def NN.Proofs.Models.Mlp.exExpected : TorchLean.Tensor ℚ [exOutDim]

The same output written out by hand: linear, ReLU, linear.

Stating both and proving them equal is the whole point. It checks that Chain.forward really does compose the layers in the order a reader would expect, rather than only that it type-checks.

def NN.Proofs.Models.Mlp.exDLdy : TorchLean.Tensor ℚ [exOutDim]

Incoming cotangent, taken to be all ones so the backward pass reads off plain derivatives.

def NN.Proofs.Models.Mlp.exGrad : TorchLean.Tensor ℚ [exHidDim, exInDim] × TorchLean.Tensor ℚ [exHidDim] × TorchLean.Tensor ℚ [exOutDim, exHidDim] × TorchLean.Tensor ℚ [exOutDim] × TorchLean.Tensor ℚ [exInDim]

Gradients from the hand-written backward pass: weight, bias and input gradients per layer.

def NN.Proofs.Models.Mlp.exDXOpspec : TorchLean.Tensor ℚ [exInDim]

Input gradient from the OpSpec backward pass, which composes per-operation adjoints instead.

def NN.Proofs.Models.Mlp.dXHand : TorchLean.Tensor ℚ [exInDim]

Input gradient projected out of exGrad, so the two routes can be compared directly.