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 concrete values computed from finite samples. They do not produce certificate checks or Prop-level guarantees.

def NN.MLTheory.Robustness.Runtime.tensorLinfNormFloat {s : Spec.Shape} (t : Spec.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 : Spec.Tensor Float s) : Float

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

def NN.MLTheory.Robustness.Runtime.l2Norm {s : Spec.Shape} : Spec.Tensor Float s → Float

Internal helper: L2 norm specialization reused by runtime wrappers in this module.

def NN.MLTheory.Robustness.Runtime.linfNorm {s : Spec.Shape} : Spec.Tensor Float s → Float

Internal helper: L∞ norm specialization reused by runtime wrappers in this module.

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

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

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

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

def NN.MLTheory.Robustness.Runtime.inL2BallFloat {s : Spec.Shape} (center : Spec.Tensor Float s) (ε : Float) (t : Spec.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 : Spec.Tensor Float s) (ε : Float) (t : Spec.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 : Spec.Tensor Float s₁ → Spec.Tensor Float s₂) (pairs : List (Spec.Tensor Float s₁ × Spec.Tensor Float s₁)) : Float

Maximum observed L2 Lipschitz ratio over a given finite list of input pairs.

This computes:

max_{(x,y) in pairs} ‖f x - f y‖₂ / ‖x - y‖₂

with the convention that a pair with ‖x-y‖₂ = 0 contributes 0.

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

Edge cases / conventions:

• If pairs = [], the result is 0 (the fold's initial value).
• If a particular pair satisfies x = y (so the input distance is 0), that pair contributes 0.

Sampling design (why these helpers look “complicated”)

The spec tensor representation Spec.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. convert the type-level shape s : Shape into a runtime shape list shapeList s : List Nat,
2. compute the number of scalar entries numel s as the product of those dimensions, then
3. construct a flat list xs : List Float of length numel s,
4. unflatten it back into a tensor of the appropriate shape.

Correctness (what is and is not guaranteed):

• Every point returned by sampleL2Ball provably satisfies the predicate in_l2_ball_float 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.shapeList (s : Spec.Shape) : List ℕ

Runtime view of a type-level Shape (same convention as TensorBridge.shapeToList).

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

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

This is the runtime analogue of Spec.Shape.size. We compute it via TensorArray.shapeProd on the list view of the shape.

def NN.MLTheory.Robustness.Runtime.Sampling.castToListShape {s : Spec.Shape} : Spec.Tensor Float s → Spec.Tensor Float (TensorBridge.listToShape (shapeList s))

Cast a tensor with type-level shape s into the definitional-equal “list-shaped” view used by TensorBridge.flatten/unflatten.

This cast is purely a type-level transport; it does not change the tensor values.

def NN.MLTheory.Robustness.Runtime.Sampling.castFromListShape {s : Spec.Shape} : Spec.Tensor Float (TensorBridge.listToShape (shapeList s)) → Spec.Tensor Float s

Inverse cast: transport a “list-shaped” tensor back to the original type-level shape s.

def NN.MLTheory.Robustness.Runtime.Sampling.perturbDirection (n seed : ℕ) : List 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.l2NormList (xs : List Float) : Float

Euclidean norm of a flat list (helper for normalization).

def NN.MLTheory.Robustness.Runtime.Sampling.normalizeList (xs : List Float) : List Float

Normalize a flat list 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 : List Float) (h : xs.length = TensorArray.shapeProd (shapeList s)) : Spec.Tensor Float s

Unflatten a flat list of length numel s into a Spec.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 : ℕ) : Spec.Tensor Float s

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

Construction:

1. Make a flat “direction” list 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 : Spec.Tensor Float s) (ε : Float) (numSamples : ℕ) : List (Spec.Tensor Float s)

Generate candidate samples in the closed L2 ball around center (deterministic sampler).

We generate numSamples candidates, each constructed as:

center + δ_k where δ_k is a direction derived from k and then scaled to a radius in [0, ε].

We then filter candidates using in_l2_ball_float 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} : List α → List (α × α)

Turn a nonempty list [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 list into a set of “nearby pairs” for empirical ratio computations.

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

Empirical max “gain from the center” on a sampled L2-ball neighborhood.

This computes:

max_{x in samples} ‖f x - f x₀‖₂ / ‖x - x₀‖₂

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