CnnVerify

LiRPA/IBP certificate checker: CNN conv2d -> linear head.

This is a small workflow that:

• encodes a single conv2d 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.Examples.Verification.LiRPA.CnnVerify.buildGraph : MLTheory.CROWN.Graph

Small fixed graph: input(flattened) -> linear(conv2d-as-affine) -> linear(head).

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

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

Seed deterministic parameters and the input box.

Key trick: we compute an affine form for conv2d (A, c) on the input box and insert it as a linearWB entry, so the graph contains only .linear nodes.

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

Check an IBP certificate JSON against this CNN graph.

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