NN.MLTheory.Robustness.Spec

Scalar-polymorphic definitions of norms/distances and basic robustness vocabulary on TorchLean's shape-indexed tensors.

Robustness specifications (polymorphic)

This file defines a small vocabulary for specifying robustness properties of tensor-valued functions.

All definitions are scalar-polymorphic in α via [Context α], so the same spec can be instantiated for:

• ℝ (paper-style theorems),
• Float (fast, executable sanity checks),
• Interval (sound enclosures for verification),
• executable IEEE-754 backends (bit-level runtime semantics).

We keep this module definition-focused: whether these norms/distances satisfy the usual metric laws depends on additional algebraic/order assumptions on α, and those theorems belong in dedicated proof developments.

The Float specializations of these definitions live in NN.MLTheory.Robustness.Runtime.

Verified bounds/certificates are proved in dedicated developments (e.g. Lipschitz bounds in NN.Proofs.Analysis.Lipschitz, and certified robustness procedures in NN.MLTheory.CROWN).

References

• Adversarial examples and threat models: Szegedy et al. (2013/2014); Goodfellow, Shlens & Szegedy (2015, FGSM); Madry et al. (2017).
• Certified robustness / verification: Wong & Kolter (2018); Cohen, Rosenfeld & Kolter (2019).
• Lipschitz-based viewpoints (one entry point): Hein & Andriushchenko (2017).

Norms on spec tensors

def NN.MLTheory.Robustness.Spec.tensorLinfNorm {α : Type} [Context α] {s : Spec.Shape} (t : Spec.Tensor α s) : α

L∞ norm of a shape-indexed tensor.

If you flatten the tensor entries into a vector tᵢ, this is maxᵢ |tᵢ|.

def NN.MLTheory.Robustness.Spec.tensorL2Norm {α : Type} [Context α] {s : Spec.Shape} (t : Spec.Tensor α s) : α

L2 (Euclidean) norm of a shape-indexed tensor.

If you flatten the tensor entries into a vector tᵢ, this is sqrt (∑ᵢ tᵢ²).

def NN.MLTheory.Robustness.Spec.tensorL2Norm.tensor_l2_norm_squared {α : Type} [Context α] {s : Spec.Shape} (t : Spec.Tensor α s) : α

Distances and balls

def NN.MLTheory.Robustness.Spec.tensorDistance {α : Type} [Context α] (norm : {s : Spec.Shape} → Spec.Tensor α s → α) {s : Spec.Shape} (t1 t2 : Spec.Tensor α s) : α

Distance induced by a tensor norm:

dist(t1,t2) = ‖t1 - t2‖.

def NN.MLTheory.Robustness.Spec.tensorDistance.tensor_sub {α : Type} [Context α] {s : Spec.Shape} : Spec.Tensor α s → Spec.Tensor α s → Spec.Tensor α s

@[simp]

theorem NN.MLTheory.Robustness.Spec.tensor_distance_tensor_sub_eq_sub_spec {α : Type} [Context α] {s : Spec.Shape} (t1 t2 : Spec.Tensor α s) : tensorDistance.tensor_sub t1 t2 = t1.subSpec t2

@[simp]

theorem NN.MLTheory.Robustness.Spec.tensor_distance_eq_norm_sub_spec {α : Type} [Context α] (norm : {s : Spec.Shape} → Spec.Tensor α s → α) {s : Spec.Shape} (t1 t2 : Spec.Tensor α s) : tensorDistance (fun {s : Spec.Shape} => norm) t1 t2 = norm (t1.subSpec t2)

def NN.MLTheory.Robustness.Spec.tensorBall {α : Type} [Context α] (norm : {s : Spec.Shape} → Spec.Tensor α s → α) {s : Spec.Shape} (center : Spec.Tensor α s) (ε : α) : Set (Spec.Tensor α s)

Closed ε-ball around center for the given norm:

{ t | dist(center,t) ≤ ε }.

Continuity / robustness specifications

def NN.MLTheory.Robustness.Spec.isLipschitzContinuous {α : Type} [Context α] {s₁ s₂ : Spec.Shape} (f : Spec.Tensor α s₁ → Spec.Tensor α s₂) (norm₁ norm₂ : {s : Spec.Shape} → Spec.Tensor α s → α) (L : α) : Prop

Lipschitz continuity (global), phrased using tensor_distance.

If f is L-Lipschitz and tensor_distance norm₁ x₀ x ≤ ε, then tensor_distance norm₂ (f x₀) (f x) ≤ L*ε.

def NN.MLTheory.Robustness.Spec.isLocallyLipschitz {α : Type} [Context α] {s₁ s₂ : Spec.Shape} (f : Spec.Tensor α s₁ → Spec.Tensor α s₂) (norm₁ norm₂ : {s : Spec.Shape} → Spec.Tensor α s → α) (x₀ : Spec.Tensor α s₁) (ε L : α) : Prop

Local Lipschitz continuity within the ε-ball around x₀.

def NN.MLTheory.Robustness.Spec.isAdversariallyRobust {α : Type} [Context α] {s₁ s₂ : Spec.Shape} (f : Spec.Tensor α s₁ → Spec.Tensor α s₂) (norm₁ norm₂ : {s : Spec.Shape} → Spec.Tensor α s → α) (x₀ : Spec.Tensor α s₁) (ε δ : α) : Prop

Adversarial robustness at a point x₀.

f is (ε,δ)-robust at x₀ if every input within distance ε of x₀ maps to an output within distance δ of f x₀.

def NN.MLTheory.Robustness.Spec.isCertifiedRobust {α : Type} [Context α] {s : Spec.Shape} (classifier : Spec.Tensor α s → ℕ) (norm : {s : Spec.Shape} → Spec.Tensor α s → α) (x₀ : Spec.Tensor α s) (ε : α) : Prop

Certified robustness for a classifier: the prediction is constant on the ε-ball around x₀.

For neural networks, classifier is typically argmax on a logits tensor.

def NN.MLTheory.Robustness.Spec.isUniformlyRobust {α : Type} [Context α] {s₁ s₂ : Spec.Shape} (f : Spec.Tensor α s₁ → Spec.Tensor α s₂) (norm₁ norm₂ : {s : Spec.Shape} → Spec.Tensor α s → α) (dataset : List (Spec.Tensor α s₁)) (ε δ : α) : Prop

Uniform adversarial robustness over a finite list of inputs.

def NN.MLTheory.Robustness.Spec.isContractive {α : Type} [Context α] {s : Spec.Shape} (f : Spec.Tensor α s → Spec.Tensor α s) (norm : {s : Spec.Shape} → Spec.Tensor α s → α) (contraction_factor : α) : Prop

Contraction mapping under a norm: f shrinks distances by contraction_factor < 1.

This is a standard sufficient condition for convergence of iterated dynamics and robustness of fixed points.

def NN.MLTheory.Robustness.Spec.sensitivity {α : Type} [Context α] {s₁ s₂ : Spec.Shape} (f : Spec.Tensor α s₁ → Spec.Tensor α s₂) (norm₁ norm₂ : {s : Spec.Shape} → Spec.Tensor α s → α) (x perturbation : Spec.Tensor α s₁) : α

Sensitivity ratio for a specific additive perturbation.

This is the local “output change divided by input change” quantity:

‖f(x) - f(x + perturbation)‖ / ‖perturbation‖.