Softplus and safeLog certificate steps #
Each proof reads the same parent values and boxes as the executable checker. Softplus uses one parent; safeLog also reads a scalar epsilon parent, whose enclosure is part of the induction hypothesis. The scalar inequalities and coordinatewise box arguments live in the imported module.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.softplus_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.softplus)
(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
A successful softplus certificate step encloses the corresponding semantic value.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.safeLog_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.safeLog)
(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
SafeLog uses the enclosure of its actual scalar epsilon parent in every coordinate.