β-phase ReLU relaxations: pointwise soundness

Analytic core of the β-extended ReLU transfer rule, stated without reference to graphs or step functions.

Given a pre-activation z enclosed both by an affine box (propagated from the parent's certificate) and by an IBP box, the relaxations returned by phaseRelaxVec? enclose relu z. The IBP box is what justifies each phase's affine rule (phaseConsistentScalar? checks the phase against it); the affine box is what the resulting slopes are applied to.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phaseRelax_getScalar_bounds {n : ℕ} (lAff uAff lo hi z αt : TorchLean.Tensor ℝ [n]) (phases : Array ℤ) (relaxLo relaxHi : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [n]) (hαrange : ∀ (i : Fin n), 0 ≤ αt.getScalar i ∧ αt.getScalar i ≤ 1) (hrelax : Cert.phaseRelaxVec? lo hi αt phases = some (relaxLo, relaxHi)) (hzAff : Theorems.Semantics.encloses { dim := n, lo := lAff, hi := uAff } z) (hzIbp : Theorems.Semantics.encloses { dim := n, lo := lo, hi := hi } z) (i : Fin n) : (relaxLo.getScalar i).slope * lAff.getScalar i + (relaxLo.getScalar i).bias ≤ Activation.Math.reluSpec (z.getScalar i) ∧ Activation.Math.reluSpec (z.getScalar i) ≤ (relaxHi.getScalar i).slope * uAff.getScalar i + (relaxHi.getScalar i).bias

Index-wise bounds delivered by a β-consistent phase relaxation.

At index i, the lower relaxation applied to the affine lower bound sits below relu (z i), and the upper relaxation applied to the affine upper bound sits above it. Both slopes are nonnegative, which is what lets the affine bounds on z pass through the relaxations.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.encloses_relu_propagateAffine {inDim n : ℕ} (xLo xHi : AffineVec ℝ inDim n) (x' : TorchLean.Tensor ℝ [inDim]) (lo hi z αt : TorchLean.Tensor ℝ [n]) (phases : Array ℤ) (relaxLo relaxHi : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [n]) (hαrange : ∀ (i : Fin n), 0 ≤ αt.getScalar i ∧ αt.getScalar i ≤ 1) (hrelax : Cert.phaseRelaxVec? lo hi αt phases = some (relaxLo, relaxHi)) (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) : Theorems.Semantics.encloses { dim := n, lo := CrownCertSoundness.affineEvalAt (Runtime.Ops.ReLU.propagateAffine relaxLo xLo) x', hi := CrownCertSoundness.affineEvalAt (Runtime.Ops.ReLU.propagateAffine relaxHi xHi) x' } (Activation.reluSpec z)

Enclosure of relu z by phase relaxations propagated through affine bounds on z.

xLo, xHi are the parent's affine lower and upper bounds (already cast to the IBP dimension n), evaluated at the input x'; lo, hi are the IBP box that phaseRelaxVec? checked the phases against.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.enclosesAtInput_relu_beta (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (xin : FlatAffineBounds ℝ) (vp : CertSoundness.Val) (preB : FlatBox ℝ) (hout : xin.outDim = preB.dim) (αt : TorchLean.Tensor ℝ [preB.dim]) (phases : Array ℤ) (relaxLo relaxHi : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [preB.dim]) (hαrange : ∀ (i : Fin preB.dim), 0 ≤ αt.getScalar i ∧ αt.getScalar i ≤ 1) (hrelax : Cert.phaseRelaxVec? preB.lo preB.hi αt phases = some (relaxLo, relaxHi)) (hpar : CrownCertSoundness.EnclosesAtInput ctx x xin vp) (hibp : CertSoundness.EnclosesBox preB vp) : CrownCertSoundness.EnclosesAtInput ctx x { inDim := xin.inDim, outDim := preB.dim, loAff := Runtime.Ops.ReLU.propagateAffine relaxLo (castAffineOut hout xin.loAff), hiAff := Runtime.Ops.ReLU.propagateAffine relaxHi (castAffineOut hout xin.hiAff) } { n := vp.n, v := Activation.reluSpec vp.v }

Soundness of the β-phase ReLU rule at one node.

The parent value vp is enclosed by its certificate entry xin (evaluated at x) and by its IBP box preB. The node's bounds are the phase relaxations for preB propagated through xin cast to preB.dim, and they enclose relu vp.