Verification

The public vocabulary used by trained-model verification. Ordinary code calls trained.verify center (radius := r) (norm := linf) and adds named choices only when needed. Report retains those choices with the returned bounds; explicit graph lowering is intentionally separate in NN.API.Verification.Lowering.

inductive TorchLean.Verification.Algorithm : Type

Bound-propagation algorithm used to construct a verification report.

• ibp : Algorithm

  Fast interval bound propagation.

• crown : Algorithm

  CROWN output bounds: forward affine on exact backends, directed backward on rounded ones.

• alphaCrown : Algorithm

  Fixed-relaxation alpha-CROWN with the ReLU phases IBP proves. No phase beyond IBP is assumed, so no beta split and no branch-and-bound search runs. Reports print it as Alpha-CROWN (IBP phases). On a rounded scalar it runs directed CROWN instead, and the report says CROWN.

@[instance_reducible]

instance TorchLean.Verification.instDecidableEqAlgorithm : DecidableEq Algorithm

def TorchLean.Verification.instReprAlgorithm.repr : Algorithm → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Verification.instReprAlgorithm : Repr Algorithm

def TorchLean.Verification.Algorithm.name : Algorithm → String

Human-readable method name used in reports.

@[instance_reducible]

instance TorchLean.Verification.Algorithm.instToString : ToString Algorithm

inductive TorchLean.Verification.Norm : Type

Norm of the input region requested for verification.

The current native CROWN path implements linf; the other cases remain part of the request language so adding a non-box region does not require another public API.

• l1 : Norm

  L1 input ball.

• l2 : Norm

  L2 input ball.

• linf : Norm

  L-infinity input ball.

@[instance_reducible]

instance TorchLean.Verification.instDecidableEqNorm : DecidableEq Norm

def TorchLean.Verification.instReprNorm.repr : Norm → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Verification.instReprNorm : Repr Norm

def TorchLean.Verification.Norm.name : Norm → String

Human-readable norm name used in reports and diagnostics.

@[instance_reducible]

instance TorchLean.Verification.Norm.instToString : ToString Norm

inductive TorchLean.Verification.Property : Type

Property evaluated from output bounds.

outputBounds returns the complete output enclosure. topLabel label additionally asks whether one flattened output stays strictly above every competing output.

• outputBounds : Property

  Return the output enclosure without an additional assertion.

• topLabel (label : ℕ) : Property

  Check that label remains the unique largest flattened output.

@[instance_reducible]

instance TorchLean.Verification.instDecidableEqProperty : DecidableEq Property

def TorchLean.Verification.instDecidableEqProperty.decEq (x✝ x✝¹ : Property) : Decidable (x✝ = x✝¹)

def TorchLean.Verification.instReprProperty.repr : Property → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Verification.instReprProperty : Repr Property

def TorchLean.Verification.Property.name : Property → String

Human-readable property description used in reports.

@[instance_reducible]

instance TorchLean.Verification.Property.instToString : ToString Property

def TorchLean.Verification.Internal.validateRadius (radius : Float) : Except String Unit

Reject an invalid input-region radius before verification begins.

structure TorchLean.Verification.Bounds : Type

Componentwise lower and upper bounds for a flattened model output.

• size : ℕ

  Shared number of flattened output components.

• lower : Tensor Float [self.size]

  Componentwise lower output bounds.

• upper : Tensor Float [self.size]

  Componentwise upper output bounds.

def TorchLean.Verification.instReprBounds.repr : Bounds → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Verification.instReprBounds : Repr Bounds

def TorchLean.Verification.Bounds.validate (bounds : Bounds) : Except String Unit

Check the basic consistency needed by public reporting helpers.

def TorchLean.Verification.Bounds.maxOther? {n : ℕ} (values : Tensor Float [n]) (label : ℕ) : Option Float

Largest output value other than label.

inductive TorchLean.Verification.Result : Type

Result of evaluating a requested output property from valid bounds.

• bounds : Result

  The report contains an output enclosure but no additional assertion.

• topLabel (label : ℕ) (margin : Float) (certified : Bool) : Result

  A top-label assertion with its computed margin and strict-positivity test. The binary64 difference may overflow to infinity even when both endpoints are finite.

def TorchLean.Verification.instReprResult.repr : Result → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Verification.instReprResult : Repr Result

def TorchLean.Verification.Result.summary : Result → String

One-line rendering of a verification result.

@[instance_reducible]

instance TorchLean.Verification.Result.instToString : ToString Result

def TorchLean.Verification.Result.fromBounds (property : Property) (bounds : Bounds) : Except String Result

Evaluate a public property against componentwise output bounds.

structure TorchLean.Verification.Report : Type

Complete report returned by trained.verify.

• radius : Float

  Radius of the checked input region around the supplied center tensor.

• norm : Norm

  Norm used to define the checked input region.

• property : Property

  Output property evaluated from the output enclosure.

• algorithm : Algorithm

  Bound-propagation algorithm that produced the enclosure.

• bounds : Bounds

  Output enclosure produced by the selected algorithm.

• result : Result

  Chosen property evaluated from the output enclosure.

@[instance_reducible]

instance TorchLean.Verification.instReprReport : Repr Report

def TorchLean.Verification.instReprReport.repr : Report → ℕ → Std.Format

def TorchLean.Verification.Report.fromBounds (radius : Float) (bounds : Bounds) (norm : Norm := linf) (property : Property := outputBounds) (algorithm : Algorithm := alphaCrown) : Except String Report

Build a report after checking the radius and consistency of the supplied output bounds.

The caller supplies the enclosure guarantee; these checks do not establish it.

def TorchLean.Verification.Report.summary (report : Report) : String

One-line human-readable verification summary.

def TorchLean.Verification.Report.printSummary (report : Report) : IO Unit

Print the concise verification summary.

@[instance_reducible]

instance TorchLean.Verification.Report.instToString : ToString Report