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, defined by specializing the polymorphic spec to Float.

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.inL2BallFloat {s : Spec.Shape} (center : TorchLean.Tensor Float s) (ε : Float) (t : TorchLean.Tensor Float s) : Bool

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

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.

Sampling design (why these helpers look “complicated”)

The spec tensor representation TorchLean.Tensor α s is shape-indexed and is represented functionally (Fin n → ...). That is great for proofs, but it is not the easiest shape to work with when you want to build concrete perturbations of a fixed length at runtime.

For sampling, we therefore go through a standard interop path:

1. compute the scalar count numel s from the tensor shape,
2. construct a flat array xs : Array Float of that length, then
3. use the checked flat-data constructor to obtain a tensor of shape s.

Correctness (what is and is not guaranteed):

• Every point returned by sampleL2Ball provably satisfies the predicate inL2BallFloat center ε because we filter candidates using that very predicate.
• The sampler is deterministic (no IO randomness). You control variability via the seed input (here derived from the loop index).
• The sampler is not intended to approximate a uniform distribution on the ball, and it does not attempt to be “complete” in any verification sense: it is purely an empirical exploration tool to produce inputs for downstream checks/counterexamples.

def NN.MLTheory.Robustness.Runtime.Sampling.numel (s : Spec.Shape) : ℕ

Number of scalar elements (“numel”) in a tensor of shape s.

def NN.MLTheory.Robustness.Runtime.Sampling.perturbDirection (n seed : ℕ) : Array Float

Deterministically generate a length-n direction vector from a seed.

This is not cryptographic and not intended to model a probabilistic distribution; it is a deterministic way to generate reproducible, varied directions without introducing IO.

def NN.MLTheory.Robustness.Runtime.Sampling.l2NormArray (xs : Array Float) : Float

Euclidean norm of a flat runtime array.

def NN.MLTheory.Robustness.Runtime.Sampling.normalizeArray (xs : Array Float) : Array Float

Normalize a flat array to unit L2 norm (when possible).

If the list has zero norm, we return it unchanged.

def NN.MLTheory.Robustness.Runtime.Sampling.unflattenToTensor {s : Spec.Shape} (xs : Array Float) (h : xs.size = s.size) : TorchLean.Tensor Float s

Unflatten a flat array of length numel s into a TorchLean.Tensor Float s.

The length proof is part of the interface to avoid “silent truncation/padding”.

def NN.MLTheory.Robustness.Runtime.Sampling.perturbationTensor {s : Spec.Shape} (radius : Float) (seed : ℕ) : TorchLean.Tensor Float s

Build a perturbation tensor of (approximately) the given radius, deterministically from seed.

Construction:

1. Make a flat direction array base of length numel s.
2. Normalize it to unit norm (when nonzero).
3. Scale by radius.
4. Unflatten back into the tensor shape.

This ensures the perturbation has the right shape by construction.

def NN.MLTheory.Robustness.Runtime.Sampling.sampleL2Ball {s : Spec.Shape} (center : TorchLean.Tensor Float s) (ε : Float) (numSamples : ℕ) : Array (TorchLean.Tensor Float s)

Generate candidate samples in the closed $L^2$ ball around center (deterministic sampler).

We generate numSamples candidates, each constructed as:

$\mathrm{center}+\delta_k$, where $\delta_k$ is a direction derived from $k$ and then scaled to a radius in $[0,\varepsilon]$.

We then filter candidates using inL2BallFloat center ε to ensure that every returned element satisfies the predicate under the same runtime distance function.

This “generate + filter” style is deliberate: it makes the only factual guarantee we claim extremely clear (“every returned element lies in the ball”), independent of the details of the direction generator.

def NN.MLTheory.Robustness.Runtime.Sampling.adjacentPairs {α : Type} [Inhabited α] (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.

def NN.MLTheory.Robustness.Runtime.empiricalMaxL2GainFromSamples {s₁ s₂ : Spec.Shape} (f : TorchLean.Tensor Float s₁ → TorchLean.Tensor Float s₂) (x₀ : TorchLean.Tensor Float s₁) (ε : Float) (numSamples : ℕ) : Except String Float

Empirical max “gain from the center” on a sampled $L^2$-ball neighborhood.

This computes:

$$ \max_{x\in\mathrm{samples}} \frac{\lVert f(x)-f(x_0)\rVert_2}{\lVert x-x_0\rVert_2} $$

where samples are generated by Sampling.sampleL2Ball. This is a maximum over those samples only (not a certified global Lipschitz bound).