Certificate Soundness: Affine Nodes #
Operator cases linear, matmul, and concat of the IBP certificate induction. Linear maps
reduce to IBP.linear with a point bias box. Concatenation transports parent enclosures through
the same coordinate bijection used by the executable CROWN passes.
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.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_concat
{layout : ConcatLayout}
{boxes : Array (FlatBox ℝ)}
{values : Array Val}
{B : FlatBox ℝ}
{v : Val}
(hboxes : concatFlatBoxes? layout boxes = some B)
(hvalues : concatFlatValues? layout values = some v)
(hparents : ∀ (i : ℕ) (Bp : FlatBox ℝ) (vp : Val), boxes[i]? = some Bp → values[i]? = some vp → EnclosesBox Bp vp)
:
EnclosesBox B v
The checked flat concat preserves enclosure for every parent occurrence.
Node-level soundness #
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.concat_node_encloses
{nodes : Array Node}
{ps : ParamStore ℝ}
{cert : Array (Option (FlatBox ℝ))}
{inputs : Std.HashMap ℕ Val}
{vals : Array (Option Val)}
{k axis : ℕ}
{B : FlatBox ℝ}
{v : Val}
(hkKind : nodes[k]!.kind = IR.OpKind.concat axis)
(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 for concat on any validated axis and number of parent occurrences.
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.