Verification

Convenience names for compiling TorchLean models into IBP/CROWN checks.

def TorchLean.Verification.compileForward {α : Type} [Context α] [DecidableEq Shape] {σ τ : Shape} (model : nn.Sequential σ τ) (params : TensorPack α (Runtime.Autograd.TorchLean.NN.Seq.paramShapes model)) : Except String (CompiledIR α)

Compile a sequential TorchLean model into verifier IR with one distinguished input.

Usual "train a model, then run IBP/CROWN on its forward pass" path.

def TorchLean.Verification.compileProgram {α : Type} [Context α] [DecidableEq Shape] {paramShapes : List Shape} {σ τ : Shape} (forwardProgram : Runtime.Autograd.TorchLean.Program α (paramShapes ++ [σ]) τ) (params : TensorPack α paramShapes) : Except String (CompiledIR α)

Compile a custom TorchLean forward program into verifier IR with one distinguished input.

Use this when the target is not a plain TorchLean.nn.Sequential, for example a hand-written loss program or an attention fragment built directly from TorchLean.Ops.

def TorchLean.Verification.seedInputBox {α : Type} [Context α] (compiled : CompiledIR α) (xB : FlatBox α) : ParamStore α

Seed the verifier input with an explicit input box.

Call this after compileForward, then hand the returned store to IBP/CROWN passes.

def TorchLean.Verification.lInfBox {α : Type} [Context α] {s : Shape} (center radius : Spec.Tensor α s) : FlatBox α

Flatten a center tensor and radius tensor into the FlatBox expected by IBP/CROWN.

Use this for a shaped TorchLean input with a shaped perturbation radius.

def TorchLean.Verification.lInfBall {α : Type} [Context α] {s : Shape} (center : Spec.Tensor α s) (eps : α) : FlatBox α

Build a uniform $\ell^\infty$ box around a shaped TorchLean input tensor.

This fills the input shape with the scalar radius eps, then flattens it into a verifier box.

def TorchLean.Verification.seedLInfBall {α : Type} [Context α] {s : Shape} (compiled : CompiledIR α) (center : Spec.Tensor α s) (eps : α) : ParamStore α

Seed the compiled verifier input with a uniform $\ell^\infty$ box around a shaped TorchLean input tensor.

def TorchLean.Verification.inputShape? {α : Type} [Context α] (compiled : CompiledIR α) : Except String Shape

Shape of the distinguished verifier input node.

def TorchLean.Verification.inputDim? {α : Type} [Context α] (compiled : CompiledIR α) : Except String ℕ

Flattened dimension of the distinguished verifier input node.

def TorchLean.Verification.affineCtx? {α : Type} [Context α] (compiled : CompiledIR α) : Except String AffineCtx

Affine context for the distinguished verifier input.

def TorchLean.Verification.runIBP {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] [NN.MLTheory.CROWN.NonlinearBoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) : Array (Option (FlatBox α))

Run IBP on a compiled verifier graph.

def TorchLean.Verification.outputBox? {α : Type} [Context α] (compiled : CompiledIR α) (boxes : Array (Option (FlatBox α))) : Except String (FlatBox α)

Read the verifier output box from an IBP result array.

def TorchLean.Verification.outputBoxOrThrow {α : Type} [Context α] (compiled : CompiledIR α) (boxes : Array (Option (FlatBox α))) : IO (FlatBox α)

Read the verifier output box, throwing an IO.userError if it is missing.

def TorchLean.Verification.runAffine {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) : Except String (Array (Option (FlatAffine α)))

Run the forward affine pass after validating the compiled verifier input.

def TorchLean.Verification.outputAffine? {α : Type} [Context α] (compiled : CompiledIR α) (affs : Array (Option (FlatAffine α))) : Except String (FlatAffine α)

Read the verifier output affine form from a forward affine result array.

def TorchLean.Verification.runCROWN {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] [NN.MLTheory.CROWN.NonlinearBoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) : Except String (Array (Option (FlatAffineBounds α)))

Run CROWN after validating the compiled verifier input.

def TorchLean.Verification.outputCROWN? {α : Type} [Context α] (compiled : CompiledIR α) (bounds : Array (Option (FlatAffineBounds α))) : Except String (FlatAffineBounds α)

Read the verifier output CROWN bounds from a CROWN result array.

def TorchLean.Verification.outputBoxCROWN? {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] [NN.MLTheory.CROWN.NonlinearBoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (xB : FlatBox α) : Except String (FlatBox α)

Run forward CROWN and evaluate the verifier output bounds on the compiled input box.

def TorchLean.Verification.outputBoxCROWNOrThrow {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] [NN.MLTheory.CROWN.NonlinearBoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (xB : FlatBox α) : IO (FlatBox α)

Run forward CROWN and return the evaluated verifier output box, throwing on failure.

def TorchLean.Verification.backwardObjectiveBox? {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (xB : FlatBox α) (obj : NN.MLTheory.CROWN.Graph.FlatVec α) : Except String (FlatBox α)

Run backward CROWN for a scalar objective and evaluate it on the compiled input box.

def TorchLean.Verification.backwardObjectiveBoxOrThrow {α : Type} [Context α] [NN.MLTheory.CROWN.BoundOps α] (compiled : CompiledIR α) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (xB : FlatBox α) (obj : NN.MLTheory.CROWN.Graph.FlatVec α) : IO (FlatBox α)

IO version of backwardObjectiveBox?.

def TorchLean.Verification.twoClassMarginLowerBound {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Shape.scalar)) (class0 class1 : Fin n) : α

Compute the conservative two-class margin lower bound $\mathrm{lo}[\mathrm{class0}]-\mathrm{hi}[\mathrm{class1}]$.

If this is positive, class class0 is certified against class1 over the input box.

def TorchLean.Verification.certifiesTwoClassMargin {α : Type} [Context α] {n : ℕ} (lo hi : Spec.Tensor α (Spec.Shape.dim n Shape.scalar)) (class0 class1 : Fin n) : Bool

Decide whether the two-class margin lower bound is strictly positive.