Quantized Neural Network Layers

This module implements two critical optimizations for neural network verification:

Optimization 1: Split-Sign Matrix Decomposition

Instead of computing interval arithmetic with min/max at every weight:

[a, b] × [x, y] = [min(ax, ay, bx, by), max(...)]

We precompute W = W⁺ - W⁻ where:

• W⁺ᵢⱼ = max(0, Wᵢⱼ)
• W⁻ᵢⱼ = max(0, -Wᵢⱼ)

Then for x ∈ [l, u]:

• y_lo = W⁺ · l - W⁻ · u
• y_hi = W⁺ · u - W⁻ · l

This reduces interval matrix multiplication to 4 standard matrix-vector products with no branching in the inner loop.

Optimization 2: Common Exponent Integer Arithmetic

Instead of Dyadic arithmetic (mantissa × 2^exp) per operation, we:

1. Align all values to a common exponent
2. Perform pure integer (GMP) arithmetic
3. Reconstruct Dyadic results at the end

This eliminates per-operation exponent handling.

Main Definitions

• SplitWeights - Pre-decomposed W⁺, W⁻ matrices
• QuantizedLayer - Layer with aligned integer representation
• forwardQuantized - Optimized forward pass

Helper Lemmas for Fold Induction

Pure Integer Matrix-Vector Operations

@[inline]

def LeanCert.ML.Optimized.dotProductInt (a b : Array ℤ) : ℤ

Integer dot product of two arrays

Equations

• LeanCert.ML.Optimized.dotProductInt a b = Array.foldl (fun (acc : ℤ) (i : ℕ) => acc + a[i]! * b[i]!) 0 (Array.range (min a.size b.size))

theorem LeanCert.ML.Optimized.dotProductInt_mono_nonneg (w lo hi : Array ℤ) (h_w_nonneg : ∀ i < min w.size lo.size, i < min w.size hi.size → 0 ≤ w[i]!) (h_lo_le_hi : ∀ i < min w.size lo.size, i < min w.size hi.size → lo[i]! ≤ hi[i]!) (h_size_eq : min w.size lo.size = min w.size hi.size) : dotProductInt w lo ≤ dotProductInt w hi

Monotonicity of integer dot product: if w[i] ≥ 0 for all i, and lo[i] ≤ hi[i], then w·lo ≤ w·hi.

@[inline]

def LeanCert.ML.Optimized.matVecMulInt (M : Array (Array ℤ)) (v : Array ℤ) : Array ℤ

Integer matrix-vector multiplication

Equations

• LeanCert.ML.Optimized.matVecMulInt M v = Array.map (fun (x : Array ℤ) => LeanCert.ML.Optimized.dotProductInt x v) M

@[inline]

def LeanCert.ML.Optimized.addIntArrays (a b : Array ℤ) : Array ℤ

Integer array addition

Equations

• LeanCert.ML.Optimized.addIntArrays a b = Array.zipWith (fun (x1 x2 : ℤ) => x1 + x2) a b

@[inline]

def LeanCert.ML.Optimized.subIntArrays (a b : Array ℤ) : Array ℤ

Integer array subtraction

Equations

• LeanCert.ML.Optimized.subIntArrays a b = Array.zipWith (fun (x1 x2 : ℤ) => x1 - x2) a b

@[inline]

def LeanCert.ML.Optimized.reluInt (a : Array ℤ) : Array ℤ

Integer max(0, x) applied element-wise

Equations

• LeanCert.ML.Optimized.reluInt a = Array.map (max 0) a

Helper lemmas for getElem! indexing

theorem LeanCert.ML.Optimized.reluInt_getElem (a : Array ℤ) (i : ℕ) (hi : i < a.size) : (reluInt a)[i] = max 0 a[i]

reluInt indexing when i is in bounds

theorem LeanCert.ML.Optimized.reluInt_getElem! (a : Array ℤ) (i : ℕ) (hi : i < a.size) : (reluInt a)[i]! = max 0 a[i]!

reluInt indexing for panicking access

