Graph IBP Certificate Soundness

The induction theorem: local IBP certificate consistency plus local semantic consistency implies that every certified node box encloses the corresponding semantic value.

Main theorem: local IBP certificate implies semantic enclosure (supported subset)

We use strong induction on node id, assuming a topological order: every parent id is strictly smaller than the node id.

def NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted (g : Graph) : Prop

Topological order assumption: all parent ids are strictly smaller than the node id.

def NN.MLTheory.CROWN.Graph.CertSoundness.Supported (g : Graph) : Prop

A graph is supported by this soundness theorem if every node kind is in our supported subset.

def NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) : Prop

Inputs are well-formed if every .input node has a value, and that value is enclosed by its input box from ParamStore.inputBoxes.

The enclosure theorem

Assumptions:

• TopoSorted g: induction works (parents are earlier).
• Supported g: every node kind is handled by the proof.
• CertLocalOK g ps cert: the certificate is locally consistent with the IBP step.
• InputsEnclosed g ps inputs: semantic inputs are inside the certified input boxes.
• SemLocalOK g ps inputs vals: vals is a locally-consistent semantic interpretation.

Conclusion:

• For every node id, if the semantics produces a value v and the certificate has a box B, then B encloses v.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.cert_encloses_semantics (g : Graph) (ps : ParamStore ℝ) (cert : Array (Option (FlatBox ℝ))) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) (htopo : TopoSorted g) (hsupp : Supported g) (hcert : CertLocalOK g ps cert) (hsem : SemLocalOK g ps inputs vals) (hinputs : InputsEnclosed g ps inputs) (id : ℕ) : id < g.nodes.size → match cert[id]!, vals[id]! with | some B, some v => EnclosesBox B v | x, x_1 => True