NN.MLTheory.Robustness.Runtime

Executable Float-specialized utilities for the robustness specifications in NN.MLTheory.Robustness.Spec.

Robustness runtime utilities (Float)

This file specializes the polymorphic spec in NN.MLTheory.Robustness.Spec to Float and adds a few executable helpers used by experiments, examples, and command-line diagnostics.

It includes:

• deterministic specializations (norms/distances/balls), and
• small sampling-based helpers that compute empirical quantities (e.g. “max observed ratio” over a chosen sample set).

The sampling helpers return Except results computed from finite samples. An error records absent or non-finite evidence; a successful value is still empirical and does not provide a certificate or Prop-level guarantee.

def NN.MLTheory.Robustness.Runtime.tensorLinfNormFloat {s : Spec.Shape} (t : TorchLean.Tensor Float s) : Float

Runtime L∞ norm, defined by specializing the polymorphic spec to Float.

def NN.MLTheory.Robustness.Runtime.tensorL2NormFloat {s : Spec.Shape} (t : TorchLean.Tensor Float s) : Float

Runtime L2 norm with scaling before squaring. Finite entries do not overflow or underflow merely because their squares do. NaNs propagate; an infinite entry or an unrepresentable final norm still produces infinity.

def NN.MLTheory.Robustness.Runtime.tensorL2DistanceFloat {s : Spec.Shape} (t1 t2 : TorchLean.Tensor Float s) : Float

L2 distance (specialization of Robustness.Spec.tensorDistance).

def NN.MLTheory.Robustness.Runtime.tensorLinfDistanceFloat {s : Spec.Shape} (t1 t2 : TorchLean.Tensor Float s) : Float

L∞ distance (specialization of Robustness.Spec.tensorDistance).

def NN.MLTheory.Robustness.Runtime.inLinfBallFloat {s : Spec.Shape} (center : TorchLean.Tensor Float s) (ε : Float) (t : TorchLean.Tensor Float s) : Bool

Decide whether t lies in the closed L∞-ball of radius ε around center.

Empirical (sampling-based) helpers

def NN.MLTheory.Robustness.Runtime.Empirical.maxL2LipschitzRatio {s₁ s₂ : Spec.Shape} (f : TorchLean.Tensor Float s₁ → TorchLean.Tensor Float s₂) (pairs : Array (TorchLean.Tensor Float s₁ × TorchLean.Tensor Float s₁)) : Except String Float

Maximum observed $L^2$ Lipschitz ratio over a given finite array of input pairs.

This computes:

$$ \max_{(x,y)\in\mathrm{pairs}} \frac{\lVert f(x)-f(y)\rVert_2}{\lVert x-y\rVert_2} $$

Factually: this is a maximum over the provided pairs only; it is not a certified global bound.

Empty input, non-finite distances or ratios, and collections containing no positive input distance are reported as errors. Zero-distance pairs are ignored when another pair is informative.

def NN.MLTheory.Robustness.Runtime.Sampling.adjacentPairs {α : Type} (xs : Array α) : Array (α × α)

Turn an array with at least two elements #[x₀,x₁,…,x_{m-1}] into adjacent pairs [(x₀,x₁),(x₁,x₂),…,(x_{m-1},x₀)].

This is a small combinator that is useful when you want to turn a sample array into a set of “nearby pairs” for empirical ratio computations. Empty and singleton arrays return no pairs.