PINN Dataset Check

Dataset-backed PINN "sanity checker".

This is intentionally lightweight: it reads a dataset JSON in the same schema as train_pinn_1d.py --dataset-json, evaluates the network on the dataset's initial/boundary/data points, and reports whether the ground-truth u value is contained in the output interval (with a tolerance).

This does not prove that the network solves the PDE; it is a bridge for using a real reference dataset while exercising the same Lean-side bound propagation machinery as the PINN CLI.

References:

• PINNs: https://arxiv.org/abs/1711.10561
• IBP (interval bounds): https://arxiv.org/abs/1810.12715
• CROWN (linear bounds): https://arxiv.org/abs/1811.00866

def NN.Verification.PINN.DatasetCheck.JsonObj : Type

structure NN.Verification.PINN.DatasetCheck.DatasetCheckOpts : Type

CLI options for pinn-dataset-check.

• weights : Option String

  weights.

• dataset : Option String

  dataset.

• eps : Float

  eps.

• tol : Float

  tol.

• maxPts : ℕ

  max Pts.

• strict : Bool

  strict.

@[implicit_reducible]

instance NN.Verification.PINN.DatasetCheck.instReprDatasetCheckOpts : Repr DatasetCheckOpts

def NN.Verification.PINN.DatasetCheck.instReprDatasetCheckOpts.repr : DatasetCheckOpts → ℕ → Std.Format

def NN.Verification.PINN.DatasetCheck.usage : String

def NN.Verification.PINN.DatasetCheck.parseFloatLit (s : String) : Option Float

def NN.Verification.PINN.DatasetCheck.parseArgs : List String → Except String DatasetCheckOpts

def NN.Verification.PINN.DatasetCheck.getFloat (o : JsonObj) (k : String) : Except String Float

def NN.Verification.PINN.DatasetCheck.getYorT (o : JsonObj) : Except String Float

def NN.Verification.PINN.DatasetCheck.getArrD (o : JsonObj) (k : String) : Except String (Array Lean.Json)

def NN.Verification.PINN.DatasetCheck.parseXYZ (j : Lean.Json) : Except String (Float × Float × Float)

def NN.Verification.PINN.DatasetCheck.loadDatasetXYZ (path sectionName : String) : IO (Array (Float × Float × Float))

def NN.Verification.PINN.DatasetCheck.loadGraphAndParams (weightsPath? : Option String) : IO (MLTheory.CROWN.Graph × MLTheory.CROWN.Graph.ParamStore Float)

def NN.Verification.PINN.DatasetCheck.inInterval (u lo hi tol : Float) : Bool

def NN.Verification.PINN.DatasetCheck.absDiff (a b : Float) : Float

def NN.Verification.PINN.DatasetCheck.checkSection (g : MLTheory.CROWN.Graph) (ps0 : MLTheory.CROWN.Graph.ParamStore Float) (opts : DatasetCheckOpts) (sectionName : String) (pts : Array (Float × Float × Float)) : IO (ℕ × ℕ × Float)

def NN.Verification.PINN.DatasetCheck.main (args : List String) : IO Unit

Entry point: dataset-backed interval containment check for a PINN model.

This is wired into the unified dispatcher as: lake exe verify -- pinn-dataset-check [PATH.json]

The JSON schema matches the exporter used by train_pinn_1d.py --dataset-json.