TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.API.Verification.Execution

Verification Execution #

Implementation support for the public trained.verify operation. The public named arguments are lowered into a verifier input region and returned as a validated Verification.Report.

Applications should import NN.API.Verification and call trained.verify center (radius := r) (norm := .inf). Direct verifier graph construction remains in NN.API.Verification.Lowering.

source
def TorchLean.Verification.Internal.readBounds {α : Type} [Storage α] [Context α] [Runtime.Autograd.Torch.TensorTransfer α] (box : NN.MLTheory.CROWN.FlatBox α) :
IO Bounds

Convert an internal flat interval into the public host-Float bounds representation.

Instances For
    source
    def TorchLean.Verification.Internal.forState {σ τ : Shape} {α : Type} [Storage α] [Context α] [Runtime.FromFloat α] [Runtime.Autograd.Torch.TensorTransfer α] [NN.MLTheory.CROWN.BoundOps α] [NN.MLTheory.CROWN.NonlinearBoundOps α] (trainer : Trainer σ τ) (modelState : nn.State α (Runtime.Autograd.Model.Layers.Seq.stateShapes trainer.model)) (center : Tensor Float σ) (radius : Float) (norm : Norm) (property : Property) (algorithm : Algorithm) :
    IO Report

    Build the verification closure retained by an ordinary trained result.

    The closure captures the completed parameter snapshot, so subsequent updates to the training session cannot change the model being verified.

    Instances For