MLP Spec Equivalence

mlp_interp_eq_spec_mlp_forward identifies the GraphSpec chain interpreter with the reference two-layer MLP: Linear → ReLU → Linear. Both receive the same weights and biases in the order (W₁, b₁, W₂, b₂).

This theorem compares pure spec evaluations. It does not assert that DAG lowering, autograd, or a native backend preserves those values.

@[reducible, inline]

abbrev NN.GraphSpec.Models.MLPParams (inputWidth hiddenWidth outputWidth : ℕ) : List Spec.Shape

Parameter ABI for the 2-layer MLP: (W₁, b₁, W₂, b₂).

theorem NN.GraphSpec.Models.mlp_interp_eq_spec_mlp_forward {α : Type} [TorchLean.Storage α] [Context α] {inputWidth hiddenWidth outputWidth : ℕ} (params : TorchLean.TensorPack α (MLPParams inputWidth hiddenWidth outputWidth)) (x : TorchLean.Tensor α [inputWidth]) : Interp.spec (mlp inputWidth hiddenWidth outputWidth) params x = match match params with | TorchLean.TensorPack.cons w1 (TorchLean.TensorPack.cons b1 (TorchLean.TensorPack.cons w2 (TorchLean.TensorPack.cons b2 TorchLean.TensorPack.nil))) => (w1, b1, w2, b2) with | (w1, b1, w2, b2) => have l1 := { weights := w1, bias := b1 }; have l2 := { weights := w2, bias := b2 }; Examples.mlpForward l1 l2 x

Theorem (GraphSpec MLP agrees with Spec reference).

Fix widths inputWidth → hiddenWidth → outputWidth. Let params be the 4-tensor parameter list (W₁, b₁, W₂, b₂) and x an input vector.

Then the GraphSpec interpreter applied to the GraphSpec MLP graph computes exactly the same tensor as the reference Examples.mlpForward from NN.Spec.Models.Mlp, after interpreting the parameter list as two LinearSpecs.

Informally, both sides compute the same explicit formula:

$$ \begin{aligned} z_1 &= W_1x+b_1,\\ a_1 &= \operatorname{ReLU}(z_1),\\ \mathrm{out} &= W_2a_1+b_2. \end{aligned} $$

where the dot/plus are the Spec.linearSpec and Activation.reluSpec operations already used by the Spec model.