Affine Arithmetic: Vector Operations

This file provides vectorized affine operations for efficient neural network verification. The key insight is that shared noise symbols track correlations across vector elements.

The Dependency Problem in Vectors

Consider LayerNorm: y_i = (x_i - μ) / σ where μ = mean(x).

With standard interval arithmetic:

• x_i ∈ [0.9, 1.1] for all i
• μ ∈ [0.9, 1.1]
• x_i - μ ∈ [-0.2, 0.2] (WRONG! Should be nearly 0)

With Affine Arithmetic:

• x_i = 1.0 + 0.1·ε_i (each element has its own noise)
• μ = 1.0 + 0.1·(ε_1 + ... + ε_n)/n
• x_i - μ = 0.1·ε_i - 0.1·(ε_1 + ... + ε_n)/n (TIGHT!)

Main definitions

• AffineVector - Vector of affine forms with shared noise symbols
• AffineVector.mean - Compute mean preserving correlations
• AffineVector.sub - Element-wise subtraction
• AffineVector.layerNorm - LayerNorm with proper dependency tracking

Affine Vector

@[reducible, inline]

abbrev LeanCert.Engine.Affine.AffineVector : Type

A vector of affine forms sharing the same noise symbol space.

All elements should have the same coeffs.length (number of noise symbols). This ensures correlations are properly tracked.

Equations

• LeanCert.Engine.Affine.AffineVector = List LeanCert.Engine.Affine.AffineForm

def LeanCert.Engine.Affine.AffineVector.ofIntervals (Is : List Core.IntervalRat) : AffineVector

Create an affine vector from intervals, assigning each a unique noise symbol.

If intervals = [I₀, I₁, I₂], creates:

• x₀ = mid(I₀) + rad(I₀)·ε₀
• x₁ = mid(I₁) + rad(I₁)·ε₁
• x₂ = mid(I₂) + rad(I₂)·ε₂

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineVector.toIntervals (v : AffineVector) : List Core.IntervalRat

Convert back to interval bounds

Equations

• v.toIntervals = List.map LeanCert.Engine.Affine.AffineForm.toInterval v

Linear Operations

def LeanCert.Engine.Affine.AffineVector.add (v w : AffineVector) : AffineVector

Element-wise addition

Equations

• v.add w = List.zipWith LeanCert.Engine.Affine.AffineForm.add v w

def LeanCert.Engine.Affine.AffineVector.sub (v w : AffineVector) : AffineVector

Element-wise subtraction

Equations

• v.sub w = List.zipWith LeanCert.Engine.Affine.AffineForm.sub v w

def LeanCert.Engine.Affine.AffineVector.neg (v : AffineVector) : AffineVector

Element-wise negation

Equations

• v.neg = List.map LeanCert.Engine.Affine.AffineForm.neg v

def LeanCert.Engine.Affine.AffineVector.scale (q : ℚ) (v : AffineVector) : AffineVector

Scalar multiplication

Equations

• LeanCert.Engine.Affine.AffineVector.scale q v = List.map (LeanCert.Engine.Affine.AffineForm.scale q) v

Aggregation Operations

def LeanCert.Engine.Affine.AffineVector.sum (v : AffineVector) : AffineForm

Sum of all elements (preserves correlations!)

Equations

• v.sum = List.foldl LeanCert.Engine.Affine.AffineForm.add LeanCert.Engine.Affine.AffineForm.zero v

def LeanCert.Engine.Affine.AffineVector.mean (v : AffineVector) : AffineForm

Mean of all elements

Equations

• v.mean = if List.isEmpty v = true then LeanCert.Engine.Affine.AffineForm.zero else LeanCert.Engine.Affine.AffineForm.scale (1 / ↑(List.length v)) v.sum

def LeanCert.Engine.Affine.AffineVector.dot (v w : AffineVector) : AffineForm

Dot product of two vectors

Equations

• v.dot w = LeanCert.Engine.Affine.AffineVector.sum (List.zipWith LeanCert.Engine.Affine.AffineForm.mul v w)

LayerNorm Components

def LeanCert.Engine.Affine.AffineVector.centered (v : AffineVector) : AffineVector

Compute (x - μ) for each element, where μ = mean(x).

This is where Affine Arithmetic shines: the subtraction properly cancels the correlated parts, giving tight bounds.

Equations

• v.centered = List.map (fun (xi : LeanCert.Engine.Affine.AffineForm) => xi.sub v.mean) v

def LeanCert.Engine.Affine.AffineVector.variance (v : AffineVector) : AffineForm

Compute variance: mean((x - μ)²)

Equations

• v.variance = LeanCert.Engine.Affine.AffineVector.mean (List.map LeanCert.Engine.Affine.AffineForm.sq v.centered)

def LeanCert.Engine.Affine.AffineVector.layerNorm (v : AffineVector) (gamma beta : List ℚ) (eps : ℚ) : AffineVector

Layer Normalization: (x - μ) / √(σ² + ε) * γ + β

Parameters:

• v: input vector (affine)
• gamma: scale parameters
• beta: shift parameters
• eps: numerical stability constant

Equations

• One or more equations did not get rendered due to their size.

Softmax Components

def LeanCert.Engine.Affine.AffineVector.shiftedExp (v : AffineVector) : AffineVector

