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 reusable 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 consistency 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^\infty$ norm of a shape-indexed tensor.

If you flatten the tensor entries into a vector $t_i$, this is $\max_i |t_i|$.

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

$L^2$ (Euclidean) norm of a shape-indexed tensor.

If you flatten the tensor entries into a vector $t_i$, this is $\sqrt{\sum_i t_i^2}$.

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:

$$ \operatorname{dist}(t_1,t_2)=\lVert t_1-t_2\rVert. $$

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 $\varepsilon$-ball around center for the given norm:

$$ \{t\mid \operatorname{dist}(\mathrm{center},t)\leq\varepsilon\}. $$

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 $d_1(x_0,x)\leq\varepsilon$, then $d_2(f(x_0),f(x))\leq L\varepsilon$.

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 $\varepsilon$-ball around $x_0$.

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_0$.

$f$ is $(\varepsilon,\delta)$-robust at $x_0$ if every input within distance $\varepsilon$ of $x_0$ maps to an output within distance $\delta$ of $f(x_0)$.

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 $\varepsilon$-ball around $x_0$.

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 a factor $c<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:

$$ \frac{\lVert f(x)-f(x+\mathrm{perturbation})\rVert} {\lVert\mathrm{perturbation}\rVert}. $$