PINN PyTorch ParamStore Bridge

Build a CROWN-style graph parameter store from a PyTorch-trained PINN checkpoint.

The verification CLIs run PINNs through the graph backend. For that, we need a ParamStore keyed by the node ids that SequentialPINNArch.buildGraph uses. Keeping this file under NN.Verification.PINN makes the ownership clear: this is not a generic PyTorch example, it is the checkpoint bridge for PINN verification.

def Import.PINNPyTorch.Internal.layerToLinParams (layer : PinnLayer) : NN.MLTheory.CROWN.Graph.LinParams Float

Convert a PinnLayer into the graph backend's LinParams container.

The declaration remains a named helper because exported PINN graph assembly refers to it directly.

def Import.PINNPyTorch.toParamStore (sd : PinnState) : NN.MLTheory.CROWN.Graph.ParamStore Float

Build a ParamStore Float for the PINN graph from a loaded state.

def Import.PINNPyTorch.toParamStoreWith {α : Type} [Context α] (ofFloat : Float → α) (sd : PinnState) : NN.MLTheory.CROWN.Graph.ParamStore α

Convert a loaded float state dict to a ParamStore over an arbitrary scalar α.

This is useful when you want to reuse the same trained parameters for:

• executable backends (Float, IEEE32Exec), or
• proof-level backends (e.g. ℝ), by supplying an appropriate ofFloat cast.

def Import.PINNPyTorch.buildGraph (sd : PinnState) : NN.MLTheory.CROWN.Graph

Build the computation graph corresponding to a loaded state.