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.

On failure this throws IO.userError with a brief message.

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