PINN Certificate

PINN certificate checker (recompute-and-compare).

This module is the executable checker for the PINN certificate workflow:

• parse a JSON certificate produced by Python,
• rebuild the same CROWN graph and seed the same input boxes,
• recompute IBP + derivative bounds in Lean, and
• compare the resulting residual intervals against the exported values.

Acceptance means that the exported endpoints match the recomputation within certTol. This is not an exact-real residual enclosure theorem or a bound on PDE solution error.

This checker always uses referenceParams 1. The JSON's model and pinn.domain fields are producer metadata, not validated inputs; acceptance does not authenticate their weights or domain. Use the weight-loading CLI for a trained model.

References / context:

• PINNs: Raissi et al. (2019), "Physics-informed neural networks" (JCP)
• CROWN/LiRPA background (for the bound propagation machinery): https://arxiv.org/abs/1811.00866

Export (Python): python3 scripts/verification/pinn/export_pinn_cert.py

Run (Lean): scripts/lake.sh exe verify -- pinn-cert [NN/Examples/Verification/PINN/pinn_cert.json]

def NN.Verification.PINN.Certificate.defaultCertPath : String

Bundled PINN certificate sample used by scripts/lake.sh exe verify -- pinn-cert.

def NN.Verification.PINN.Certificate.requireApproxInterval (ctx : String) (leanBounds artifactBounds : FloatInterval) : IO Unit

Reject a certificate interval that differs from Lean's recomputed interval.

def NN.Verification.PINN.Certificate.verifyCert (path : String) : IO Unit

IO entry that reads the cert, recomputes bounds, and prints comparisons.