Certificate Soundness: Elementwise Arithmetic Nodes #
Operator cases add, sub, and mulElem of the IBP certificate induction. Each operator has a
box-level lemma (enclosure of the propagated box, with the dimension bookkeeping done once) and a
node-level lemma that reads the parents off the graph and applies it.
Box-level enclosure #
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_boxAdd
{B1 B2 : FlatBox ℝ}
{v1 v2 : Val}
(h1 : EnclosesBox B1 v1)
(h2 : EnclosesBox B2 v2)
(hxy : v1.n = v2.n)
:
EnclosesBox (boxAdd B1 B2) { n := v1.n, v := v1.v.addSpec (castDimScalar ⋯ v2.v) }
boxAdd encloses the sum of enclosed values with matching dimensions.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_boxSub
{B1 B2 : FlatBox ℝ}
{v1 v2 : Val}
(h1 : EnclosesBox B1 v1)
(h2 : EnclosesBox B2 v2)
(hxy : v1.n = v2.n)
:
EnclosesBox (boxSub B1 B2) { n := v1.n, v := v1.v.subSpec (castDimScalar ⋯ v2.v) }
boxSub encloses the difference of enclosed values with matching dimensions.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_boxMulElem
{B1 B2 Bm : FlatBox ℝ}
{v1 v2 : Val}
(h1 : EnclosesBox B1 v1)
(h2 : EnclosesBox B2 v2)
(hxy : v1.n = v2.n)
(hmul : boxMulElem B1 B2 = some Bm)
:
EnclosesBox Bm { n := v1.n, v := v1.v.mulSpec (castDimScalar ⋯ v2.v) }
A successful boxMulElem encloses the elementwise product of enclosed values.
Node-level soundness #
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.add_node_encloses
{nodes : Array Node}
{ps : ParamStore ℝ}
{cert : Array (Option (FlatBox ℝ))}
{inputs : Std.HashMap ℕ Val}
{vals : Array (Option Val)}
{k : ℕ}
{B : FlatBox ℝ}
{v : Val}
(hkKind : nodes[k]!.kind = IR.OpKind.add)
(hcertStep : certStepNode? nodes ps cert k = some B)
(hvalStep : evalNode? nodes ps inputs vals k = some v)
(hpe : ParentsEnclosed nodes cert vals k)
:
EnclosesBox B v
Certificate soundness at an add node.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.sub_node_encloses
{nodes : Array Node}
{ps : ParamStore ℝ}
{cert : Array (Option (FlatBox ℝ))}
{inputs : Std.HashMap ℕ Val}
{vals : Array (Option Val)}
{k : ℕ}
{B : FlatBox ℝ}
{v : Val}
(hkKind : nodes[k]!.kind = IR.OpKind.sub)
(hcertStep : certStepNode? nodes ps cert k = some B)
(hvalStep : evalNode? nodes ps inputs vals k = some v)
(hpe : ParentsEnclosed nodes cert vals k)
:
EnclosesBox B v
Certificate soundness at a sub node.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.mulElem_node_encloses
{nodes : Array Node}
{ps : ParamStore ℝ}
{cert : Array (Option (FlatBox ℝ))}
{inputs : Std.HashMap ℕ Val}
{vals : Array (Option Val)}
{k : ℕ}
{B : FlatBox ℝ}
{v : Val}
(hkKind : nodes[k]!.kind = IR.OpKind.mulElem)
(hcertStep : certStepNode? nodes ps cert k = some B)
(hvalStep : evalNode? nodes ps inputs vals k = some v)
(hpe : ParentsEnclosed nodes cert vals k)
:
EnclosesBox B v
Certificate soundness at a mulElem node.