TorchLean API

Docs HomeGuideExamplesGraphs

NN.Verification.LiRPA.Common

Shared LiRPA Certificate Helpers #

Small utilities used by the LiRPA certificate examples. The model graphs stay in their own modules; this file only contains the repeated artifact-checking and input-box plumbing.

source
def NN.Verification.LiRPA.naturalCenter (dim : ℕ) :
Spec.Tensor Float (Spec.Shape.dim dim Spec.Shape.scalar)

Center vector [1, 2, ..., dim], used by the small deterministic LiRPA examples.

Instances For
    source
    def NN.Verification.LiRPA.seedVectorInputBox (inputId dim : ℕ) (center : Spec.Tensor Float (Spec.Shape.dim dim Spec.Shape.scalar)) (eps : Float) (ps : MLTheory.CROWN.Graph.ParamStore Float) :
    MLTheory.CROWN.Graph.ParamStore Float

    Insert an L∞ input box around center into a graph parameter store.

    Instances For
      source
      def NN.Verification.LiRPA.seedNaturalInputBox (inputId dim : ℕ) (eps : Float) (ps : MLTheory.CROWN.Graph.ParamStore Float) :
      MLTheory.CROWN.Graph.ParamStore Float

      Insert an L∞ input box around [1, 2, ..., dim].

      Instances For
        source
        def NN.Verification.LiRPA.checkIBPCert (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (outId : ℕ) (path : String) (tol : Float := 1e-5) :
        IO Unit

        Recompute Lean IBP bounds and compare them against a JSON certificate.

        Instances For