MLP PyTorch Reference Import

MLP reference weight import from a PyTorch-style state_dict.

On the Python side we usually write JSON (nested lists of floats) under keys that mirror the names you would see in model.state_dict():

• fc1.weight, fc1.bias, fc2.weight, fc2.bias for a hand-written nn.Module with fc1/fc2,
• or layers.0.weight, layers.0.bias, ... if the model was built from an nn.Sequential.

This file keeps the parsing logic in one place so the rest of the codebase can talk in terms of typed Lean tensors.

structure Import.PyTorch.MLP.Parameters (inputWidth hiddenWidth outputWidth : ℕ) : Type

Parameters for a two-layer MLP imported from a PyTorch state_dict.

We keep the tensors as Float because these importers are meant for runtime examples: train in Python, export to JSON, then run/verify in TorchLean.

• inputWeight : TorchLean.Tensor Float [hiddenWidth, inputWidth]

  First linear layer weight, PyTorch shape (hidden, input).

• inputBias : TorchLean.Tensor Float [hiddenWidth]

  First linear layer bias.

• outputWeight : TorchLean.Tensor Float [outputWidth, hiddenWidth]

  Second linear layer weight, PyTorch shape (output, hidden).

• outputBias : TorchLean.Tensor Float [outputWidth]

  Second linear layer bias.

def Import.PyTorch.MLP.load (inputWidth hiddenWidth outputWidth : ℕ) (json : Lean.Json) : Option (Parameters inputWidth hiddenWidth outputWidth)

Load MLP parameters from JSON using either supported PyTorch key convention.

def Import.PyTorch.MLP.forward {inputWidth hiddenWidth outputWidth : ℕ} (parameters : Parameters inputWidth hiddenWidth outputWidth) (input : TorchLean.Tensor Float [inputWidth]) : TorchLean.Tensor Float [outputWidth]

Run the imported two-layer MLP.