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

This keeps the checker’s trust boundary small: β is treated as additional evidence that is verified against the (trusted-for-this-theorem) IBP bounds.

Background / citations

This checker is deliberately 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

• inactive : ReLUPhase
• unstable : ReLUPhase
• active : ReLUPhase

@[implicit_reducible]

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

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

@[implicit_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} [Context α] {n : ℕ} (lo hi αv : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (phases : Array ℤ) : Option (Spec.Tensor (Runtime.Ops.ReLURelax α) (Spec.Shape.dim n Spec.Shape.scalar) × Spec.Tensor (Runtime.Ops.ReLURelax α) (Spec.Shape.dim n Spec.Shape.scalar))

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} [Context α] (nodes : Array Graph.Node) (ps : Graph.ParamStore α) (ibp : Array (Option (FlatBox α))) (alpha : Array (Option (Graph.FlatVec α))) (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?.