AbCrown Leaf Artifact

Alpha-beta-CROWN (AbCrown) leaf-artifact checker.

This module checks a small TorchLean JSON schema (abcrown_leaf_artifact_v0_1). Vanilla alpha-beta-CROWN does not emit this TorchLean schema directly; use scripts/verification/abcrown/export_leaf_artifact.py to convert terminal leaf/domain data from an external verifier into the checked schema.

The checker does not run bound propagation itself. It validates only the finite claims present in the artifact:

• each leaf input box is nested inside the declared root input box,
• the leaf boxes together cover the root box, and
• each leaf contains a witness that refutes the unsafe threshold ($\mathrm{lb}[i]>\mathrm{threshold}[i]$ for some $i$).

The lower bounds lb are the producer's claims and are not recomputed, so a passing artifact is consistent, not verified. The output says so.

This is useful for:

• regression testing JSON export/import paths, and
• reviewer-friendly validation of the leaf data that TorchLean actually checks.

References:

• beta-CROWN paper (NeurIPS 2021): https://arxiv.org/abs/2103.06624
• alpha-beta-CROWN implementation: https://github.com/Verified-Intelligence/alpha-beta-CROWN

Run: lake exe verify -- abcrown-leaf [path/to/artifact.json]

def NN.Verification.Cert.AbCrownLeafCert.defaultArtifactPath : String

Bundled sample alpha-beta-CROWN-style leaf artifact.

def NN.Verification.Cert.AbCrownLeafCert.breakpoints (xs : Array Float) : Array Float

Sorted distinct values of one coordinate across the root and leaf endpoints.

def NN.Verification.Cert.AbCrownLeafCert.leavesCoverRoot (rootLo rootHi : Array Float) (leaves : Array (Array Float × Array Float)) (maxCells : ℕ := 1000000) : Except String Bool

Check that the closed leaf boxes cover the closed root box, assuming every leaf is inside the root.

Along each coordinate, the root and leaf endpoints cut the root into a grid of closed cells. Every leaf is a union of cells, so the leaves cover the root exactly when each cell lies inside one leaf. Coordinates on which every leaf spans the whole root are skipped. The grid is refused, with an error, when it has more than maxCells cells.

def NN.Verification.Cert.AbCrownLeafCert.check (path : String) : IO Unit

Parse and validate a abcrown_leaf_artifact_v0_1 JSON artifact.

Structural problems with the document itself (wrong format tag, missing fields, inconsistent dimensions) throw IO.userError immediately. A leaf that parses but fails one of the three accepted predicates is counted, and the reason is printed for that leaf before the summary line, because the three failure modes call for different responses: a leaf outside the root box means the exporter built the wrong region, a failed prune inequality means the producer's bound does not clear the threshold, and a stale witness_margin means the document disagrees with itself.

def NN.Verification.Cert.AbCrownLeafCert.run (args : List String) : IO Unit

CLI entry point: lake exe verify -- abcrown-leaf [artifact.json].

If no path is provided, checks a small bundled sample artifact under NN/Examples/Verification/AbCrown/.