PINN CLI

PINN residual-bounding CLI.

This file implements a small interactive tool for bounding PDE residuals of a trained physics-informed neural network (PINN) over a box input region. Concretely, it:

• parses a compact PDE mini-language (see PdeAst / PdeParse),
• evaluates that expression using interval bounds for u, du, and d2u,
• computes those primitive bounds via IBP/CROWN-style propagation on a CROWN Graph,
• optionally tightens bounds by recursively splitting the input box (1D/2D).

This CLI is the interactive PINN residual-bound tool:

• use it when you want to inspect residual bounds interactively;
• use it when you are iterating on a PDE expression or input box;
• use the certificate checker when you want a stable artifact for docs, papers, or CI.

The stable artifact checker is: lake exe verify -- pinn-cert [NN/Examples/Verification/PINN/pinn_cert.json]

Run this CLI via the unified verification dispatcher: lake exe verify -- pinn-cli -- [flags] "<PDE>" x eps or for 2D: lake exe verify -- pinn-cli -- [flags] "<PDE>" x y eps

Examples:

• lake exe verify -- pinn-cli -- "u_xx + u" 0.0 0.1
• lake exe verify -- pinn-cli -- --backend=float "u_t - u_xx" 0.0 0.05

References:

• PINNs: https://arxiv.org/abs/1711.10561
• IBP: https://arxiv.org/abs/1810.12715
• CROWN: https://arxiv.org/abs/1811.00866

noncomputable def NN.Verification.PINN.CLI.realToFloat (x : ℝ) (digits : ℕ := 6) : Float

noncomputable def NN.Verification.PINN.CLI.computePrimsAtNF (g : MLTheory.CROWN.Graph) {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] [TorchLean.Floats.NeuralValidRnd rnd] (ps : MLTheory.CROWN.Graph.ParamStore (TorchLean.Floats.NF β fexp rnd)) (_useAffineU : Bool := false) : IO PdeAst.Prims

Compute primitives using a rounded backend α = NF with single-precision nearest-even.

inductive NN.Verification.PINN.CLI.Backend : Type

• float : Backend
• neuralfloat : Backend

def NN.Verification.PINN.CLI.parseBackendArg (s : String) : Option Backend

def NN.Verification.PINN.CLI.parseFloat (s : String) : Option Float

def NN.Verification.PINN.CLI.parseAlphaDecimal {α : Type} [Context α] (s : String) : Option α

Parse a non-scientific decimal string into a generic numeric α using Numbers and Context. Supports optional leading '-' and a single '.'.

def NN.Verification.PINN.CLI.parseAlphaDecimal.pow10 {α : Type} [Context α] (k : ℕ) : α

inductive NN.Verification.PINN.CLI.UBoundsMethod : Type

Compute primitives u, duX, duY, d2uX, d2uY at the unique output node (id=5) for 1D/2D models. Optionally, replace the u-interval with a tighter CROWN/DeepPoly bound.

• ibp : UBoundsMethod
• crownFwd : UBoundsMethod
• crownBwd : UBoundsMethod

def NN.Verification.PINN.CLI.computePrimsAt (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (uMethod : UBoundsMethod := UBoundsMethod.ibp) (backend : Backend := Backend.float) : IO PdeAst.Prims

inductive NN.Verification.PINN.CLI.Method : Type

• ibp : Method
• crownFwd : Method
• crownBwd : Method

@[implicit_reducible]

instance NN.Verification.PINN.CLI.instToStringMethod : ToString Method

def NN.Verification.PINN.CLI.parseMethodVal (s : String) : Option Method

structure NN.Verification.PINN.CLI.Opts : Type

• method : Method

  method.

• backend : Backend

  Execution backend selection.

• weights? : Option String
• splitDepth : ℕ

  split Depth.

partial def NN.Verification.PINN.CLI.parseFlags (opts : Opts) (args : List String) : Opts × List String

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

Entry point for the PINN residual-bounding CLI.

This is an interactive tool registered as: lake exe verify -- pinn-cli -- ...

For certificate checking, use: lake exe verify -- pinn-cert [NN/Examples/Verification/PINN/pinn_cert.json]

Run: lake exe verify -- pinn-cli -- [--method=ibp|crown-fwd|crown-bwd|partial] [--split-depth=N] [--backend=float|neuralfloat] [--weights=PATH.json] "<PDE>" x eps or (2D): lake exe verify -- pinn-cli -- [flags] "<PDE>" x y eps

def NN.Verification.PINN.CLI.main.split1D (x eps : Float) (d : ℕ) (evalAt : Float → Float → IO (Float × Float)) : IO (Float × Float)

def NN.Verification.PINN.CLI.main.split2D (x y eps : Float) (d : ℕ) (evalAt : Float → Float → Float → IO (Float × Float)) : IO (Float × Float)