LiRPA convolutional certificate checker

LiRPA/IBP certificate checker for a convolution followed by a linear head.

This workflow:

• encodes a convolution as an affine form (so the graph stays in the flat-vector LiRPA engine),
• adds a linear head, and
• checks a JSON certificate (produced by Python) using NN.Verification.Cert.IBPCert.

References:

• IBP: arXiv:1810.12715 https://arxiv.org/abs/1810.12715
• auto_LiRPA (reference implementation / cert exporter inspiration): https://github.com/Verified-Intelligence/auto_LiRPA

Export (Python): python3.12 scripts/verification/lirpa/export_cnn_cert.py

Run (Lean): lake exe verify -- lirpa-cnn [NN/Examples/Verification/LiRPA/cnn_cert.json]

def NN.Verification.LiRPA.Cnn.buildGraph : MLTheory.CROWN.Graph

Small fixed graph: input(flattened) -> linear(convolution) -> ReLU -> linear(head).

We keep it flat so the certificate checker works over FlatBox inputs.

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

Seed deterministic parameters and the input box.

The convolution is materialized as its exact flattened matrix and bias. ReLU remains an explicit graph node, so IBP applies its interval rule instead of disguising one affine relaxation as an exact linear layer.

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

Check an IBP certificate JSON against this CNN graph.

This is wired into lake exe verify -- lirpa-cnn [path].