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 : TorchLean.Tensor Float [self.outDim, self.inDim]

  Layer weight matrix, shaped as PyTorch stores Linear.weight.

• bias : TorchLean.Tensor Float [self.outDim]

  Layer bias vector.

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 : Array 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 we default to tanh; an unrecognized value rejects the checkpoint instead of silently bounding it as a tanh network.

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

Parse optional activation metadata from JSON (meta.activation).

An absent meta object or activation field selects tanh. A present value must name a supported nonlinearity (tanh, relu, or sin/sine/siren); anything else fails the load.

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 (see Internal.parseActivation; unsupported values reject)

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