Transformer PyTorch Import

Transformer weight import from JSON.

TorchLean's executable Transformer keeps query/key/value/output projections, feed-forward weights, and LayerNorm affine parameters in one shape-indexed state pack. In PyTorch these values are usually spread across several nn.Linear and nn.LayerNorm submodules.

For round-trip examples we accept a stable, explicit key format in JSON: Wq, Wk, Wv, Wo, W1, W2, b1, b2, norm1_gamma, norm1_beta, norm2_gamma, norm2_beta.

We also accept the nested PyTorch module keys emitted by Export.PyTorch.Transformer.withParameters, such as layers.0.mha.q_proj.weight. Explicit attention keys use (input, output) matrices. Nested nn.Linear projection keys use (output, input) and are transposed during import; feed-forward weights retain PyTorch's orientation under either naming scheme.

structure Import.PyTorch.Transformer.Parameters (modelWidth feedForwardWidth : ℕ) : Type

Parameters for a single-layer Transformer encoder imported from a PyTorch state_dict.

This is the normalized typed view returned by the JSON loader. The loader accepts both TorchLean's explicit keys and the nested PyTorch module keys emitted by the exporter.

• queryWeight : TorchLean.Tensor Float [modelWidth, modelWidth]

  Query projection matrix in (input, output) orientation.

• keyWeight : TorchLean.Tensor Float [modelWidth, modelWidth]

  Key projection matrix.

• valueWeight : TorchLean.Tensor Float [modelWidth, modelWidth]

  Value projection matrix.

• outputWeight : TorchLean.Tensor Float [modelWidth, modelWidth]

  Output projection matrix.

• feedForwardInputWeight : TorchLean.Tensor Float [feedForwardWidth, modelWidth]

  Input feed-forward weight in PyTorch (output, input) layout.

• feedForwardOutputWeight : TorchLean.Tensor Float [modelWidth, feedForwardWidth]

  Output feed-forward weight in PyTorch (output, input) layout.

• feedForwardInputBias : TorchLean.Tensor Float [feedForwardWidth]

  Input feed-forward projection bias.

• feedForwardOutputBias : TorchLean.Tensor Float [modelWidth]

  Output feed-forward projection bias.

• norm1Scale : TorchLean.Tensor Float [modelWidth]

  First LayerNorm scale.

• norm1Bias : TorchLean.Tensor Float [modelWidth]

  First LayerNorm bias.

• norm2Scale : TorchLean.Tensor Float [modelWidth]

  Second LayerNorm scale.

• norm2Bias : TorchLean.Tensor Float [modelWidth]

  Second LayerNorm bias.

def Import.PyTorch.Transformer.load (modelWidth feedForwardWidth : ℕ) (json : Lean.Json) : Option (Parameters modelWidth feedForwardWidth)

Load Transformer parameters from JSON matching either supported export key format.