α/β-CROWN certificate step function (graph dialect)

This extends AlphaCROWN.alphaCrownStepNode? with explicit β-phase constraints for ReLU:

For a ReLU node, a certificate may additionally provide a per-neuron phase vector:

• -1 = neuron forced inactive (z ≤ 0)
• 0 = no phase constraint (unstable)
• 1 = neuron forced active (0 ≤ z)

The step function checks phase consistency against the provided IBP pre-activation bounds:

• active requires 0 ≤ lo
• inactive requires hi ≤ 0

If the phase vector is present and consistent, the propagated affine bounds use the exact ReLU behavior for active/inactive neurons (slope 1 / slope 0), and the usual α-CROWN / CROWN relaxations for unstable neurons.

Trust boundary: β is additional evidence verified against the trusted-for-this-theorem IBP bounds.

Background / citations

This checker is kept narrow and certificate-friendly. Conceptually, β-phase information corresponds to the phase constraints used in branch-and-bound based verifiers (and in β-CROWN-style splitting), where additional information can turn unstable ReLUs into provably active/inactive ones.

• CROWN: Zhang et al., Efficient Neural Network Robustness Certification with General Activation Functions, NeurIPS 2018.
• β-CROWN (splitting / phase refinement): Wang et al., Beta-CROWN: Efficient Bound Propagation with Provable Guarantees, NeurIPS 2021 (and follow-up work).

We do not attempt to formalize the full β-CROWN search/optimization loop here; the checker only verifies that the provided β phases are consistent with IBP and then uses the corresponding exact ReLU transfer rule (slope $0$ or $1$).

ReLU phase encoding

We represent β information using a three-valued phase:

• inactive: pre-activation $z \le 0$, so ReLU is exactly $0$;
• active: pre-activation $0 \le z$, so ReLU is exactly $z$;
• unstable: no phase constraint, so we fall back to linear relaxations.

At runtime, a certificate provides an Array Int with entries in $\{-1,0,1\}$, which we decode using ReLUPhase.ofInt?.

inductive NN.MLTheory.CROWN.Cert.ReLUPhase : Type

Which side of the origin a certificate claims a pre-activation stays on.

unstable is the honest "do not know", and it is the only phase that forces the relaxation to spend an α parameter.

• inactive : ReLUPhase

  The pre-activation is claimed nonpositive, so the ReLU output is zero.

• unstable : ReLUPhase

  No claim: the pre-activation may cross zero.

• active : ReLUPhase

  The pre-activation is claimed nonnegative, so the ReLU acts as the identity.

@[instance_reducible]

instance NN.MLTheory.CROWN.Cert.instDecidableEqReLUPhase : DecidableEq ReLUPhase

def NN.MLTheory.CROWN.Cert.instReprReLUPhase.repr : ReLUPhase → ℕ → Std.Format

@[instance_reducible]

instance NN.MLTheory.CROWN.Cert.instReprReLUPhase : Repr ReLUPhase

def NN.MLTheory.CROWN.Cert.ReLUPhase.toInt : ReLUPhase → ℤ

Encode a ReLUPhase as the certificate integer convention {-1, 0, 1}.

def NN.MLTheory.CROWN.Cert.ReLUPhase.ofInt? (i : ℤ) : Option ReLUPhase

Decode a runtime β phase integer (-1/0/1) into a ReLUPhase, returning none on invalid input.

def NN.MLTheory.CROWN.Cert.getBeta? (beta : Array (Option (Array ℤ))) (id : ℕ) : Option (Array ℤ)

Safe lookup of the optional β vector at node id id.

def NN.MLTheory.CROWN.Cert.phaseConsistentScalar? {α : Type} [Context α] (l u : α) (ph : ReLUPhase) : Option Unit

Executable phase-consistency check for a scalar pre-activation interval $[l,u]$.

This is written for a generic Context α (so it can run over floats or other semirings). For proof-level soundness over ℝ, see theorems in NN/MLTheory/CROWN/Proofs/AlphaBetaReLUScalarSoundness.lean.

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

