α-CROWN with ReLU phases (graph dialect)

This extends AlphaCROWN.alphaCrownStepNode? with optional ReLU phases. For a ReLU node, a certificate may provide one phase per neuron:

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

The step checks each phase against the IBP pre-activation bounds: active requires 0 ≤ lo, and inactive requires hi ≤ 0. When every phase is consistent, active and inactive neurons use the exact ReLU (slope 1 or 0) and unstable neurons use the usual α-CROWN relaxation.

Because a phase is accepted only when the IBP interval already proves it, phases add no information beyond IBP. α-CROWN already uses the identity when 0 < lo and zero when hi ≤ 0, so there the two passes agree. They differ only for an active phase with lo = 0: the phase uses the identity, while α-CROWN uses the lower slope α when 0 < hi and zero when hi = 0. Both lines agree at zero, so either choice is sound. Without phases the pass is exactly alphaCrownStepNode?. There are no Lagrangian β multipliers and no branch splits.

Phases have the form of the ReLU split constraints of β-CROWN (Wang et al., Beta-CROWN: Efficient Bound Propagation with Provable Guarantees, NeurIPS 2021), where branch-and-bound chooses the splits and β multipliers enforce them; neither is formalized here. CROWN itself is Zhang et al., Efficient Neural Network Robustness Certification with General Activation Functions, NeurIPS 2018.

ReLU phase encoding

A phase has three values:

• 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

@[instance_reducible]

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

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

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 phase integer (-1/0/1) into a ReLUPhase, returning none on invalid input.

def NN.MLTheory.CROWN.Cert.getPhases? (phases : Array (Option (Array ℤ))) (id : ℕ) : Option (Array ℤ)

The phases of node id, if the certificate gives any.

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

def NN.MLTheory.CROWN.Cert.phaseAt (phases : Array ℤ) (i : ℕ) : ℤ

Read the phase of neuron i, with 0 (unconstrained) past the end of the array.

phaseRelaxVec? checks the array length before reading, so the default is never used there. The total read keeps the executable code free of bounds proofs, and the definition reduces in the kernel.

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 phase array 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 α).
• Phases are read with phaseAt (a total Array.getD read) after checking the length, so no bounds proofs are carried and the definition reduces in the kernel.

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

One-node α-CROWN step with ReLU phases:

• delegates to alphaCrownStepNode? for all non-ReLU ops;
• for ReLU, uses the node's phases if phases[id] provides them.

If the node has no phases, this is exactly alphaCrownStepNode?.

Automatic graph execution

The certificate step above accepts explicit α vectors and phases. The helpers below provide the ordinary executable path used by TorchLean's high-level verifier: α uses the checker's default relaxation, and the phases record every ReLU already proved stable by IBP. Crossing intervals remain unconstrained. This is a fixed-relaxation pass, not the branch-and-bound search of the external alpha-beta-CROWN verifier.

The output-box API uses this affine pass only for backends that certify exact reassociation. Rounded backends use directed CROWN instead; rounded affine coefficients alone are not sound enclosures of the real-valued model. The requested input box seeds both paths.

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.inferredPhasesAt? {α : Type} [TorchLean.Storage α] [Context α] (nodes : Array Graph.Node) (ibp : Array (Option (FlatBox α))) (id : ℕ) : Option (Array ℤ)

The IBP-justified phases of one ReLU node.

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

The phases of every ReLU node that the IBP pass already justifies.

def NN.MLTheory.CROWN.Cert.runPhasedCROWN {α : 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 with IBP phase annotations.

Stable ReLU phases come from IBP and are checked again by phasedCrownStepNode?. Unstable neurons use the default α-CROWN lower relaxation. No β multipliers are optimized and no neuron is split.

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

Evaluate the automatic phased α-CROWN pass at the graph output.

Rounded scalars use directed CROWN: composing nearest-rounded affine coefficients is not a sound enclosure calculation. Both routes seed IBP with the caller's requested input box.