α-CROWN and α/β-CROWN End-to-End Enclosure

The transfer theorems alphaCrown_transfer_sound and alphaBetaCrown_transfer_sound take the IBP boxes as an assumption (IBPEnclosesVals): every IBP box present at a node must enclose the semantic value at that node. This file discharges that assumption from the IBP soundness theorem CertSoundness.cert_encloses_semantics and states the fully composed corollaries.

The composed statements are quantified over the node ids at which both a certificate entry and a semantic value are present, or, given CrownCertCovers, over every node. The match form of the underlying checker theorems is trivially true at nodes where either side is missing, so these are the forms a caller should use.

Discharging IBPEnclosesVals

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.ibp_encloses_vals_of_cert_local_ok (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (vals : Array (Option CertSoundness.Val)) (htopo : CertSoundness.TopoSorted g) (hsupp : CertSoundness.Supported g) (hibp : CertSoundness.CertLocalOK g ps ibp) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputs : CertSoundness.InputsEnclosed g ps inputs) : IBPEnclosesVals ibp vals

A locally consistent IBP certificate encloses every locally consistent semantic interpretation.

This is CertSoundness.cert_encloses_semantics repackaged in the shape the α-CROWN transfer theorems expect. The hypotheses are exactly those of the IBP theorem: the graph is topologically sorted and uses only supported ops, the IBP boxes replay the checker step at every node, the values replay the evaluator at every node, and the input values lie inside their seed boxes.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.ibp_encloses_vals_runIBP? (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ CertSoundness.Val) (htopo : CertSoundness.TopoSorted g) (hsupp : CertSoundness.Supported g) (hinputs : CertSoundness.InputsEnclosed g ps inputs) : IBPEnclosesVals (CertSoundness.runIBP? g ps) (CertSoundness.evalGraphRec g ps inputs)

The IBP boxes computed by the total checker pass runIBP? enclose the values computed by the total evaluator evalGraphRec.

α-CROWN

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaCrown_cert_encloses_semantics (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]) (htopo : CertSoundness.TopoSorted g) (hsupp : CertSoundness.Supported g) (hibp : CertSoundness.CertLocalOK g ps ibp) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputsEnc : CertSoundness.InputsEnclosed g ps inputs) (hinputs : InputsMatch inputs ctx x) (halpha : AlphaOK alpha) (hcert : CrownCertSoundness.CrownCertLocalOK g (stepAlpha g ps ibp alpha 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 α-CROWN certificate encloses every corresponding graph value, with the IBP boxes justified rather than assumed.

Compared with alphaCrown_transfer_sound, the hypothesis IBPEnclosesVals is replaced by the IBP-side hypotheses Supported g, CertLocalOK g ps ibp, and InputsEnclosed g ps inputs.

The conclusion is stated for every node id at which the certificate has an entry b and the semantics has a value v; a node missing either one carries no claim.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaCrown_cert_encloses_all_nodes (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]) (htopo : CertSoundness.TopoSorted g) (hsupp : CertSoundness.Supported g) (hibp : CertSoundness.CertLocalOK g ps ibp) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputsEnc : CertSoundness.InputsEnclosed g ps inputs) (hinputs : InputsMatch inputs ctx x) (halpha : AlphaOK alpha) (hcert : CrownCertSoundness.CrownCertLocalOK g (stepAlpha g ps ibp alpha ctx) cert) (hcoverage : CrownCertSoundness.CrownCertCovers g cert vals) (id : ℕ) : id < g.nodes.size → ∃ (b : FlatAffineBounds ℝ) (v : CertSoundness.Val), cert[id]! = some b ∧ vals[id]! = some v ∧ CrownCertSoundness.EnclosesAtInput ctx x b v

Every node of a fully covered α-CROWN certificate is enclosed.

