Verification starts with a concrete promise: a property is checked against the graph, parameters, shapes, and scalar interpretation that the verifier actually saw. TorchLean’s examples make those objects explicit. Some examples run bound propagation natively over a TorchLean graph. Others replay an exported certificate. In both cases, the important trail is the artifact being checked and the predicate Lean recomputes.

IBP and alpha-CROWN verification example

The Question

Most neural-network verification examples begin with a robustness question:

For every input inside a small box around the example point, can the model’s output still satisfy the desired margin or safety condition?

TorchLean represents that question with four concrete objects:

The common path is therefore:

  1. write or import a TorchLean model,
  2. compile it to NN.IR.Graph,
  3. attach an input box,
  4. run a bound engine,
  5. inspect or check the output bounds.

The examples under NN/Examples/Verification/TorchLean/ keep the model, input box, bound pass, and reported margin in one place, so the verification path can be read directly from the source.

The local example is compact enough that the whole verification object can be read directly: the graph, the input box, the output property, and the bound pass all appear in one place. That matters more than the size of the network. Once the objects are named clearly, the same pattern can be used for generated graphs, imported weights, or external verifier leaves.

The seed box is built explicitly. For the small MLP example, inputCenter is the center point, eps is the radius, and inputBox is the flattened input box inserted at the compiled input node:

let inputCenter : Tensor α xShape :=
  NN.Tensor.ofListOfLength (α := α) [2] [cast 0.5, cast 0.8] (by rfl)
let eps : α := Runtime.ofFloat 0.1
let rad : Tensor α xShape := Spec.fill eps xShape

let inputBox : FlatBox α :=
  { dim := inDim
    lo := Tensor.subSpec inputCenter rad
    hi := Tensor.addSpec inputCenter rad }

let ps : ParamStore α :=
  { compiled.ps with inputBoxes := compiled.ps.inputBoxes.insert compiled.inputId inputBox }

The verifier checks every input in the box $[\mathtt{inputCenter}-\mathtt{eps},\mathtt{inputCenter}+\mathtt{eps}]$.

let ibp := runIBP (α := α) compiled.graph ps
let some outB := ibp[compiled.outputId]! |
  throw <| IO.userError "IBP produced no output box"

The bound engine returns node-indexed FlatBox values. Each box stores a flattened dimension plus lower and upper tensors. If the output box satisfies a margin condition such as $\mathrm{lo}[\mathrm{label}]>\max_{\mathrm{other}}\mathrm{hi}[\mathrm{other}]$, every input in the seed box is certified for that label.

IBP: Propagate Boxes Through The Graph

Interval bound propagation is the simplest sound bound engine used here. Each node gets a lower and upper bound. The transformer for each operation must enclose all possible outputs of that operation when its inputs range over their current boxes.

A scalar example captures the idea. Suppose

\[x \in [-1,2], \qquad y=3x+0.5.\]

IBP computes

\[y \in [3(-1)+0.5,\;3(2)+0.5]=[-2.5,6.5].\]

For a ReLU node, the transformer is monotone:

\[z \in [\ell,u] \quad\Longrightarrow\quad \operatorname{ReLU}(z) \in [\max(0,\ell),\max(0,u)].\]

For a linear layer, the implementation splits positive and negative weights so each input interval is used in the direction that gives the worst case. The result is conservative by design: every true activation is inside the box, but the box may include values that cannot occur together.

That tradeoff explains both why IBP works well as a first verifier and why it can fail to certify true properties. It is fast, local, and easy to compose over graphs; it loses correlations between coordinates.

A Margin Example

Consider a two-logit classifier. To certify class $0$ against class $1$, we want:

\[\operatorname{logit}_0-\operatorname{logit}_1 \geq 0.\]

If IBP gives

\[\operatorname{logit}_0 \in [1.2,1.8], \qquad \operatorname{logit}_1 \in [0.1,0.7],\]

then the margin is at least $1.2-0.7=0.5$, so the box certifies the property. If instead IBP gives

\[\operatorname{logit}_0 \in [0.8,1.4], \qquad \operatorname{logit}_1 \in [0.2,1.0],\]

then the lower margin bound is $0.8-1.0=-0.2$. The property is undecided at the IBP-box level. The model may still be safe; this abstraction was not tight enough for this input box.

CROWN-Style Affine Bounds

CROWN-style passes keep affine upper and lower forms instead of only interval boxes. In other words, the bound can say more than “this node lies between two numbers.” It can be “this node is bounded by a linear expression over the input variables.” That preserves more correlation information.

CROWN still uses IBP intervals, because nonlinear relaxations need pre-activation ranges. Forward CROWN stores affine lower and upper forms for nodes with respect to the chosen input node. Backward CROWN starts from one scalar objective, such as $\operatorname{logit}_0-\operatorname{logit}_1$, and propagates that objective back to an input-box bound.

For ReLU, the affine relaxation depends on the pre-activation interval:

The example builds a context for the input node and runs CROWN after IBP:

let ctx : AffineCtx :=
  { inputId := compiled.inputId, inputDim := softmaxInDim }

let crown := runCROWN (α := α) compiled.graph ps ctx ibp

For a margin objective, the backward pass asks for a bound on one scalar expression, such as $\operatorname{logit}_0-\operatorname{logit}_1$. Instead of bounding every output independently, this lets the verifier push a single objective backward through the graph:

let objV : Tensor α (.dim softmaxOutDim .scalar) :=
  NN.Tensor.ofListOfLength
    (α := α) [3] [cast 1.0, cast (-1.0), cast 0.0] (by rfl)

