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, and
• each leaf contains a witness that refutes the unsafe threshold ($\mathrm{lb}[i]>\mathrm{threshold}[i]$ for some $i$).

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.checkAbCrownLeafArtifact (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/.