MLP Spec Equivalence

This is the first model-level alignment theorem for GraphSpec.

We prove that interpreting the GraphSpec MLP architecture (NN.GraphSpec.Models.mlp) via the GraphSpec Spec-interpreter (NN.GraphSpec.Interp.spec) agrees with the existing hand-written Spec reference implementation (NN.Spec.Models.Mlp.Examples.mlp_forward), after packaging the typed parameter list into two LinearSpecs in the obvious way.

Why this matters:

• It proves that Primitive.linear and sequential composition (>>>) compute the intended Spec formula for a concrete model.
• It gives a template for additional equivalence proofs where we compare a GraphSpec architecture to an existing hand-written Spec reference implementation.
• It anchors the intended meaning of the parameter ABI for the sequential DSL: when you compose graphs with >>>, the type-level parameter list concatenates, so each model has a canonical “parameter order” that refactors can be checked against.

Related context (informal pointers):

• Many projects formalize neural-network semantics in a proof assistant, but the combination of (1) a typed architecture DSL, (2) a pure “Spec” semantics, and (3) a compilation path to an executable runtime is still relatively uncommon.
• For comparison, see e.g.:
  • Brucker & Stell (2025), “Formalizing Neural Networks” (Isabelle/HOL; relates two network representations and supports importing models from TensorFlow.js),
  • Aleksandrov & Völlinger (2023), “Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq” (formal layer semantics for verification).

@[reducible, inline]

abbrev NN.GraphSpec.Models.MLPParams (inDim hidDim outDim : ℕ) : List Shape

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

theorem NN.GraphSpec.Models.mlp_interp_eq_spec_mlp_forward {α : Type} [Context α] {inDim hidDim outDim : ℕ} (params : Runtime.Autograd.Torch.TList α (MLPParams inDim hidDim outDim)) (x : Tensor.Tensor α (Tensor.Shape.Vec inDim)) : Interp.spec (mlp inDim hidDim outDim) params x = match match params with | Proofs.Autograd.Algebra.TList.cons w1 (Proofs.Autograd.Algebra.TList.cons b1 (Proofs.Autograd.Algebra.TList.cons w2 (Proofs.Autograd.Algebra.TList.cons b2 Proofs.Autograd.Algebra.TList.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 dimensions inDim → hidDim → outDim. 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.mlp_forward from NN.Spec.Models.Mlp, after interpreting the parameter list as two LinearSpecs.

Informally, both sides compute the same explicit formula:

z₁ = W₁ · x + b₁
a₁ = relu(z₁)
out = W₂ · a₁ + b₂

where the dot/plus are the Spec.linear_spec and Activation.relu_spec operations already used by the Spec model.