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\leq0$)
0 = unconstrained / unstable
1 = forced active ($0\leq z$)

As with the α-CROWN checker, the certificate is accepted only if the provided binary32 affine bounds exactly match Lean recomputation.

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

These are the JSON-facing utilities for the checker: they parse imported bounds, require exact binary32 agreement for affine replay data, 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

source

structure NN.Verification.CROWNNodeCertAlphaBeta.AlphaBetaCROWNNodeCertificate :

Type

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

The checker returns this structure from readAlphaBetaCROWNNodeCertificate, and the blueprint uses it as the documented shape of the artifact being checked.

ctx : MLTheory.CROWN.Graph.AffineCtx
Affine-propagation context, including the chosen input node and flattened input dimension.
ibp : Array (Option (MLTheory.CROWN.FlatBox (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) _proof_1 _proof_2 _proof_3 _proof_4)))
Optional per-node interval bounds used by nonlinear CROWN steps.
crown : Array (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) _proof_1 _proof_2 _proof_3 _proof_4)))
Optional per-node affine lower/upper bounds.
alpha : Array (Option (MLTheory.CROWN.Graph.FlatTensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) _proof_1 _proof_2 _proof_3 _proof_4)))
Optional per-node α values for ReLU lower relaxations.
beta : Array (Option (Array ℤ))
Optional per-node β phase annotations for ReLU nodes.

Instances For

source

def NN.Verification.CROWNNodeCertAlphaBeta.readAlphaBetaCROWNNodeCertificate (g : MLTheory.CROWN.Graph) (path : String) :

IO AlphaBetaCROWNNodeCertificate

Read an alpha/beta-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) AlphaBetaCROWNNodeCertificate._proof_1 AlphaBetaCROWNNodeCertificate._proof_2 AlphaBetaCROWNNodeCertificate._proof_3 AlphaBetaCROWNNodeCertificate._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

The final in-memory acceptance decision for an α/β-CROWN artifact. It combines all diagnostic checks with a complete pure replay whose proposition-level meaning is proved below.

Instances For

source

theorem NN.Verification.CROWNNodeCertAlphaBeta.AlphaBetaCROWNNodeCertificate.accepts_eq_true (cert : AlphaBetaCROWNNodeCertificate) (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) _proof_1 _proof_2 _proof_3 _proof_4)) (authoritativeIbp : Array (Option (MLTheory.CROWN.FlatBox (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) _proof_1 _proof_2 _proof_3 _proof_4)))) (diagnosticsOk : Bool) (haccept : cert.accepts g ps authoritativeIbp diagnosticsOk = true) :

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.CROWNNodeCertAlphaBeta.checkAlphaBetaCROWNNodeCertificate (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) AlphaBetaCROWNNodeCertificate._proof_1 AlphaBetaCROWNNodeCertificate._proof_2 AlphaBetaCROWNNodeCertificate._proof_3 AlphaBetaCROWNNodeCertificate._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.CROWNNodeCertAlphaBeta

CROWNNodeCertAlphaBeta #