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 its binary32 affine transcript exactly matches Lean recomputation.
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, require exact binary32 agreement for affine replay data, and check parent and shape requirements before invoking the semantic checker.

source

def NN.Verification.CROWNNodeCert.readCROWNNodeCertificate (g : MLTheory.CROWN.Graph) (path : String) :

IO Cert.NodeReplay.CROWNNodeCoreCertificate

Read a CROWN node certificate from JSON on disk.

Instances For

source

IO (Bool × Option (MLTheory.CROWN.Graph.FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkCROWNNode._proof_1 checkCROWNNode._proof_2 checkCROWNNode._proof_3 checkCROWNNode._proof_4)))

Check the local CROWN enclosure condition for one node against a certificate entry.

Instances For

source

The α-CROWN replay function associated with a parsed certificate.

Instances For

source

Bool

The final in-memory acceptance decision for an α-CROWN artifact.

diagnosticsOk records parsing-independent IBP, shape, domain, and incremental-replay checks. The second conjunct establishes local replay consistency. Semantic enclosure additionally requires coverage of the relevant graph nodes and proved transfer rules for their operations.

Instances For

source

MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK g (replayStep g ps authoritativeIbp cert) cert.crown

Acceptance of the concrete α-CROWN decision supplies graph-level local consistency.

source

def NN.Verification.CROWNNodeCert.checkCROWNNodeCertificate (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) checkCROWNNode._proof_1 checkCROWNNode._proof_2 checkCROWNNode._proof_3 checkCROWNNode._proof_4)) (path : String) :

IO Bool

Check a per-node α-CROWN certificate against Lean's propagation rules.

Returns true iff every supplied IBP box contains Lean's authoritative recomputation and every node's affine replay data agrees exactly with Lean's CROWN step.

Instances For

TorchLean API

NN.Verification.Cert.CROWNNodeCert

CROWNNodeCert #