CrownCertCovers g cert vals says that every node has both a certificate entry and a semantic value. It is needed because the checker theorems say nothing about nodes at which the certificate producer or the evaluator returned none; with coverage, the conclusion cannot hold through a missing entry.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaCrown_cert_encloses_evalGraphRec (g : Graph) (ps : ParamStore ℝ) (alpha : Array (Option (FlatTensor ℝ))) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsupp : CertSoundness.Supported g) (hinputsEnc : CertSoundness.InputsEnclosed g ps inputs) (hinputs : InputsMatch inputs ctx x) (halpha : AlphaOK alpha) (hcert : CrownCertSoundness.CrownCertLocalOK g (stepAlpha g ps (CertSoundness.runIBP? g ps) alpha ctx) cert) (id : ℕ) : id < g.nodes.size → ∀ (b : FlatAffineBounds ℝ) (v : CertSoundness.Val), cert[id]! = some b → (CertSoundness.evalGraphRec g ps inputs)[id]! = some v → CrownCertSoundness.EnclosesAtInput ctx x b v

α-CROWN enclosure against the total IBP pass and the total evaluator.

Here the IBP boxes are runIBP? g ps and the values are evalGraphRec g ps inputs, so the only remaining hypotheses about the graph are TopoSorted, Supported, and the input conditions.

α/β-CROWN

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaBetaCrown_cert_encloses_semantics' (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (beta : 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) (hsupp : CertSoundness.Supported g) (hibp : CertSoundness.CertLocalOK g ps ibp) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputsEnc : CertSoundness.InputsEnclosed g ps inputs) (hinputs : InputsMatch inputs ctx x) (halpha : AlphaOK alpha) (hcert : CrownCertSoundness.CrownCertLocalOK g (stepAlphaBeta g ps ibp alpha beta 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 α/β-CROWN certificate encloses every corresponding graph value, with the IBP boxes justified rather than assumed.

This is alphaBetaCrown_cert_encloses_semantics with IBPEnclosesVals discharged from the IBP soundness theorem; see alphaCrown_cert_encloses_semantics for the hypothesis trade.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaBetaCrown_cert_encloses_all_nodes (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (beta : 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) (hsupp : CertSoundness.Supported g) (hibp : CertSoundness.CertLocalOK g ps ibp) (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hinputsEnc : CertSoundness.InputsEnclosed g ps inputs) (hinputs : InputsMatch inputs ctx x) (halpha : AlphaOK alpha) (hcert : CrownCertSoundness.CrownCertLocalOK g (stepAlphaBeta g ps ibp alpha beta ctx) cert) (hcoverage : CrownCertSoundness.CrownCertCovers g cert vals) (id : ℕ) : id < g.nodes.size → ∃ (b : FlatAffineBounds ℝ) (v : CertSoundness.Val), cert[id]! = some b ∧ vals[id]! = some v ∧ CrownCertSoundness.EnclosesAtInput ctx x b v

Every node of a fully covered α/β-CROWN certificate is enclosed. See alphaCrown_cert_encloses_all_nodes for the role of CrownCertCovers.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaBetaCrown_cert_encloses_evalGraphRec (g : Graph) (ps : ParamStore ℝ) (alpha : Array (Option (FlatTensor ℝ))) (beta : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ CertSoundness.Val) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (htopo : CertSoundness.TopoSorted g) (hsupp : CertSoundness.Supported g) (hinputsEnc : CertSoundness.InputsEnclosed g ps inputs) (hinputs : InputsMatch inputs ctx x) (halpha : AlphaOK alpha) (hcert : CrownCertSoundness.CrownCertLocalOK g (stepAlphaBeta g ps (CertSoundness.runIBP? g ps) alpha beta ctx) cert) (id : ℕ) : id < g.nodes.size → ∀ (b : FlatAffineBounds ℝ) (v : CertSoundness.Val), cert[id]! = some b → (CertSoundness.evalGraphRec g ps inputs)[id]! = some v → CrownCertSoundness.EnclosesAtInput ctx x b v

α/β-CROWN enclosure against the total IBP pass and the total evaluator; see alphaCrown_cert_encloses_evalGraphRec.