α-CROWN transfer step (graph dialect)

This file defines a pure, per-node transfer rule for affine bound propagation in the NN.MLTheory.CROWN.Graph dialect, extended with an α-parameter for the ReLU lower relaxation (α-CROWN).

The step function is shared by:

• the certificate checker (recompute each node from its parents and compare to a claimed bound), and
• soundness theorems of the form: "if local replay is consistent, then the claimed enclosure holds".

This module does not implement the outer dual-parameter optimization loop used by α/β-CROWN; it only defines the local transfer rule for a fixed set of α-parameters.

References

• CROWN: Zhang et al., Efficient Neural Network Robustness Certification with General Activation Functions, NeurIPS 2018. (arXiv:1811.00866)
• β-CROWN (and the α/β-CROWN toolchain): Wang et al., Beta-CROWN: Efficient Bound Propagation with Provable Guarantees, NeurIPS 2021. (arXiv:2103.06624)

Affine bounds in the graph dialect

A FlatAffineBounds α stores two affine maps (lower/upper) of the flattened input vector: $$ \ell(x) = A_\ell x + c_\ell,\qquad u(x) = A_u x + c_u. $$ These are propagated through the graph using local transfer rules.

The certificate checker recomputes these affine maps node-by-node, so the functions below are written in an executable style (using the repo’s Tensor operations), while still being usable in theorem statements over ℝ.

α-ReLU lower relaxation

α-CROWN lower relaxation for ReLU

For a pre-activation scalar $z\in[l,u]$, CROWN/DeepPoly uses:

• an upper linear envelope (the usual triangular relaxation), and
• a lower linear envelope.

In the unstable crossing case $l < 0 < u$, the lower relaxation can be parameterized by $\alpha\in[0,1]$ to interpolate between the sound choices $y \ge 0$ and $y \ge z$.

We encode this by using alphaRelaxLowerScalar for the lower bound, and using Runtime.Ops.ReLU.relaxScalar / relaxVector for the upper bound.

def NN.MLTheory.CROWN.Cert.alphaRelaxLowerScalar {α : Type} [Context α] (l u a : α) : Runtime.Ops.ReLURelax α

The α-CROWN lower relaxation of a scalar ReLU on [l, u] with slope parameter a.

A stable-active neuron gets the identity, a stable-inactive one gets zero, and an unstable one gets the tunable line y = a·x through the origin.

def NN.MLTheory.CROWN.Cert.alphaRelaxLowerVec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (lo hi αv : TorchLean.Tensor α [n]) : TorchLean.Tensor (Runtime.Ops.ReLURelax α) [n]

Vectorized α-CROWN lower relaxation for ReLU, applied componentwise.

Node step function

def NN.MLTheory.CROWN.Cert.getAff? {α : Type} [TorchLean.Storage α] [Context α] (cert : Array (Option (Graph.FlatAffineBounds α))) (pid : ℕ) : Option (Graph.FlatAffineBounds α)

Safe lookup of the affine bounds recorded for node id pid, none when out of range.

def NN.MLTheory.CROWN.Cert.getAlpha? {α : Type} [TorchLean.Storage α] [Context α] (alpha : Array (Option (Graph.FlatTensor α))) (pid : ℕ) : Option (Graph.FlatTensor α)

Safe lookup of the optional α vector at node id pid.

def NN.MLTheory.CROWN.Cert.defaultAlphaVec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (lo hi : TorchLean.Tensor α [n]) : TorchLean.Tensor α [n]

Default α vector used when the certificate omits α values.

This matches TorchLean's default lower relaxation: pick slope 1 when u > -l, otherwise 0.

def NN.MLTheory.CROWN.Cert.alphaCrownStepNode? {α : Type} [TorchLean.Storage α] [Context α] (nodes : Array Graph.Node) (ps : Graph.ParamStore α) (ibp : Array (Option (FlatBox α))) (alpha : Array (Option (Graph.FlatTensor α))) (cert : Array (Option (Graph.FlatAffineBounds α))) (ctx : Graph.AffineCtx) (id : ℕ) : Option (Graph.FlatAffineBounds α)

One-node α-CROWN step function for a supported subset of IR ops.

The step returns none when required parent bounds or parameters are missing, or when dimensions mismatch. Callers must validate node ids and the size of the IBP table before calling it; direct array indexing relies on those invariants.

It is intended to be used for:

• executable per-node certificate checking (recompute node id from certificate parents), and
• proof-level soundness theorems about the checker.

Supported node kinds

This step function handles the verifier core of the IR:

• .input, .const, .detach
• .linear, .matmul (ParamStore-driven linear operators in the verifier dialect)
• .relu (CROWN upper + α-CROWN lower)
• .sum (treated as a $1\times n$ linear layer)
• .reshape, .flatten (shape-only, guarded by dimensional consistency)

Custom computations return none, even when an IBP box is supplied: a source-evaluation proof does not supply a real-enclosure or derivative rule. Other node kinds fall back to a conservative constant affine enclosure derived from the IBP box at the same node id (if present). The checker remains total over graphs that contain operators outside this affine-transfer subset; end-to-end theorems account for those nodes through the soundness assumptions attached to their IBP boxes.