PINN Dataset Check

Dataset-backed PINN certificate checker.

This is small and explicit: 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.defaultDatasetPath : String

Bundled dataset sample used by lake exe verify -- pinn-dataset-check.

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

CLI options for pinn-dataset-check.

• weights : Option String

  Optional JSON file containing exported PINN weights.

• dataset : Option String

  Dataset JSON containing initial, boundary, residual, or data points to check.

• eps : Float

  Radius used to seed the input interval around each dataset point.

• tol : Float

  Allowed endpoint tolerance when checking that the reference value is enclosed.

• maxPts : ℕ

  Maximum number of points checked from each dataset section.

• strict : Bool

  Treat any failed enclosure check as a command failure.

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

@[implicit_reducible]

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

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

Help text for the dataset-backed PINN checker.

def NN.Verification.PINN.DatasetCheck.parseArgs (args : List String) : Except String DatasetCheckOpts

Parse command-line flags for pinn-dataset-check.

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

Load a PINN graph and parameters, using built-in seed parameters when no weights are supplied.

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

Check one dataset section and return (contained, missed, maxAbsMidpointError).

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.