CROWNNodeCert #

Per-node α-CROWN certificate checking (graph dialect).

This mirrors NN.Verification.IBPNodeCert, but for affine bounds produced by a CROWN/DeepPoly pass with optional α-parameters for the ReLU lower relaxation (α-CROWN).

Certificate JSON format:

{
  "ctx": { "inputId": 0, "inputDim": 2 },
  "ibp": [ null | { "lo": [...], "hi": [...] }, ... ],
  "crown": [
    null |
      {
        "loA": [[...], ...], "loC": [...],
        "hiA": [[...], ...], "hiC": [...]
      },
    ...
  ],
  "alpha": [ null | [...], ... ] // optional per-node ReLU α vector
}

Trust boundary notes:

The certificate is untrusted; we accept it only if Lean recomputation matches (within a float tolerance due to JSON decimal serialization).
Transcendental relaxations are checked only via structural recomputation, not via a formal "libm is correct" guarantee.

The helpers below are the JSON-facing boundary for the CROWN certificate checkers. They parse the artifact, compare decimal-serialized floats with an explicit tolerance, and check parent/shape requirements before invoking the semantic checker.

CROWNNodeCertificate is the in-memory representation of a node-wise CROWN certificate read from JSON.

This is part of the public surface of the checker because readCROWNNodeCertificate returns it, and because the blueprint points to it as the “shape of the artifact” being checked.

source

structure NN.Verification.CROWNNodeCert.CROWNNodeCertificate :

Type

ctx : MLTheory.CROWN.Graph.AffineCtx
Affine-propagation context, including the chosen input node and flattened input dimension.
ibp : Array (Option (MLTheory.CROWN.FlatBox Float))
Optional per-node interval bounds used by nonlinear CROWN steps.
crown : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds Float))
Optional per-node affine lower/upper bounds.
alpha : Array (Option (MLTheory.CROWN.Graph.FlatVec Float))
Optional per-node α values for ReLU lower relaxations.