theorem LeanCert.ML.Optimized.addIntArrays_getElem! (a b : Array ℤ) (i : ℕ) (ha : i < a.size) (hb : i < b.size) : (addIntArrays a b)[i]! = a[i]! + b[i]!

addIntArrays indexing when i is in bounds for both

theorem LeanCert.ML.Optimized.subIntArrays_getElem! (a b : Array ℤ) (i : ℕ) (ha : i < a.size) (hb : i < b.size) : (subIntArrays a b)[i]! = a[i]! - b[i]!

subIntArrays indexing when i is in bounds for both

theorem LeanCert.ML.Optimized.matVecMulInt_getElem! (M : Array (Array ℤ)) (v : Array ℤ) (i : ℕ) (hi : i < M.size) : (matVecMulInt M v)[i]! = dotProductInt M[i]! v

matVecMulInt indexing when i is in bounds

Split-Sign Weight Decomposition

structure LeanCert.ML.Optimized.SplitWeights (outDim inDim : ℕ) : Type

Pre-decomposed weight matrices for branch-free interval multiplication. Stores W⁺ = max(0, W) and W⁻ = max(0, -W) separately as integer arrays.

• pos : Array (Array ℤ)

  Positive part as integers: W⁺ᵢⱼ × 2^(-exp)

• neg : Array (Array ℤ)

  Negative part as integers: W⁻ᵢⱼ × 2^(-exp)

• exp : ℤ

  Common exponent

• pos_rows : self.pos.size = outDim

  Size invariants

• neg_rows : self.neg.size = outDim

def LeanCert.ML.Optimized.instReprSplitWeights.repr {outDim✝ inDim✝ : ℕ} : SplitWeights outDim✝ inDim✝ → ℕ → Std.Format

Equations

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

instance LeanCert.ML.Optimized.instReprSplitWeights {outDim✝ inDim✝ : ℕ} : Repr (SplitWeights outDim✝ inDim✝)

Equations

• LeanCert.ML.Optimized.instReprSplitWeights = { reprPrec := LeanCert.ML.Optimized.instReprSplitWeights.repr }

Quantized Layer

structure LeanCert.ML.Optimized.QuantizedLayer : Type

A layer with all weights aligned to a common exponent for pure integer arithmetic.

This is the key optimization: instead of Dyadic operations (which involve per-operation exponent handling), we shift everything to a common exponent and do pure BigInt arithmetic.

• commonExp : ℤ

  Common exponent for the entire layer

• weightsPos : Array (Array ℤ)

  W⁺ scaled to integers

• weightsNeg : Array (Array ℤ)

  W⁻ scaled to integers

• bias : Array ℤ

  Bias scaled to integers

• outDim : ℕ

  Output dimension

• inDim : ℕ

  Input dimension

instance LeanCert.ML.Optimized.instReprQuantizedLayer : Repr QuantizedLayer

Equations

• LeanCert.ML.Optimized.instReprQuantizedLayer = { reprPrec := LeanCert.ML.Optimized.instReprQuantizedLayer.repr }

def LeanCert.ML.Optimized.instReprQuantizedLayer.repr : QuantizedLayer → ℕ → Std.Format

Equations

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

def LeanCert.ML.Optimized.QuantizedLayer.scaleToInt (x : ℚ) (exp : ℤ) : ℤ

Scale a rational to an integer given a common exponent. Returns floor(x × 2^(-exp)).

Equations

• LeanCert.ML.Optimized.QuantizedLayer.scaleToInt x exp = (x * if exp ≥ 0 then 1 / 2 ^ exp.toNat else 2 ^ (-exp).toNat).floor

def LeanCert.ML.Optimized.QuantizedLayer.ofLayer (l : Layer) (prec : ℤ := -53) : QuantizedLayer

Create a quantized layer from a rational Layer

Equations

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

Aligned Input Representation

structure LeanCert.ML.Optimized.QuantizedLayer.AlignedInput : Type

Input representation aligned to a common exponent

• lo : Array ℤ

  Lower bounds as integers

• hi : Array ℤ

  Upper bounds as integers

• exp : ℤ

  The exponent these are aligned to