Compute exp(x_i - max(x)) for numerical stability

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineVector.softmax (v : AffineVector) : AffineVector

Softmax using algebraic cancellation.

softmax(x)_i = exp(x_i) / Σ exp(x_j) = 1 / Σ exp(x_j - x_i)

By computing differences first, we track correlations better.

Equations

• One or more equations did not get rendered due to their size.

Attention Components

def LeanCert.Engine.Affine.AffineVector.attentionWeights (q : AffineVector) (K : List AffineVector) (inv_sqrt_dk : ℚ) : AffineVector

Scaled dot-product attention scores for a single query.

Computes softmax(q · K^T / √d_k) where K is a list of key vectors.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineVector.applyAttention (weights : AffineVector) (V : List AffineVector) : AffineVector

Apply attention weights to values

Equations

• One or more equations did not get rendered due to their size.

GELU

def LeanCert.Engine.Affine.AffineVector.gelu (v : AffineVector) : AffineVector

GELU activation: x · Φ(x) ≈ 0.5 · x · (1 + tanh(√(2/π) · (x + 0.044715 · x³)))

Using affine arithmetic preserves correlations in x · tanh(f(x)).

Equations

• One or more equations did not get rendered due to their size.

Soundness

def LeanCert.Engine.Affine.AffineVector.mem (v_real : List ℝ) (v : AffineVector) (eps : AffineForm.NoiseAssignment) : Prop

Membership for affine vectors

Equations

• LeanCert.Engine.Affine.AffineVector.mem v_real v eps = (v_real.length = List.length v ∧ ∀ (i : ℕ) (hi_v : i < List.length v) (hi_r : i < v_real.length), v[i].mem_affine eps v_real[i])

theorem LeanCert.Engine.Affine.AffineVector.mem_sum {v_real : List ℝ} {v : AffineVector} {eps : AffineForm.NoiseAssignment} (_hvalid : AffineForm.validNoise eps) (hmem : mem v_real v eps) : v.sum.mem_affine eps v_real.sum

Sum is sound

theorem LeanCert.Engine.Affine.AffineVector.mem_mean {v_real : List ℝ} {v : AffineVector} {eps : AffineForm.NoiseAssignment} (hvalid : AffineForm.validNoise eps) (hmem : mem v_real v eps) (hne : ¬List.isEmpty v = true) : v.mean.mem_affine eps (v_real.sum / ↑v_real.length)

Mean is sound

theorem LeanCert.Engine.Affine.AffineVector.mem_centered {v_real : List ℝ} {v : AffineVector} {eps : AffineForm.NoiseAssignment} (hvalid : AffineForm.validNoise eps) (hmem : mem v_real v eps) : have μ := v_real.sum / ↑v_real.length; have centered_real := List.map (fun (x : ℝ) => x - μ) v_real; mem centered_real v.centered eps

Centered is sound: x - mean(x)

theorem LeanCert.Engine.Affine.AffineVector.mem_variance {v_real : List ℝ} {v : AffineVector} {eps : AffineForm.NoiseAssignment} (hvalid : AffineForm.validNoise eps) (hmem : mem v_real v eps) (hne : ¬List.isEmpty v = true) : have μ := v_real.sum / ↑v_real.length; have var_real := (List.map (fun (x : ℝ) => (x - μ) * (x - μ)) v_real).sum / ↑v_real.length; v.variance.mem_affine eps var_real

Variance is sound

theorem LeanCert.Engine.Affine.AffineVector.mem_layerNorm {v_real : List ℝ} {v : AffineVector} {eps : AffineForm.NoiseAssignment} (gamma beta : List ℚ) (epsilon : ℚ) (heps_pos : 0 < epsilon) (hvalid : AffineForm.validNoise eps) (hmem : mem v_real v eps) (hne : ¬List.isEmpty v = true) (hlen_eps : List.length eps = (v.variance.add (AffineForm.const epsilon)).coeffs.length) (hlen_sqrt : List.length eps = (v.variance.add (AffineForm.const epsilon)).sqrt.coeffs.length) (hsqrt_pos : 0 < (v.variance.add (AffineForm.const epsilon)).sqrt.toInterval.lo) : have μ := v_real.sum / ↑v_real.length; have variance_real := (List.map (fun (x : ℝ) => (x - μ) * (x - μ)) v_real).sum / ↑v_real.length; have std_real := √(variance_real + ↑epsilon); have inv_std_real := 1 / std_real; have output_real := List.zipWith3 (fun (xi : ℝ) (g b : ℚ) => (xi - μ) * inv_std_real * ↑g + ↑b) v_real gamma beta; mem output_real (v.layerNorm gamma beta epsilon) eps

LayerNorm is sound for the complete operation.

Note: This theorem requires additional hypotheses that would typically be verified at the call site:

• The variance + epsilon must be positive (guaranteed by epsilon > 0)
• Length constraints for gamma and beta
• The affine form for var + eps must have positive lower bound for inv

The proof composition uses:

1. mem_centered for centering
2. mem_variance for variance
3. mem_add for adding epsilon
4. mem_sqrt for standard deviation
5. mem_inv for reciprocal
6. mem_layerNorm_elem for each output element