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.

It is conservative by design: the goal is to validate the export/import path and the interval computations, not to be a fully featured PDE verifier.

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.12 scripts/verification/pinn/export_pinn_cert.py

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

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

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

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

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