def LeanCert.ML.Optimized.QuantizedLayer.instReprAlignedInput.repr : AlignedInput → ℕ → Std.Format

Equations

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

instance LeanCert.ML.Optimized.QuantizedLayer.instReprAlignedInput : Repr AlignedInput

Equations

• LeanCert.ML.Optimized.QuantizedLayer.instReprAlignedInput = { reprPrec := LeanCert.ML.Optimized.QuantizedLayer.instReprAlignedInput.repr }

def LeanCert.ML.Optimized.QuantizedLayer.alignInput {n : ℕ} (v : IntervalArray n) (targetExp : ℤ) : AlignedInput

Align an IntervalArray to a given exponent for integer arithmetic

Equations

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

@[inline]

def LeanCert.ML.Optimized.QuantizedLayer.shiftInt (x shift : ℤ) : ℤ

Shift an integer by a given amount (left if positive, right if negative)

Equations

• LeanCert.ML.Optimized.QuantizedLayer.shiftInt x shift = if shift ≥ 0 then x * 2 ^ shift.toNat else x / 2 ^ (-shift).toNat

def LeanCert.ML.Optimized.QuantizedLayer.forwardQuantized (l : QuantizedLayer) (input : AlignedInput) : AlignedInput

The Optimized Forward Pass

This is the main verification kernel. It performs:

1. Input alignment to layer's common exponent
2. Split-sign matrix multiplication (no branching!)
3. Integer addition for bias
4. Integer max for ReLU
5. Result in aligned integer format

All operations are pure integer (GMP) arithmetic.

Equations

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

def LeanCert.ML.Optimized.QuantizedLayer.toIntervalArray (a : AlignedInput) (n : ℕ) (hn : a.lo.size = n ∧ a.hi.size = n) : IntervalArray n

Convert AlignedInput back to an IntervalArray

Equations

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

Semantics of Quantized Types

noncomputable def LeanCert.ML.Optimized.QuantizedLayer.intVal (n e : ℤ) : ℝ

The real value represented by a quantized integer: n × 2^e

Equations

• LeanCert.ML.Optimized.QuantizedLayer.intVal n e = ↑n * 2 ^ e

theorem LeanCert.ML.Optimized.QuantizedLayer.intVal_add (a b e : ℤ) : intVal (a + b) e = intVal a e + intVal b e

Basic property: intVal respects addition

theorem LeanCert.ML.Optimized.QuantizedLayer.intVal_sub (a b e : ℤ) : intVal (a - b) e = intVal a e - intVal b e

Basic property: intVal respects subtraction

theorem LeanCert.ML.Optimized.QuantizedLayer.intVal_mul (a b ea eb : ℤ) : intVal a ea * intVal b eb = intVal (a * b) (ea + eb)

Basic property: intVal respects multiplication with exponent addition

theorem LeanCert.ML.Optimized.QuantizedLayer.intVal_zero (e : ℤ) : intVal 0 e = 0

intVal 0 is 0

theorem LeanCert.ML.Optimized.QuantizedLayer.intVal_nonneg {n : ℤ} (hn : 0 ≤ n) (e : ℤ) : 0 ≤ intVal n e

intVal of nonnegative integer is nonnegative

def LeanCert.ML.Optimized.QuantizedLayer.AlignedInput.mem (a : AlignedInput) (x : List ℝ) : Prop

Membership in AlignedInput: a real vector x is contained if each component satisfies lo[i] × 2^exp ≤ x[i] ≤ hi[i] × 2^exp

Equations

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

Split-Sign Arithmetic Lemmas

theorem LeanCert.ML.Optimized.QuantizedLayer.nonneg_mul_bounds {p l u x : ℝ} (hp : 0 ≤ p) (hl : l ≤ x) (hu : x ≤ u) : p * l ≤ p * x ∧ p * x ≤ p * u

Key lemma: For p ≥ 0, if l ≤ x ≤ u then pl ≤ px ≤ p*u