let obj : FlatVec α := { n := softmaxOutDim, v := objV }

match runCROWNBackwardObjective
    (α := α) compiled.graph ps ctx ibp compiled.outputId obj with
| none => IO.println "[CROWN-backward] no affine bounds"
| some objAff => IO.println s!"[CROWN-backward] objective dim = {objAff.outDim}"

The model, graph, bounds, and certificate checks all refer to the same node ids and tensor shapes.

What Each Command Shows

Run the small TorchLean-native examples first:

lake exe verify -- torchlean-ibp --dtype float
lake exe verify -- torchlean-crown-ops --dtype float
lake exe verify -- torchlean-robustness --dtype float
lake exe verify -- torchlean-mlp-workflow
lake exe verify -- digits-train-certify --epochs=50 --eps=0.02 --max=100
lake exe verify -- margin-cert
lake exe verify -- vnncomp-mnistfc
lake exe verify -- camera-box3d-cert

torchlean-ibp is the smallest graph-bound check: compile a TorchLean model, attach an input box, and propagate interval bounds to the output. torchlean-crown-ops uses the same graph style but adds forward and backward CROWN-style affine passes over supported operations. torchlean-robustness prints IBP, CROWN, and backward-CROWN certification booleans for a compact robustness example. torchlean-mlp-workflow trains an MLP through the compiled backend and then runs IBP/CROWN on the resulting graph-shaped artifact.

The remaining commands show artifact boundaries. digits-train-certify trains a small sklearn-digits classifier with Python, exports weights and test examples, then immediately recompiles and certifies those artifacts in Lean. margin-cert checks an exported margin JSON artifact by recomputing the margin predicate. vnncomp-mnistfc exercises a compact VNN-COMP-style fully connected MNIST network/property pair. camera-box3d-cert checks a camera projection certificate for a 3D box artifact by recomputing the projected corners and the claimed 2D envelope.

The MNIST runner labels its result numerically_refuted, not safe. It uses outward-widened host Float operations to refute the unsafe output region, but that executable result is not itself a Lean theorem about real-valued network semantics.

Typical output from the native CROWN example includes softmax bounds, an MSE-loss bound, a margin lower bound, and the backward objective bound. The exact numbers depend on dtype and runtime flags, but the shape of the output should look like this:

[IBP] logits lo = ...
[IBP] logits hi = ...
[CROWN] logits lo = ...
[CROWN] logits hi = ...
[CROWN-backward] objective bound = ...

Then check the bundled alpha-beta-CROWN-style leaf artifact:

lake exe verify -- abcrown-leaf

Run the compact LiRPA-style JSON fixtures:

lake exe verify -- lirpa-mlp
lake exe verify -- lirpa-cnn
lake exe verify -- lirpa-attention
lake exe verify -- lirpa-gru
lake exe verify -- lirpa-encoder

These commands are good checks when changing certificate parsing or bound-replay utilities. Each bundled fixture names a small supported fragment, such as an MLP, convolutional head, attention softmax block, GRU gate, or transformer encoder block. Lean checks the artifact it receives; the fixture is evidence for the checker format and replay predicate, not a claim about every possible LiRPA producer.

To run the fast non-interactive checker suite:

lake exe verify -- all

External Artifacts

The alpha-beta-CROWN leaf checker is a structural checker for a declared leaf artifact. Vanilla alpha-beta-CROWN does not emit TorchLean’s JSON schema directly. The current path is: an external verifier exposes or dumps terminal leaf data, TorchLean’s exporter converts that data to abcrown_leaf_artifact_v0_1, and Lean checks the represented part of the artifact: box nesting, compatible array sizes, and the witness lower-bound test.

That last sentence is the trust boundary. The Lean checker accepts a specific schema and checks the part of the terminal leaf represented in that schema. If the exporter lies about what the external verifier produced, that is an exporter/provenance boundary. If the JSON satisfies the schema and witness predicate, the Lean side check is local and reproducible.

def leafVerifiedAt (lb thr : Array Float) (witnessIdx : Nat) : Bool :=
  if witnessIdx < lb.size ∧ witnessIdx < thr.size then
    ltBool thr[witnessIdx]! lb[witnessIdx]!
  else
    false

The CLI entry point defaults to a small bundled artifact:

lake exe verify -- abcrown-leaf \
  NN/Examples/Verification/AbCrown/sample_abcrown_leaf_artifact_v0_1.json

To create that schema from a raw terminal-domain dump, use the TorchLean exporter:

python3 scripts/verification/abcrown/export_leaf_artifact.py \
  --input NN/Examples/Verification/AbCrown/example_raw_leaf_dump.json \
  --out _external/abcrown/leaf_artifact.json \
  --check

ABCROWN_ARTIFACT_OUT is the TorchLean side exporter hook. Use it from a small wrapper or instrumented external verifier to write the schema that Lean checks. The external search still owns the branch-and-bound run; TorchLean owns the exported artifact schema and the local witness predicate replayed by the checker.

How To Read A Verification Result

The native and external examples produce different kinds of evidence:

When a command succeeds, cite the object and predicate it checked. For example, say that Lean accepted the abcrown_leaf_artifact_v0_1 witness predicate for a particular JSON file, or that the TorchLean graph IBP pass certified the reported margin on the stated input box. That phrasing is more precise than saying only that a verifier ran.

A green command should always be read together with the object it checked. The question is: which graph, which box, which scalar semantics, which certificate schema, and which theorem or checker predicate did this command use?

Where To Read The Source

The examples provide commands that check the relevant graph, bound, or certificate artifact in Lean, rather than relying only on plots or external Python objects.