PINN PyTorch Checkpoint Loading

PINN weight import (JSON → typed tensors).

This is the “loading” half of the PINN PyTorch bridge:

• read a PyTorch-style state dictionary encoded as JSON,
• parse each weight/bias matrix into a shape-checked Tensor Float ... (shape inferred/checked),
• infer a TorchLean SequentialPINNArch from the layer shapes plus optional activation metadata.

The generic JSON helpers (loadWeights?, parseTensor, inferMatrixDims, …) live in NN/Runtime/PyTorch/Import/Core.lean.

structure Import.PINNPyTorch.PinnLayer : Type

One fully-connected layer of a PINN (weights + bias) as trained in PyTorch.

• inDim : ℕ

  Input dimension.

• outDim : ℕ

  Output dimension.

• weights : Spec.Tensor Float (Spec.Shape.dim self.outDim (Spec.Shape.dim self.inDim Spec.Shape.scalar))

  weights.

• bias : Spec.Tensor Float (Spec.Shape.dim self.outDim Spec.Shape.scalar)

  bias.

structure Import.PINNPyTorch.PinnState : Type

A parsed PINN state dict together with the inferred TorchLean sequential PINN architecture.

• arch : NN.Verification.PINN.SequentialPINNArch

  Inferred sequential fully-connected PINN architecture.

• layers : List PinnLayer

  Layer stack.

Activation metadata

Python training scripts often record which nonlinearity they used. We treat that as optional metadata under meta.activation. If it is missing (or unknown), we default to tanh.

def Import.PINNPyTorch.Internal.parseActivation (metaOpt : Option Lean.Json) : NN.Verification.PINN.HiddenActivation

Internal: parse optional activation metadata from JSON (meta.activation).

def Import.PINNPyTorch.loadPinnState (j : Lean.Json) : Option PinnState

Load a PINN state dict with arbitrary hidden widths.

Expected keys:

• layers.<i>.weight and layers.<i>.bias for each layer index i
• optional meta.activation

Unlike fixed-shape demos, we infer (outDim, inDim) for each layer from the JSON matrix shape.