theorem LeanCert.ML.Optimized.QuantizedLayer.dotProduct_bounds_nonneg {n : ℕ} (p l u x : Fin n → ℝ) (hp : ∀ (i : Fin n), 0 ≤ p i) (hl : ∀ (i : Fin n), l i ≤ x i) (hu : ∀ (i : Fin n), x i ≤ u i) : ∑ i : Fin n, p i * l i ≤ ∑ i : Fin n, p i * x i ∧ ∑ i : Fin n, p i * x i ≤ ∑ i : Fin n, p i * u i

Dot product bounds for nonnegative weights. If p[i] ≥ 0 for all i, and l[i] ≤ x[i] ≤ u[i], then Σ p[i]*l[i] ≤ Σ p[i]*x[i] ≤ Σ p[i]*u[i]

theorem LeanCert.ML.Optimized.QuantizedLayer.split_sign_bounds {n : ℕ} (pos neg l u x : Fin n → ℝ) (hpos : ∀ (i : Fin n), 0 ≤ pos i) (hneg : ∀ (i : Fin n), 0 ≤ neg i) (hl : ∀ (i : Fin n), l i ≤ x i) (hu : ∀ (i : Fin n), x i ≤ u i) : have w := fun (i : Fin n) => pos i - neg i; have y := ∑ i : Fin n, w i * x i; ∑ i : Fin n, pos i * l i - ∑ i : Fin n, neg i * u i ≤ y ∧ y ≤ ∑ i : Fin n, pos i * u i - ∑ i : Fin n, neg i * l i

Main split-sign lemma: If W = P - N with P,N ≥ 0, and l ≤ x ≤ u, then P·l - N·u ≤ W·x ≤ P·u - N·l

theorem LeanCert.ML.Optimized.QuantizedLayer.relu_preserves_bounds {lo x hi : ℝ} (hlo : lo ≤ x) (hhi : x ≤ hi) : max 0 lo ≤ max 0 x ∧ max 0 x ≤ max 0 hi

ReLU preserves bounds: if lo ≤ x ≤ hi then max(0,lo) ≤ max(0,x) ≤ max(0,hi)

Soundness Theorem

theorem LeanCert.ML.Optimized.QuantizedLayer.intVal_max_le {a b : ℤ} (h : a ≤ b) (e : ℤ) : intVal (max 0 a) e ≤ intVal (max 0 b) e

Integer max(0, ·) implies intVal ordering

theorem LeanCert.ML.Optimized.QuantizedLayer.intVal_mono {a b : ℤ} (h : a ≤ b) (e : ℤ) : intVal a e ≤ intVal b e

intVal is monotone in the integer argument

theorem LeanCert.ML.Optimized.QuantizedLayer.intVal_strictMono {a b : ℤ} (h : a < b) (e : ℤ) : intVal a e < intVal b e

intVal is strictly monotone

theorem LeanCert.ML.Optimized.QuantizedLayer.forwardQuantized_sound (l_quant : QuantizedLayer) (input : AlignedInput) (h_lo_dim : input.lo.size = l_quant.inDim) (h_hi_dim : input.hi.size = l_quant.inDim) (h_wpos_dim : l_quant.weightsPos.size = l_quant.outDim) (h_wneg_dim : l_quant.weightsNeg.size = l_quant.outDim) (h_bias_dim : l_quant.bias.size = l_quant.outDim) (h_wpos_cols : ∀ (r : ℕ) (hr : r < l_quant.outDim), l_quant.weightsPos[r].size = l_quant.inDim) (h_wneg_cols : ∀ (r : ℕ) (hr : r < l_quant.outDim), l_quant.weightsNeg[r].size = l_quant.inDim) (h_pos_nonneg : ∀ (r c : ℕ), r < l_quant.outDim → c < l_quant.inDim → 0 ≤ l_quant.weightsPos[r]![c]!) (h_neg_nonneg : ∀ (r c : ℕ), r < l_quant.outDim → c < l_quant.inDim → 0 ≤ l_quant.weightsNeg[r]![c]!) (h_bounds_valid : ∀ k < l_quant.inDim, input.lo[k]! ≤ input.hi[k]!) (h_aligned : input.exp = l_quant.commonExp) (idx : ℕ) (_hidx : idx < l_quant.outDim) : (l_quant.forwardQuantized input).lo[idx]! ≤ (l_quant.forwardQuantized input).hi[idx]!

