Sequential PINN Architecture

Sequential fully-connected PINN architecture helpers for TorchLean verification.

This module covers the PINN architecture class used by the verification pipeline: fully-connected feed-forward networks with one shared hidden activation between linear layers. That is enough for the corridor networks used by the PINN/ODE checkers, but it is not a complete taxonomy of all PINN architectures. Convolutional PINNs, residual PINNs, Fourier-feature PINNs, and multi-branch physics models should get their own architecture records rather than overloading this sequential MLP description.

inductive NN.Verification.PINN.HiddenActivation : Type

Supported hidden activation functions between linear layers.

• tanh : HiddenActivation
• relu : HiddenActivation
• sin : HiddenActivation

@[implicit_reducible]

instance NN.Verification.PINN.instDecidableEqHiddenActivation : DecidableEq HiddenActivation

@[implicit_reducible]

instance NN.Verification.PINN.instReprHiddenActivation : Repr HiddenActivation

def NN.Verification.PINN.instReprHiddenActivation.repr : HiddenActivation → ℕ → Std.Format

structure NN.Verification.PINN.SequentialPINNArch : Type

Architectural description for a sequential fully-connected PINN/corridor network.

• inputDim : ℕ

  Input dimension.

• hiddenDims : List ℕ

  Hidden layer widths, in order.

• outputDim : ℕ

  Output dimension.

• activation : HiddenActivation

  Shared hidden activation function.

def NN.Verification.PINN.instDecidableEqSequentialPINNArch.decEq (x✝ x✝¹ : SequentialPINNArch) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance NN.Verification.PINN.instDecidableEqSequentialPINNArch : DecidableEq SequentialPINNArch

def NN.Verification.PINN.instReprSequentialPINNArch.repr : SequentialPINNArch → ℕ → Std.Format

@[implicit_reducible]

instance NN.Verification.PINN.instReprSequentialPINNArch : Repr SequentialPINNArch

def NN.Verification.PINN.SequentialPINNArch.linearLayerCount (arch : SequentialPINNArch) : ℕ

Number of linear layers in the architecture.

def NN.Verification.PINN.SequentialPINNArch.linearDims (arch : SequentialPINNArch) : List (ℕ × ℕ)

Dimensions (input, output) for each linear layer, in order.

def NN.Verification.PINN.SequentialPINNArch.linearDims.go : ℕ → List ℕ → List (ℕ × ℕ)

def NN.Verification.PINN.SequentialPINNArch.linearNodeId (idx : ℕ) : ℕ

Node id assigned to the k-th linear layer (0-indexed).

def NN.Verification.PINN.SequentialPINNArch.outputNodeId (arch : SequentialPINNArch) : ℕ

Id of the terminal linear layer (network output).

def NN.Verification.PINN.SequentialPINNArch.Internal.activationOpKind : HiddenActivation → MLTheory.CROWN.Graph.OpKind

Internal: map a PINN.HiddenActivation to the corresponding NN.IR.OpKind.

def NN.Verification.PINN.SequentialPINNArch.Internal.buildNodesAux (activation : HiddenActivation) (remaining : List (ℕ × ℕ)) (prevId nextId : ℕ) (acc : Array MLTheory.CROWN.Graph.Node) : Array MLTheory.CROWN.Graph.Node

Internal: worker for buildGraph.

Implementation note: TorchLean enables the backward.privateInPublic check, so exported definitions should not depend on private helpers.

def NN.Verification.PINN.SequentialPINNArch.buildGraph (arch : SequentialPINNArch) : MLTheory.CROWN.Graph

Build a computation graph matching the supplied sequential PINN architecture.

def NN.Verification.PINN.SequentialPINNArch.graphOutputId (g : MLTheory.CROWN.Graph) : ℕ

Output node id for an arbitrary graph, assuming the last node is the network output.