Phase-aware upper (over-approx) linear relaxation for ReLU.

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

Phase-aware lower (under-approx) linear relaxation for ReLU.

opaque NN.MLTheory.CROWN.Cert.betaAt (phases : Array ℤ) (i : ℕ) : ℤ

Opaque wrapper around Array.get! for β-phase vectors.

Why this exists:

• The executable definition phaseRelaxVec? indexes phases with get! after a length check, to avoid threading bounds proofs through the code.
• During proofs, simp can sometimes rewrite get! into the safe indexing phases[i] (which carries a proof argument). Those proof terms are definitional artifacts and can make routine simplification depend on irrelevant proof objects.

Keeping the indexing step opaque prevents simp from introducing proof-carrying indices, while preserving executability.

def NN.MLTheory.CROWN.Cert.phaseRelaxVec? {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (lo hi αv : TorchLean.Tensor α [n]) (phases : Array ℤ) : Option (TorchLean.Tensor (Runtime.Ops.ReLURelax α) [n] × TorchLean.Tensor (Runtime.Ops.ReLURelax α) [n])

Vectorized construction of ReLU relaxations under β-phase constraints.

Returns (relaxLo, relaxHi) if:

• the β vector has the correct length, and
• every scalar entry is decodable and phase-consistent with the IBP interval bounds.

Implementation notes:

• We first compute a boolean ok over all indices (so the function remains executable in a generic Context α).
• We access the β-phase vector with get! after checking the length. This avoids carrying bounds proofs while remaining total as Lean code.

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

One-node α/β-CROWN step:

• delegates to alphaCrownStepNode? for all non-ReLU ops;
• for ReLU, optionally uses a β phase vector (if provided at beta[id]).

If no β info is present for this node, this is exactly alphaCrownStepNode?.

Automatic graph execution

The certificate step above accepts explicit α and β evidence. The helpers below provide the ordinary executable path used by TorchLean's high-level verifier: α uses the checker's default relaxation, while β records every ReLU phase already proved stable by IBP. Crossing intervals remain unconstrained. This is a fixed-relaxation α/β-CROWN pass, not the external branch-and-bound search performed by full Alpha-Beta-CROWN implementations.

def NN.MLTheory.CROWN.Cert.inferredPhase {α : Type} [Context α] (lo hi : α) : ReLUPhase

Infer the strongest phase justified directly by one pre-activation interval.

def NN.MLTheory.CROWN.Cert.inferredBetaForNode? {α : Type} [TorchLean.Storage α] [Context α] (nodes : Array Graph.Node) (ibp : Array (Option (FlatBox α))) (id : ℕ) : Option (Array ℤ)

Infer an IBP-justified β vector for one ReLU node.

def NN.MLTheory.CROWN.Cert.inferredBeta {α : Type} [TorchLean.Storage α] [Context α] (nodes : Array Graph.Node) (ibp : Array (Option (FlatBox α))) : Array (Option (Array ℤ))

Infer all β phase vectors that are already justified by the IBP pass.

def NN.MLTheory.CROWN.Cert.runAlphaBetaCROWN {α : Type} [TorchLean.Storage α] [Context α] (g : Graph) (ps : Graph.ParamStore α) (ctx : Graph.AffineCtx) (ibp : Array (Option (FlatBox α))) : Array (Option (Graph.FlatAffineBounds α))

Run the fixed-relaxation α/β-CROWN graph pass.

Stable ReLU phases come from IBP and are checked again by alphaBetaCrownStepNode?. Unstable neurons use the default α-CROWN lower relaxation.

def NN.MLTheory.CROWN.Cert.outputBoxAlphaBetaCROWN? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : Graph.ParamStore α) (xB : FlatBox α) (inputId outputId inputDim : ℕ) : Except String (FlatBox α)

Evaluate the automatic α/β-CROWN pass at the graph output.