Soundness of the Optimized Forward Pass.

This theorem establishes that the interval bounds computed by forwardQuantized are mathematically valid: the output lower bound is ≤ output upper bound.

The proof uses the split-sign decomposition property:

• If W = W⁺ - W⁻ where W⁺, W⁻ ≥ 0
• And l ≤ x ≤ u
• Then W⁺·l - W⁻·u ≤ W·x ≤ W⁺·u - W⁻·l

Combined with ReLU monotonicity, this gives the soundness of the entire forward pass.

theorem LeanCert.ML.Optimized.QuantizedLayer.forwardQuantized_nonempty (l_quant : QuantizedLayer) (input : AlignedInput) (x : List ℝ) (_h_input_dim : x.length = l_quant.inDim) (h_lo_dim : input.lo.size = l_quant.inDim) (h_hi_dim : input.hi.size = l_quant.inDim) (h_wpos_dim : l_quant.weightsPos.size = l_quant.outDim) (h_wneg_dim : l_quant.weightsNeg.size = l_quant.outDim) (h_bias_dim : l_quant.bias.size = l_quant.outDim) (h_wpos_cols : ∀ (r : ℕ) (hr : r < l_quant.outDim), l_quant.weightsPos[r].size = l_quant.inDim) (h_wneg_cols : ∀ (r : ℕ) (hr : r < l_quant.outDim), l_quant.weightsNeg[r].size = l_quant.inDim) (h_pos_nonneg : ∀ (r c : ℕ), r < l_quant.outDim → c < l_quant.inDim → 0 ≤ l_quant.weightsPos[r]![c]!) (h_neg_nonneg : ∀ (r c : ℕ), r < l_quant.outDim → c < l_quant.inDim → 0 ≤ l_quant.weightsNeg[r]![c]!) (h_aligned : input.exp = l_quant.commonExp) (hx_lo : ∀ k < l_quant.inDim, intVal input.lo[k]! input.exp ≤ x[k]!) (hx_hi : ∀ k < l_quant.inDim, x[k]! ≤ intVal input.hi[k]! input.exp) (i : ℕ) (_hi : i < l_quant.outDim) : intVal (l_quant.forwardQuantized input).lo[i]! (l_quant.forwardQuantized input).exp ≤ intVal (l_quant.forwardQuantized input).hi[i]! (l_quant.forwardQuantized input).exp

Main soundness theorem: The output interval bounds satisfy lo ≤ hi when there exists a real input x in the input interval.

This version shows that the output interval is non-empty.

Full Network with Quantized Layers

structure LeanCert.ML.Optimized.QuantizedNet : Type

A neural network with all layers quantized for fast verification

• layers : Array QuantizedLayer

instance LeanCert.ML.Optimized.instReprQuantizedNet : Repr QuantizedNet

Equations

• LeanCert.ML.Optimized.instReprQuantizedNet = { reprPrec := LeanCert.ML.Optimized.instReprQuantizedNet.repr }

def LeanCert.ML.Optimized.instReprQuantizedNet.repr : QuantizedNet → ℕ → Std.Format

Equations

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

def LeanCert.ML.Optimized.QuantizedNet.ofLayers (ls : List Layer) (prec : ℤ := -53) : QuantizedNet

Create a quantized network from a list of layers

Equations

• LeanCert.ML.Optimized.QuantizedNet.ofLayers ls prec = { layers := (List.map (fun (x : LeanCert.ML.Layer) => LeanCert.ML.Optimized.QuantizedLayer.ofLayer x prec) ls).toArray }

def LeanCert.ML.Optimized.QuantizedNet.forward (net : QuantizedNet) (input : QuantizedLayer.AlignedInput) : QuantizedLayer.AlignedInput

Forward pass through the entire quantized network

Equations

• net.forward input = Array.foldl (fun (acc : LeanCert.ML.Optimized.QuantizedLayer.AlignedInput) (l : LeanCert.ML.Optimized.QuantizedLayer) => l.forwardQuantized acc) input net.layers