Certificate soundness for convolution #
The interval and value evaluators use the same checked convolution payload and leading shape. The node enclosure theorem therefore applies after reconstructing the semantic input tensor. Parent lookup and the certificate induction supply its input enclosure.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.ibpConvNode_encloses_evalConvNode
{configuration : IR.ConvConfig}
{parentShape outShape : Spec.Shape}
{id : ℕ}
{ps : ParamStore ℝ}
{Xin Bout : FlatBox ℝ}
{input output : Val}
(hinput : EnclosesBox Xin input)
(hout : ibpConvNode configuration parentShape outShape id ps Xin = some Bout)
(hvalue : evalConvNode? configuration parentShape outShape id ps input = some output)
:
EnclosesBox Bout output
The checked interval convolution encloses the checked value convolution on an enclosed flat input, including all dimension casts performed by both evaluators.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.conv_node_encloses
{nodes : Array Node}
{ps : ParamStore ℝ}
{cert : Array (Option (FlatBox ℝ))}
{inputs : Std.HashMap ℕ Val}
{vals : Array (Option Val)}
{k : ℕ}
{configuration : IR.ConvConfig}
{B : FlatBox ℝ}
{v : Val}
(hkKind : nodes[k]!.kind = IR.OpKind.conv configuration)
(hcertStep : certStepNode? nodes ps cert k = some B)
(hvalStep : evalNode? nodes ps inputs vals k = some v)
(hparents : ParentsEnclosed nodes cert vals k)
:
EnclosesBox B v
Certificate soundness at a convolution node with successfully validated payload geometry.