Certificate Soundness: Elementwise Activation Nodes #
Operator cases relu, tanh, sigmoid, sin, and cos of the IBP certificate induction.
tanh and sigmoid share one box-level lemma about Runtime.Ops.IBP.mapMinmax for monotone
scalar maps; sin and cos use the Lipschitz enclosures from NonlinearOps.
Monotonicity of the scalar activations over the reals #
The scalar tanh specification is monotone over ℝ.
The scalar sigmoid specification is monotone over ℝ.
Box-level enclosure #
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_boxRelu
{B1 : FlatBox ℝ}
{v1 : Val}
(h1 : EnclosesBox B1 v1)
:
EnclosesBox (boxRelu B1) { n := v1.n, v := Activation.reluSpec v1.v }
boxRelu encloses the ReLU of an enclosed value.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_map_minmax
{B1 : FlatBox ℝ}
{v1 : Val}
(f : ℝ → ℝ)
(hf : Monotone f)
(h1 : EnclosesBox B1 v1)
:
EnclosesBox (toFlatBox B1.dim (Runtime.Ops.IBP.mapMinmax f (ofFlatBox B1)))
{ n := v1.n, v := TorchLean.Tensor.mapSpec f v1.v }
Endpoint min/max propagation encloses any monotone elementwise map of an enclosed value.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_ibp_tanh
{B1 : FlatBox ℝ}
{v1 : Val}
(h1 : EnclosesBox B1 v1)
:
EnclosesBox (toFlatBox B1.dim (Runtime.Ops.IBP.tanh (ofFlatBox B1))) { n := v1.n, v := Activation.tanhSpec v1.v }
The tanh IBP transfer encloses tanh of an enclosed value.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_ibp_sigmoid
{B1 : FlatBox ℝ}
{v1 : Val}
(h1 : EnclosesBox B1 v1)
:
EnclosesBox (toFlatBox B1.dim (Runtime.Ops.IBP.sigmoid (ofFlatBox B1))) { n := v1.n, v := Activation.sigmoidSpec v1.v }
The sigmoid IBP transfer encloses the sigmoid of an enclosed value.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_ibp_sin
{B1 : FlatBox ℝ}
{v1 : Val}
(h1 : EnclosesBox B1 v1)
:
EnclosesBox (toFlatBox B1.dim (Runtime.Ops.IBP.sin (ofFlatBox B1)))
{ n := v1.n, v := TorchLean.Tensor.mapSpec (fun (z : ℝ) => Real.sin z) v1.v }
The sin IBP transfer encloses sin of an enclosed value.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_ibp_cos
{B1 : FlatBox ℝ}
{v1 : Val}
(h1 : EnclosesBox B1 v1)
:
EnclosesBox (toFlatBox B1.dim (Runtime.Ops.IBP.cos (ofFlatBox B1)))
{ n := v1.n, v := TorchLean.Tensor.mapSpec (fun (z : ℝ) => Real.cos z) v1.v }
The cos IBP transfer encloses cos of an enclosed value.
Node-level soundness #
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.relu_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.relu)
(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 relu node.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.tanh_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.tanh)
(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 tanh node.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.sigmoid_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.sigmoid)
(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 sigmoid node.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.sin_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.sin)
(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 sin node.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.cos_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.cos)
(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 cos node.