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.Verification.LiRPA.Mlp.buildGraph : MLTheory.CROWN.Graph

Four-node 3 → 4 → 2 ReLU MLP graph used by the compact LiRPA certificate example.

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

Deterministic Float weights and biases for both linear nodes in buildGraph.

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

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