Certificate Soundness: Affine Nodes #
Operator cases linear and matmul of the IBP certificate induction. Both reduce to one
box-level lemma about IBP.linear with a point bias box; matmul instantiates the bias with the
zero vector.
Box-level enclosure #
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_ibp_linear
{B1 : FlatBox ℝ}
{v1 : Val}
{m n : ℕ}
(W : TorchLean.Tensor ℝ [m, n])
(b : TorchLean.Tensor ℝ [m])
(h1 : EnclosesBox B1 v1)
(hXin : B1.dim = n)
(hxDim : v1.n = n)
:
EnclosesBox (toFlatBox m (IBP.linear W (castBoxDim hXin (ofFlatBox B1)) (Box.point b)))
{ n := m, v := Spec.linearSpec { weights := W, bias := b } (castDimScalar hxDim v1.v) }
IBP.linear with a point bias box encloses the affine image of an enclosed value, once the
input box and the value are cast to the weight's input dimension.
Node-level soundness #
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.linear_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.linear)
(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 linear node.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.matmul_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.matmul)
(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 matmul node.