TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.API.Verification.Lowering

Explicit Verification Lowering #

Low-level access to TorchLean's verifier graph. Most applications should import NN.API.Verification, train with trainer.train, then call trained.verify center (radius := r) (norm := .inf); import this module only when constructing or inspecting graph-level IBP/CROWN workflows directly.

source
def TorchLean.Verification.lowerForwardToIR {α : Type} [Storage α] [Context α] {σ τ : Shape} (model : nn.Sequential σ τ) (state : nn.State α (Runtime.Autograd.Model.Layers.Seq.stateShapes model)) :
Except String (LoweredIR α)

Lower a sequential model into checked verifier IR with one distinguished input.

Instances For
    source
    def TorchLean.Verification.lowerProgramToIR {α : Type} [Storage α] [Context α] {paramShapes : List Shape} {σ τ : Shape} (forwardProgram : Runtime.Autograd.Model.Program α (paramShapes ++ [σ]) τ) (state : nn.State α paramShapes) :
    Except String (LoweredIR α)

    Lower a custom forward program into checked verifier IR with one distinguished input.

    Instances For
      source
      def TorchLean.Verification.inputShape? {α : Type} [Storage α] [Context α] (lowered : LoweredIR α) :
      Except String Shape

      Dimensions of the distinguished verifier input node.

      Instances For
        source
        def TorchLean.Verification.runAffine {α : Type} [Storage α] [Context α] [NN.MLTheory.CROWN.BoundOps α] (lowered : LoweredIR α) (parameters : ParamStore α) (intervalBounds : Array (Option (FlatBox α))) :
        Except String (Array (Option (FlatAffine α)))

        Compute upper affine bounds after validating the lowered verifier input.

        The engine retains both sides internally so negative coefficients use the correct parent bound.

        Instances For
          source
          def TorchLean.Verification.runCROWN {α : Type} [Storage α] [Context α] [NN.MLTheory.CROWN.BoundOps α] [NN.MLTheory.CROWN.NonlinearBoundOps α] (lowered : LoweredIR α) (parameters : ParamStore α) (intervalBounds : Array (Option (FlatBox α))) :
          Except String (Array (Option (FlatAffineBounds α)))

          Compute nodewise CROWN bounds after validating the lowered verifier input.

          Instances For