Phased α-CROWN Graph Transfer Soundness

Pointwise soundness theorem for the phase-aware graph transfer rule.

The proof is a dispatch over two cases. Every node that is not a ReLU carrying phases is handled by alphaCrown_transfer_sound, since stepPhased agrees with stepAlpha there (stepPhased_eq_stepAlpha). A ReLU node with phases is handled by inverting the step (stepPhased_relu_phase_inv), reading off the parent's value from the semantics, and applying the pointwise phased ReLU lemma enclosesAtInput_relu_phase.

Semantic glue

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.vals_relu_eq {g : Graph} {ps : ParamStore ℝ} {inputs : Std.HashMap ℕ CertSoundness.Val} {vals : Array (Option CertSoundness.Val)} {id p1 : ℕ} {v : CertSoundness.Val} (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hid : id < g.nodes.size) (hk : g.nodes[id]!.kind = IR.OpKind.relu) (hps : IR.unaryParent? g.nodes[id]!.parents = some p1) (hv : vals[id]! = some v) : ∃ (vp : CertSoundness.Val), vals[p1]! = some vp ∧ v = { n := vp.n, v := Activation.reluSpec vp.v }

A ReLU node's semantic value is relu of its unary parent's value.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.enclosesBox_parent {g : Graph} {ps : ParamStore ℝ} {inputs : Std.HashMap ℕ CertSoundness.Val} {ibp : Array (Option (FlatBox ℝ))} {vals : Array (Option CertSoundness.Val)} {id p : ℕ} {preB : FlatBox ℝ} {vp : CertSoundness.Val} (htopo : CertSoundness.TopoSorted g) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hibp : IBPEnclosesVals ibp vals) (hid : id < g.nodes.size) (hp : p ∈ g.nodes[id]!.parents) (hpre : ibp[p]! = some preB) (hvp : vals[p]! = some vp) : CertSoundness.EnclosesBox preB vp

The IBP box of a parent node encloses that parent's semantic value.

Per-case soundness

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phasedCrown_alpha_case_sound (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (phases : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputs : InputsMatch inputs ctx x) (hibp : IBPEnclosesVals ibp vals) (halpha : AlphaOK alpha) (id : ℕ) (hid : id < g.nodes.size) (hparents : ∀ p ∈ g.nodes[id]!.parents, match cert[p]!, vals[p]! with | some bp, some vp => CrownCertSoundness.EnclosesAtInput ctx x bp vp | x, x_1 => True) (hnoPhases : g.nodes[id]!.kind = IR.OpKind.relu → Cert.getPhases? phases id = none) {b : FlatAffineBounds ℝ} {v : CertSoundness.Val} (hs : stepPhased g ps ibp alpha phases ctx cert id = some b) (hv : vals[id]! = some v) : CrownCertSoundness.EnclosesAtInput ctx x b v

Soundness of stepPhased at every node handled by the α-CROWN rule: all non-ReLU kinds, and ReLU nodes with no phases. The step is literally stepAlpha there, so this is alphaCrown_transfer_sound read at one node.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phasedCrown_relu_phase_case_sound (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (phases : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hibp : IBPEnclosesVals ibp vals) (halpha : AlphaOK alpha) (id : ℕ) (hid : id < g.nodes.size) (hparents : ∀ p ∈ g.nodes[id]!.parents, match cert[p]!, vals[p]! with | some bp, some vp => CrownCertSoundness.EnclosesAtInput ctx x bp vp | x, x_1 => True) {nodePhases : Array ℤ} (hk : g.nodes[id]!.kind = IR.OpKind.relu) (hphases : Cert.getPhases? phases id = some nodePhases) {b : FlatAffineBounds ℝ} {v : CertSoundness.Val} (hs : stepPhased g ps ibp alpha phases ctx cert id = some b) (hv : vals[id]! = some v) : CrownCertSoundness.EnclosesAtInput ctx x b v

Soundness of stepPhased at a ReLU node carrying phases.

The step inversion supplies the parent's certificate entry, its IBP box, the α vector used, and the accepted phase relaxations; the semantics supplies the parent's value; enclosesAtInput_relu_phase does the rest.

Main transfer theorem

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phasedCrown_transfer_sound (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (phases : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputs : InputsMatch inputs ctx x) (hibp : IBPEnclosesVals ibp vals) (halpha : AlphaOK alpha) : CrownCertSoundness.CrownTransferSound g ps inputs vals ctx x (stepPhased g ps ibp alpha phases ctx) cert

Pointwise soundness of the graph-dialect phased α-CROWN transfer rule.

This is the phase-aware analog of alphaCrown_transfer_sound. The step function additionally receives a phases array of per-ReLU phase constraints (active, inactive, unstable). At a ReLU node with phases, phaseRelaxVec? checks each phase against the IBP pre-activation interval via phaseConsistentScalar? (inactive needs u ≤ 0, active needs 0 ≤ l) and, if every phase passes, uses the phase's exact affine rule for that unit; an inconsistent phase rejects the step rather than falling back to another relaxation. All other nodes use the α-CROWN rule.

What the phases contribute here, and what they do not. Because a phase is accepted only when the IBP interval already implies it, the phases can never certify a sign that the supplied ibp box does not fix on its own; for such stable units the phase rule coincides with the standard relaxation, except for an active phase with a zero lower endpoint, where the phase rule uses the identity and α-CROWN uses the slope α (or zero when the upper endpoint is zero too). The theorem therefore establishes two things about phases: the exact rules are sound whenever the consistency check passes, and inconsistent phases are rejected. It does not model branch-and-bound split constraints. A split that tightens beyond IBP would have to be reflected in a tighter ibp argument, which this theorem takes as given through IBPEnclosesVals.

The theorem states that this concrete step function satisfies CrownTransferSound, and thus can be used as the trusted checker semantics in crown_checker_encloses_semantics.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.phasedCrown_cert_encloses_semantics_of_ibpEnclosesVals (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (phases : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputs : InputsMatch inputs ctx x) (hibp : IBPEnclosesVals ibp vals) (halpha : AlphaOK alpha) (hcert : CrownCertSoundness.CrownCertLocalOK g (stepPhased g ps ibp alpha phases ctx) cert) (id : ℕ) : id < g.nodes.size → ∀ (b : FlatAffineBounds ℝ) (v : CertSoundness.Val), cert[id]! = some b → vals[id]! = some v → CrownCertSoundness.EnclosesAtInput ctx x b v

A locally replayed phased α-CROWN certificate encloses every corresponding graph value, given IBP boxes that enclose those values (IBPEnclosesVals).

This is the composition of phasedCrown_transfer_sound with the generic graph certificate checker; EndToEnd discharges IBPEnclosesVals to obtain the user-facing phasedCrown_cert_encloses_semantics. The certificate producer remains untrusted: hcert requires its entries to agree node-by-node with TorchLean's phased transfer function.