PINN Core

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

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

• a dimension-parameterized CROWN graph for a tanh MLP,
• deterministic parameters and typed input-box seeding,
• 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:

• scripts/lake.sh exe verify -- pinn-cert [NN/Examples/Verification/PINN/pinn_cert.json]
• scripts/lake.sh 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.parseObjectField (ctx key : String) (j : Lean.Json) : Except String (Std.TreeMap.Raw String Lean.Json compare)

Parse an object-valued JSON field.

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

Parse an array-valued JSON field.

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

Parse a finite-float-array JSON field.

structure NN.Verification.PINN.FloatInterval : Type

A closed interval with finite floating-point endpoints.

• lower : Float

  Lower endpoint.

• upper : Float

  Upper endpoint.

@[instance_reducible]

instance NN.Verification.PINN.instReprFloatInterval : Repr FloatInterval

def NN.Verification.PINN.instReprFloatInterval.repr : FloatInterval → ℕ → Std.Format

def NN.Verification.PINN.parseInterval (ctx : String) (j : Lean.Json) : Except String FloatInterval

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

def NN.Verification.PINN.parseIntervals (ctx : String) (j : Lean.Json) (expected : ℕ) : Except String (Array FloatInterval)

Parse parallel lower/upper arrays into checked intervals.

structure NN.Verification.PINN.SolutionBounds : Type

One finite-difference sample from a PINN certificate.

• point : Float

  Coordinate at the center of the finite-difference stencil.

• previous : FloatInterval

  Solution enclosure at point - spacing.

• center : FloatInterval

  Solution enclosure at point.

• next : FloatInterval

  Solution enclosure at point + spacing.

@[instance_reducible]

instance NN.Verification.PINN.instReprSolutionBounds : Repr SolutionBounds

def NN.Verification.PINN.instReprSolutionBounds.repr : SolutionBounds → ℕ → Std.Format

def NN.Verification.PINN.parseSolutionBounds (ctx : String) (j : Lean.Json) : Except String SolutionBounds

Parse one finite-difference u_bounds entry.

structure NN.Verification.PINN.CertificateConfig : Type

Configuration parsed from a PINN certificate JSON.

• pde : String

  PDE identifier carried by the certificate.

• spacing : Float

  Grid spacing used by the exported finite-difference residual.

• radius : Float

  Input perturbation radius for interval checking.

• pointCount : ℕ

  Number of sample points encoded in points.

• points : TorchLean.Tensor Float [self.pointCount]

  Sample points as a length-pointCount 1D tensor.

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

structure NN.Verification.PINN.Certificate : Type

A parsed and validated PINN certificate artifact.

• config : CertificateConfig

  Model and sampling configuration.

• residualBounds : Array FloatInterval

  Finite-difference residual enclosures at each sample point.

• derivativeResidualBounds : Array FloatInterval

  Derivative residual enclosures at each sample point.

• solutionBounds : Array SolutionBounds

  Solution enclosures for each three-point finite-difference stencil.

def NN.Verification.PINN.certTol : Float

Absolute tolerance for PINN artifact replay comparisons through NN.Verification.Util.approxEq. This is a comparison policy, not a proved bound on rounding or finite-difference truncation error.

def NN.Verification.PINN.referenceArch (inputDim : ℕ) : SequentialPINNArch

The reference scalar-output PINN architecture at an arbitrary input dimension.

def NN.Verification.PINN.buildReferenceGraph (inputDim : ℕ) : MLTheory.CROWN.Graph

Build the reference PINN graph at the requested input dimension.

def NN.Verification.PINN.referenceParams {α : Type} [TorchLean.Storage α] [Context α] (inputDim : ℕ) : MLTheory.CROWN.Graph.ParamStore α

Deterministic reference parameters at an arbitrary input dimension.

These values mirror the bundled exporter. They are demonstration parameters, not trained weights; production checks should load the exported state through PINN.PyTorch.

def NN.Verification.PINN.seedInput {α : Type} [TorchLean.Storage α] [Context α] [MLTheory.CROWN.BoundOps α] {inputDim : ℕ} (ps : MLTheory.CROWN.Graph.ParamStore α) (center : TorchLean.Tensor α [inputDim]) (eps : α) : MLTheory.CROWN.Graph.ParamStore α

Seed an $\ell_\infty$ input box centered at a typed input tensor.

def NN.Verification.PINN.outputInterval (ctx : String) (boxes : Array (Option (MLTheory.CROWN.FlatBox Float))) (outId : ℕ) : Except String FloatInterval

Read the output box of a propagation pass as a scalar interval.

Scalar-output PINN graphs have a length-one output vector, so summing its entries is the exact scalar readout. A missing box is reported with ctx as the message prefix, so callers can name the failing pass.

def NN.Verification.PINN.axisDerivativeBounds (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (ibp : Array (Option (MLTheory.CROWN.FlatBox Float))) (inDim : ℕ) (axis : Fin inDim) : Option FloatInterval × Option FloatInterval

Enclose the first and second directional derivatives of the output along one input axis.

The two come back together on purpose. The second derivative is propagated on top of the first, so splitting them into separate entry points would repeat the same sweep. The interval boxes arrive as a parameter instead of being recomputed here, which is what lets a two-dimensional model pay for the IBP pass once and then ask about x and y in turn. A none component means the derivative propagator produced no box at the output node, which happens when the graph contains an operator it does not cover.

def NN.Verification.PINN.parseCertificate (j : Lean.Json) : Except String Certificate

Parse the JSON certificate consumed by the PINN verification CLI.

def NN.Verification.PINN.finiteDifferenceResidual (previous center next : FloatInterval) (spacing : Float) : FloatInterval

Finite-difference residual bounds for 1D second derivative.