TorchLean API

Docs HomeGuideExamplesGraphs

NN.MLTheory.CROWN.Proofs.GraphCertSoundness.Semantics

Graph Certificate Semantics #

Value semantics for the verifier graph dialect over ℝ, together with the local semantic consistency predicate used by certificate soundness proofs.

Basic types and predicates #

We work over ℝ because it has the right order structure for “true” soundness theorems. The runtime checkers operate over Float (fast, executable), and can be used to connect a Python-produced floating certificate to the same computations in Lean.

source
@[reducible, inline]
abbrev NN.MLTheory.CROWN.Graph.CertSoundness.Val :
Type
Instances For
    source
    @[reducible, inline]
    abbrev NN.MLTheory.CROWN.Graph.CertSoundness.encloses (B : FlatBox ℝ) (x : Spec.Tensor ℝ (Spec.Shape.dim B.dim Spec.Shape.scalar)) :
    Prop

    Componentwise enclosure predicate for a tensor point inside a FlatBox.

    Instances For
      source
      def NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox (B : FlatBox ℝ) (v : Val) :
      Prop

      EnclosesBox B v means the value vector v lies inside the interval box B.

      We phrase enclosure using the existing Sem.encloses predicate, but our semantic values are FlatVecs (carrying their dimension as a Nat), so we also carry a dimension equality witness.

      Instances For

        Denotational (value) semantics for the verifier graph dialect #

        The semantics is defined as a safe Option evaluator:

        source
        def NN.MLTheory.CROWN.Graph.CertSoundness.getVal? (vals : Array (Option Val)) (pid : ℕ) :
        Option Val

        Safe lookup of a previously computed parent value.

        Instances For
          source
          noncomputable def NN.MLTheory.CROWN.Graph.CertSoundness.evalNode? (nodes : Array Node) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) (id : ℕ) :
          Option Val

          Value semantics for a single node in the supported dialect (over ℝ).

          Instances For
            source
            noncomputable def NN.MLTheory.CROWN.Graph.CertSoundness.evalGraph? (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) :
            Array (Option Val)

            Evaluate an entire graph in node-id order using evalNode?.

            Instances For

              Even though we provided an executable evalGraph?, the main soundness theorem below does not depend on it.

              Reason: proving properties about the foldl evaluator would introduce a lot of “bookkeeping” lemmas about Array.set! and list folds.

              Instead, we state soundness for any array vals that is a local model of the semantics step: each node’s value must equal evalNode? computed from its parents’ values.

              This is a standard technique in proof engineering: separate “semantic consistency” from “the particular implementation of the evaluator”.

              Local semantic consistency (SemLocalOK) #

              SemLocalOK g ps inputs vals means:

              For a DAG (and only for a DAG), this is exactly the property that vals is a valid interpretation of the graph semantics.

              Existence and uniqueness of vals are evaluator-correctness facts. This file proves the certificate theorem in the reusable form: for any semantic interpretation vals, a locally-correct certificate encloses it.

              source
              def NN.MLTheory.CROWN.Graph.CertSoundness.SemLocalOK (g : Graph) (ps : ParamStore ℝ) (inputs : Std.HashMap ℕ Val) (vals : Array (Option Val)) :
              Prop
              Instances For