α-CROWN Transfer: ReLU Nodes

The .relu case of alphaCrown_transfer_sound. The step propagates the parent's affine bounds through the α lower relaxation and the CROWN upper relaxation built from the IBP pre-activation box. The proof is componentwise: scalar inequalities for the two relaxations, a vector-level enclosure for a fixed α vector in [0, 1], and the range facts for the α vector the step selects.

Scalar relaxation inequalities

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.alpha_relax_lower_le_relu (l u a lAff z : ℝ) (hl : l ≤ z) (hu : z ≤ u) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hlz : lAff ≤ z) : (Cert.alphaRelaxLowerScalar l u a).slope * lAff + (Cert.alphaRelaxLowerScalar l u a).bias ≤ Activation.Math.reluSpec z

The α lower relaxation on [l, u], evaluated at a lower estimate lAff ≤ z, lies below relu z.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.relu_le_relax_upper (l u uAff z : ℝ) (hl : l ≤ z) (hu : z ≤ u) (hzu : z ≤ uAff) : Activation.Math.reluSpec z ≤ (Runtime.Ops.ReLU.relaxScalar l u).slope * uAff + (Runtime.Ops.ReLU.relaxScalar l u).bias

relu z lies below the CROWN upper relaxation on [l, u] evaluated at an upper estimate z ≤ uAff.

Vector-level enclosure

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.relu_propagate_getScalar_bounds {inDim n : ℕ} (lo hi αt z : TorchLean.Tensor ℝ [n]) (xLo xHi : AffineVec ℝ inDim n) (x' : TorchLean.Tensor ℝ [inDim]) (hαrange : ∀ (i : Fin n), 0 ≤ αt.getScalar i ∧ αt.getScalar i ≤ 1) (hzAff : Theorems.Semantics.encloses { dim := n, lo := CrownCertSoundness.affineEvalAt xLo x', hi := CrownCertSoundness.affineEvalAt xHi x' } z) (hzIbp : Theorems.Semantics.encloses { dim := n, lo := lo, hi := hi } z) (i : Fin n) : (CrownCertSoundness.affineEvalAt (Runtime.Ops.ReLU.propagateAffine (Cert.alphaRelaxLowerVec lo hi αt) xLo) x').getScalar i ≤ (Activation.reluSpec z).getScalar i ∧ (Activation.reluSpec z).getScalar i ≤ (CrownCertSoundness.affineEvalAt (Runtime.Ops.ReLU.propagateAffine (Runtime.Ops.ReLU.relaxVector lo hi) xHi) x').getScalar i

Componentwise ReLU bound: if z lies in both the affine estimate box and the IBP box, and the α vector lies in [0, 1], then the propagated lower and upper affine forms bracket relu z at every index.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.enclosesAtInput_relu_propagate {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {xin : FlatAffineBounds ℝ} {vp : CertSoundness.Val} {preB : FlatBox ℝ} (αt : TorchLean.Tensor ℝ [preB.dim]) (hαrange : ∀ (i : Fin preB.dim), 0 ≤ αt.getScalar i ∧ αt.getScalar i ≤ 1) (hout : xin.outDim = preB.dim) (hpar : CrownCertSoundness.EnclosesAtInput ctx x xin vp) (hEncIbp : CertSoundness.EnclosesBox preB vp) : CrownCertSoundness.EnclosesAtInput ctx x { inDim := xin.inDim, outDim := preB.dim, loAff := Runtime.Ops.ReLU.propagateAffine (Cert.alphaRelaxLowerVec preB.lo preB.hi αt) (castAffineOut hout xin.loAff), hiAff := Runtime.Ops.ReLU.propagateAffine (Runtime.Ops.ReLU.relaxVector preB.lo preB.hi) (castAffineOut hout xin.hiAff) } { n := vp.n, v := Activation.reluSpec vp.v }

ReLU transfer core: if xin encloses the parent value vp at x, the IBP box preB encloses vp, and the α vector lies in [0, 1], then propagating xin through the α lower and CROWN upper relaxations encloses relu vp.

The α vector selected by the step

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.alpha_cast_range {alpha : Array (Option (FlatTensor ℝ))} {id : ℕ} {αv : FlatTensor ℝ} {n : ℕ} (halpha : AlphaOK alpha) (hαopt : Cert.getAlpha? alpha id = some αv) (hα : αv.n = n) (i : Fin n) : 0 ≤ (castDimScalar hα αv.v).getScalar i ∧ (castDimScalar hα αv.v).getScalar i ≤ 1

A certificate α entry, cast to the pre-activation dimension, has all components in [0, 1] under AlphaOK.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.selected_alpha_range {alpha : Array (Option (FlatTensor ℝ))} {id : ℕ} {αv : FlatTensor ℝ} {preB : FlatBox ℝ} (halpha : AlphaOK alpha) (hαopt : Cert.getAlpha? alpha id = some αv) (i : Fin preB.dim) : 0 ≤ (if hα : αv.n = preB.dim then castDimScalar hα αv.v else Cert.defaultAlphaVec preB.lo preB.hi).getScalar i ∧ (if hα : αv.n = preB.dim then castDimScalar hα αv.v else Cert.defaultAlphaVec preB.lo preB.hi).getScalar i ≤ 1

The α vector the step selects when a certificate entry is present (the entry cast to the pre-activation dimension if the sizes agree, the default relaxation otherwise) has all components in [0, 1].

The .relu case

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.relu_sound {g : Graph} {ps : ParamStore ℝ} {ibp : Array (Option (FlatBox ℝ))} {alpha : Array (Option (FlatTensor ℝ))} {cert : Array (Option (FlatAffineBounds ℝ))} {inputs : Std.HashMap ℕ CertSoundness.Val} {vals : Array (Option CertSoundness.Val)} {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {id : ℕ} {b : FlatAffineBounds ℝ} {v : CertSoundness.Val} (hk : g.nodes[id]!.kind = IR.OpKind.relu) (hs : stepAlpha g ps ibp alpha ctx cert id = some b) (hEvalSome : CertSoundness.evalNode? g.nodes ps inputs vals id = some v) (hpar : ParentsEnclosed g cert vals ctx x id) (hparLt : ∀ p ∈ g.nodes[id]!.parents, p < vals.size) (hibp : IBPEnclosesVals ibp vals) (halpha : AlphaOK alpha) : CrownCertSoundness.EnclosesAtInput ctx x b v

The .relu case: the step propagates the parent's affine bounds through the α lower and CROWN upper relaxations built from the IBP pre-activation box at the parent, and the evaluator applies reluSpec to the parent's value. The α vector is the certificate entry when present and well-sized, and the default relaxation otherwise.