CROWNNodeCertAlphaBeta #

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

This extends NN.Verification.CROWNNodeCert with an optional β phase vector for ReLU nodes.

Certificate JSON format:

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

β encoding (per neuron):

-1 = forced inactive (z ≤ 0)
0 = unconstrained / unstable
1 = forced active (0 ≤ z)

As with the α-CROWN checker, the certificate is accepted only if Lean recomputation matches the provided affine bounds up to a small float tolerance.

Helpers for the alpha/beta-CROWN style node certificate checker.

These are the JSON-facing utilities for the checker: they parse imported bounds, compare decimal-serialized floats with an explicit tolerance, and keep shape mismatches from reaching the semantic checker.

source

def NN.Verification.CROWNNodeCertAlphaBeta.parseInt? (j : Lean.Json) :

Option ℤ

Parse a JSON integer (used for beta vectors).

Instances For

source

def NN.Verification.CROWNNodeCertAlphaBeta.parseBetaVec? (dim : ℕ) (j : Lean.Json) :

IO (Option (Array ℤ))

Parse a beta vector from JSON.

Instances For

AlphaBetaCROWNNodeCertificate is the in-memory representation of an alpha/beta-CROWN node certificate read from JSON.

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

source

structure NN.Verification.CROWNNodeCertAlphaBeta.AlphaBetaCROWNNodeCertificate :

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.
beta : Array (Option (Array ℤ))
Optional per-node β phase annotations for ReLU nodes.