LiRPA MLP certificate checker

This module is a compact end-to-end example of checking an IBP certificate for a compact MLP in TorchLean's graph-based verifier.

It does three things:

1. Defines a compact graph (buildGraph),
2. Seeds deterministic parameters and an input box,
3. Checks a JSON certificate produced by an external tool (LiRPA-style workflow).

Run via the unified CLI registry:

• lake exe verify -- lirpa-mlp [path]

If path is omitted, the CLI uses the default example certificate at: NN/Examples/Verification/LiRPA/mlp_cert.json.

def NN.Examples.Verification.LiRPA.MlpVerify.buildGraph : MLTheory.CROWN.Graph

def NN.Examples.Verification.LiRPA.MlpVerify.seedParamsFloat : MLTheory.CROWN.Graph.ParamStore Float

def NN.Examples.Verification.LiRPA.MlpVerify.seedInputFloat (ps : MLTheory.CROWN.Graph.ParamStore Float) (eps : Float) : MLTheory.CROWN.Graph.ParamStore Float

def NN.Examples.Verification.LiRPA.MlpVerify.verifyCert (path : String) : IO Unit

Check an IBP certificate JSON file and throw an error if it does not match recomputed bounds.