PINN Core

PINN helper library: reference graphs, seeding, and certificate parsing.

This module is shared by the PINN verification workflows. It provides:

• small CROWN graphs for a tanh MLP (1D and 2D inputs),
• deterministic parameters and input-box seeding helpers,
• a few interval/finite-difference residual helpers,
• JSON parsing for the certificate schema used by the surrounding examples.

Run the curated entrypoints instead of importing this file directly:

• lake exe verify -- pinn-cert [NN/Examples/Verification/PINN/pinn_cert.json]
• lake exe verify -- pinn-dataset-check --dataset=PATH.json [--weights=WEIGHTS.json]

References:

• PINNs (physics-informed neural nets): https://arxiv.org/abs/1711.10561
• CROWN (linear bound propagation): https://arxiv.org/abs/1811.00866
• IBP (interval bound propagation): https://arxiv.org/abs/1810.12715

def NN.Verification.PINN.expectFieldObjE (ctx key : String) (j : Lean.Json) : Except String (Std.TreeMap.Raw String Lean.Json compare)

Require a JSON object field in an Except parser.

def NN.Verification.PINN.expectFieldArrayE (ctx key : String) (j : Lean.Json) : Except String (Array Lean.Json)

Require a JSON array field in an Except parser.

def NN.Verification.PINN.expectFieldFloatArrayE (ctx key : String) (j : Lean.Json) : Except String (Array Float)

Require a float-array field.

def NN.Verification.PINN.expectIntervalPairE (ctx : String) (j : Lean.Json) : Except String (Float × Float)

Require an interval object { "lo": ..., "hi": ... }.

def NN.Verification.PINN.expectIntervalPairArrayE (ctx : String) (j : Lean.Json) (expected : ℕ) : Except String (List (Float × Float))

Require an array of interval pairs with an expected length.

def NN.Verification.PINN.expectUBoundsEntryE (ctx : String) (j : Lean.Json) : Except String (Float × (Float × Float) × (Float × Float) × Float × Float)

Require one finite-difference u_bounds entry.

structure NN.Verification.PINN.PinnCfg : Type

Configuration parsed from a PINN certificate JSON.

• pde : String

  PDE identifier carried by the certificate.

• h : Float

  Grid spacing used by the exported finite-difference residual.

• eps : Float

  Input perturbation radius for interval checking.

• nPts : ℕ

  Number of sample points encoded in pts.

• pts : Spec.Tensor Float (Spec.Shape.dim self.nPts Spec.Shape.scalar)

  Sample points as a length-nPts 1D tensor.

  PyTorch analogue: this is the torch.Tensor you would keep in memory after loading a JSON/CSV list of sample coordinates.

def NN.Verification.PINN.approxEq (x y : Float) (tol : Float := 1e-5) : Bool

Approximate equality for Float used by certificate consistency checks.

def NN.Verification.PINN.buildGraph : MLTheory.CROWN.Graph

Reference tanh-MLP graph for u : R -> R used by the compact PINN certificate workflow.

def NN.Verification.PINN.buildGraph2D : MLTheory.CROWN.Graph

Same reference architecture as buildGraph, but with a 2D input u : R^2 -> R.

def NN.Verification.PINN.seedParamsFloat : MLTheory.CROWN.Graph.ParamStore Float

Deterministic weights matching the exporter convention (1D input).

def NN.Verification.PINN.seedParamsFloat2D : MLTheory.CROWN.Graph.ParamStore Float

Deterministic weights for the 2D variant buildGraph2D.

def NN.Verification.PINN.seedInputFloat (ps : MLTheory.CROWN.Graph.ParamStore Float) (x eps : Float) : MLTheory.CROWN.Graph.ParamStore Float

Seed a 1D input box $[x-\varepsilon,x+\varepsilon]$ at node id 0.

def NN.Verification.PINN.seedInputFloat2D (ps : MLTheory.CROWN.Graph.ParamStore Float) (x y eps : Float) : MLTheory.CROWN.Graph.ParamStore Float

Seed a 2D input box $[(x,y)-(\varepsilon,\varepsilon),(x,y)+(\varepsilon,\varepsilon)]$ at node id 0.

def NN.Verification.PINN.hessian2D (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) : Option (Float × Float) × Option (Float × Float)

Compute (d2u/dx2, d2u/dy2) intervals at node id=5 when available. Returns a pair of Options for X and Y directions respectively.

def NN.Verification.PINN.laplacianBounds2D (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) : Option (Float × Float)

Laplacian enclosure: $\Delta u=u_{xx}+u_{yy}$. For one-dimensional inputs, this returns $u_{xx}$.

def NN.Verification.PINN.parseCert (j : Lean.Json) : Except String (PinnCfg × List (Float × Float) × List (Float × Float) × List (Float × (Float × Float) × (Float × Float) × Float × Float))

Parse the JSON certificate consumed by the PINN verification CLI.

def NN.Verification.PINN.fdResidualBounds (u_minus u0 u_plus : Float × Float) (h : Float) : Float × Float

Finite-difference residual bounds for 1D second derivative.

def NN.Verification.PINN.seedParamsGeneric {α : Type} [Context α] : MLTheory.CROWN.Graph.ParamStore α

Generic param seeding (1D).

def NN.Verification.PINN.seedParamsGeneric2D {α : Type} [Context α] : MLTheory.CROWN.Graph.ParamStore α

2D generic param seeding (first layer 16x2).

def NN.Verification.PINN.seedInputGeneric {α : Type} [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) (x eps : α) : MLTheory.CROWN.Graph.ParamStore α

Generic input seeding for 1D.

def NN.Verification.PINN.seedInputGeneric2D {α : Type} [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) (x y eps : α) : MLTheory.CROWN.Graph.ParamStore α

Generic input seeding for 2D.