Transformer PyTorch Fixture Import

Transformer fixture weight import from JSON.

In the spec layer, our transformer encoder parameters are explicit tensors (query/key/value/output projections, feed-forward weights, and LayerNorm affine parameters). In PyTorch these are usually spread across multiple nn.Linear and nn.LayerNorm submodules.

For round-trip demos 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.TransformerPyTorch.generateTransformerEncoderWithWeights, such as layers.0.mha.q_proj.weight. That keeps generated export state dicts loadable by both PyTorch and this Lean importer.

structure Import.TransformerPyTorch.TransformerEncoderStateDict (embedDim headCount hiddenDim : ℕ) : Type

Typed view of a single-layer Transformer encoder state_dict (Float tensors).

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.

• Wq : Spec.Tensor Float (Spec.Shape.dim embedDim (Spec.Shape.dim embedDim Spec.Shape.scalar))

  Query projection matrix.

• Wk : Spec.Tensor Float (Spec.Shape.dim embedDim (Spec.Shape.dim embedDim Spec.Shape.scalar))

  Key projection matrix.

• Wv : Spec.Tensor Float (Spec.Shape.dim embedDim (Spec.Shape.dim embedDim Spec.Shape.scalar))

  Value projection matrix.

• Wo : Spec.Tensor Float (Spec.Shape.dim embedDim (Spec.Shape.dim embedDim Spec.Shape.scalar))

  Output projection matrix.

• W1 : Spec.Tensor Float (Spec.Shape.dim embedDim (Spec.Shape.dim hiddenDim Spec.Shape.scalar))

  Weight matrix for layer 1.

• W2 : Spec.Tensor Float (Spec.Shape.dim hiddenDim (Spec.Shape.dim embedDim Spec.Shape.scalar))

  Weight matrix for layer 2.

• b1 : Spec.Tensor Float (Spec.Shape.dim hiddenDim Spec.Shape.scalar)

  Bias for layer 1.

• b2 : Spec.Tensor Float (Spec.Shape.dim embedDim Spec.Shape.scalar)

  Bias for layer 2.

• norm1_gamma : Spec.Tensor Float (Spec.Shape.dim embedDim Spec.Shape.scalar)

  First LayerNorm scale.

• norm1_beta : Spec.Tensor Float (Spec.Shape.dim embedDim Spec.Shape.scalar)

  First LayerNorm bias.

• norm2_gamma : Spec.Tensor Float (Spec.Shape.dim embedDim Spec.Shape.scalar)

  Second LayerNorm scale.

• norm2_beta : Spec.Tensor Float (Spec.Shape.dim embedDim Spec.Shape.scalar)

  Second LayerNorm bias.

def Import.TransformerPyTorch.getTensorAny? (o : PyTorch.StateDict) (s : Spec.Shape) (keys : List String) : Option (Spec.Tensor Float s)

def Import.TransformerPyTorch.loadTransformerEncoderStateDict (embedDim headCount hiddenDim : ℕ) (j : Lean.Json) : Option (TransformerEncoderStateDict embedDim headCount hiddenDim)

Load Transformer Encoder state dict from JSON matching either supported export key format.