Documentation

LeanMlir.Proofs.Certificates.IntervalBound

Interval bound propagation (IBP), sound and kernel-checkable #

The L∞ counterpart of the Lipschitz scorecard: push an axis-aligned box through the network (sign-split interval arithmetic for the bias-free dense layers, endpoint max for ReLU) and certify the prediction whenever the output boxes separate — denseHi … j < denseLo … y for every j ≠ y gives ∀ δ, (∀ i, |δ i| ≤ ε) → argmax fixed (ibp2_certified_at_eps).

Why this matters here: IBP is LINEAR in width (two interval dots per neuron), where the Gram/Schatten and LipSDP certificates are quadratic-to-cubic — this is the certificate that scales past the h=16 wall to canonical widths. And the perturbation model is the literature-standard pixel L∞ ball, stated coordinatewise (∀ i, |δ i| ≤ ε) with no norm-instance games.

The first layer sees a UNIFORM box x ∓ ε, where the interval image collapses to ⟨w, x⟩ ∓ ε·‖w‖₁ (denseLo_uniform/denseHi_uniform) — so the generated files reuse the scorecard's kernel dotZ facts for ⟨w, x⟩ and one absSumZ kernel fact per row for ‖w‖₁ (ListDot.lean).

The certificate itself is stated on a bracket, not on interval arithmetic: certified_of_boxSound takes any BoxSoundE f Flo Fhi — "Flo/Fhi trap f on the box" — and ibp2_certified_at_eps is its corollary at the interval bracket mlp2_boxSound. A tighter bracket (CROWN, planning/archive/crown_ibp.md) therefore plugs into this tier rather than forking it.

Everything is elementary and 3-axiom clean; instance files: LipschitzCertScorecardIBP*.lean (generated by scripts/lipschitz_cert_scorecard_ibp.py).

noncomputable def Proofs.LipschitzCertDemo.denseLo {m n : ℕ} (W : Fin m → Fin n → ℝ) (lo hi : Fin n → ℝ) :

Fin m → ℝ

Sign-split LOWER image of a bias-free dense layer on the box [lo, hi]: positive weights pull from lo, negative from hi.

Equations

Proofs.LipschitzCertDemo.denseLo W lo hi k = ∑ j : Fin n, if 0 ≤ W k j then W k j * lo j else W k j * hi j

Instances For

noncomputable def Proofs.LipschitzCertDemo.denseHi {m n : ℕ} (W : Fin m → Fin n → ℝ) (lo hi : Fin n → ℝ) :

Fin m → ℝ

Sign-split UPPER image.

Equations

Proofs.LipschitzCertDemo.denseHi W lo hi k = ∑ j : Fin n, if 0 ≤ W k j then W k j * hi j else W k j * lo j

Instances For

noncomputable def Proofs.LipschitzCertDemo.reluLo {n : ℕ} (lo : Fin n → ℝ) :

Fin n → ℝ

ReLU box endpoints.

Equations

Proofs.LipschitzCertDemo.reluLo lo j = max (lo j) 0

Instances For

noncomputable def Proofs.LipschitzCertDemo.reluHi {n : ℕ} (hi : Fin n → ℝ) :

Fin n → ℝ

Equations

Proofs.LipschitzCertDemo.reluHi hi j = max (hi j) 0

Instances For

def Proofs.LipschitzCertDemo.CertifiedAtLinf {n k : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)) (ε : ℝ) (x : EuclideanSpace ℝ (Fin n)) (y : Fin k) :

f is certified at L∞ radius ε on input x with class y: every coordinatewise-bounded perturbation keeps y the strict argmax. The L∞ peer of CertifiedAt (LipschitzCertScorecard.lean).

Equations

Proofs.LipschitzCertDemo.CertifiedAtLinf f ε x y = ∀ (δ : EuclideanSpace ℝ (Fin n)), (∀ (i : Fin n), |δ.ofLp i| ≤ ε) → ∀ (j : Fin k), j ≠ y → (f (x + δ)).ofLp j < (f (x + δ)).ofLp y

Instances For

theorem Proofs.LipschitzCertDemo.CertifiedAtLinf.mono {n k : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} {ε ε' : ℝ} {x : EuclideanSpace ℝ (Fin n)} {y : Fin k} (hc : CertifiedAtLinf f ε x y) (hle : ε' ≤ ε) :

CertifiedAtLinf f ε' x y

Certification is monotone in the radius, directly from the statement. An instance therefore only needs to carry the certificate data for the LARGEST radius at which an image certifies; every smaller radius on the ε-grid is a one-line corollary rather than another propagated box. The peer of IBP.CertifiedAtLinf3.mono.

theorem Proofs.LipschitzCertDemo.denseLo_le {m n : ℕ} (W : Fin m → Fin n → ℝ) {lo hi : Fin n → ℝ} {x : EuclideanSpace ℝ (Fin n)} (hbox : ∀ (j : Fin n), lo j ≤ x.ofLp j ∧ x.ofLp j ≤ hi j) (k : Fin m) :

denseLo W lo hi k ≤ (denseE W x).ofLp k

theorem Proofs.LipschitzCertDemo.le_denseHi {m n : ℕ} (W : Fin m → Fin n → ℝ) {lo hi : Fin n → ℝ} {x : EuclideanSpace ℝ (Fin n)} (hbox : ∀ (j : Fin n), lo j ≤ x.ofLp j ∧ x.ofLp j ≤ hi j) (k : Fin m) :

(denseE W x).ofLp k ≤ denseHi W lo hi k

theorem Proofs.LipschitzCertDemo.relu_box {n : ℕ} {lo hi : Fin n → ℝ} {u : EuclideanSpace ℝ (Fin n)} (hbox : ∀ (j : Fin n), lo j ≤ u.ofLp j ∧ u.ofLp j ≤ hi j) (j : Fin n) :

reluLo lo j ≤ (reluE u).ofLp j ∧ (reluE u).ofLp j ≤ reluHi hi j

ReLU maps the box [lo, hi] into [reluLo lo, reluHi hi].

theorem Proofs.LipschitzCertDemo.denseLo_uniform {m n : ℕ} (W : Fin m → Fin n → ℝ) (x : EuclideanSpace ℝ (Fin n)) (ε : ℝ) (k : Fin m) :

denseLo W (fun (j : Fin n) => x.ofLp j - ε) (fun (j : Fin n) => x.ofLp j + ε) k = ∑ j : Fin n, W k j * x.ofLp j - ε * ∑ j : Fin n, |W k j|

theorem Proofs.LipschitzCertDemo.denseHi_uniform {m n : ℕ} (W : Fin m → Fin n → ℝ) (x : EuclideanSpace ℝ (Fin n)) (ε : ℝ) (k : Fin m) :

denseHi W (fun (j : Fin n) => x.ofLp j - ε) (fun (j : Fin n) => x.ofLp j + ε) k = ∑ j : Fin n, W k j * x.ofLp j + ε * ∑ j : Fin n, |W k j|

theorem Proofs.LipschitzCertDemo.denseLo2_eval {n h k : ℕ} (W1 : Fin h → Fin n → ℝ) (W2 : Fin k → Fin h → ℝ) (x : EuclideanSpace ℝ (Fin n)) (ε : ℝ) (c : Fin k) :

denseLo W2 (reluLo (denseLo W1 (fun (i : Fin n) => x.ofLp i - ε) fun (i : Fin n) => x.ofLp i + ε)) (reluHi (denseHi W1 (fun (i : Fin n) => x.ofLp i - ε) fun (i : Fin n) => x.ofLp i + ε)) c = ∑ t : Fin h, if 0 ≤ W2 c t then W2 c t * max (∑ j : Fin n, W1 t j * x.ofLp j - ε * ∑ j : Fin n, |W1 t j|) 0 else W2 c t * max (∑ j : Fin n, W1 t j * x.ofLp j + ε * ∑ j : Fin n, |W1 t j|) 0

The 2-layer LOWER box endpoint, evaluated: outer sign-split over the ReLU'd first-layer uniform box, with the inner sums left as ⟨w,x⟩ and Σ|w| (which instance files rewrite via their hpre/absSumZ data — the 784-sums must be REWRITTEN, never unfolded).

theorem Proofs.LipschitzCertDemo.denseHi2_eval {n h k : ℕ} (W1 : Fin h → Fin n → ℝ) (W2 : Fin k → Fin h → ℝ) (x : EuclideanSpace ℝ (Fin n)) (ε : ℝ) (c : Fin k) :

denseHi W2 (reluLo (denseLo W1 (fun (i : Fin n) => x.ofLp i - ε) fun (i : Fin n) => x.ofLp i + ε)) (reluHi (denseHi W1 (fun (i : Fin n) => x.ofLp i - ε) fun (i : Fin n) => x.ofLp i + ε)) c = ∑ t : Fin h, if 0 ≤ W2 c t then W2 c t * max (∑ j : Fin n, W1 t j * x.ofLp j + ε * ∑ j : Fin n, |W1 t j|) 0 else W2 c t * max (∑ j : Fin n, W1 t j * x.ofLp j - ε * ∑ j : Fin n, |W1 t j|) 0

The 2-layer UPPER box endpoint, evaluated (sibling of denseLo2_eval).

The certificate below never inspects how the output box was computed — only that it brackets the net on x ∓ ε. Factoring that out as a hypothesis (the IntervalBoundConv.lean engine's own shape, BoxSound3 / ibp3_certified_of_boxSound) is what lets a second, tighter bracket — a CROWN backward pass, say — reuse this tier instead of forking a parallel stack: anything that discharges BoxSoundE certifies. ibp2_certified_at_eps is then the interval bracket's corollary, not the entry point.

def Proofs.LipschitzCertDemo.InBoxE {n : ℕ} (lo hi : Fin n → ℝ) (u : EuclideanSpace ℝ (Fin n)) :

u lies in the axis-aligned box [lo, hi].

Equations

Proofs.LipschitzCertDemo.InBoxE lo hi u = ∀ (i : Fin n), lo i ≤ u.ofLp i ∧ u.ofLp i ≤ hi i

Instances For

def Proofs.LipschitzCertDemo.BoxSoundE {n m : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)) (Flo Fhi : (Fin n → ℝ) → (Fin n → ℝ) → Fin m → ℝ) :

A sound bracket for f. Flo lo hi / Fhi lo hi trap f on every point of the box [lo, hi]. This says nothing about interval arithmetic — it is the pure bracketing predicate the capstone consumes.

Equations

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

Instances For

theorem Proofs.LipschitzCertDemo.BoxSoundE.comp {n m p : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)} {g : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin p)} {Flo Fhi : (Fin n → ℝ) → (Fin n → ℝ) → Fin m → ℝ} {Glo Ghi : (Fin m → ℝ) → (Fin m → ℝ) → Fin p → ℝ} (hg : BoxSoundE g Glo Ghi) (hf : BoxSoundE f Flo Fhi) :

BoxSoundE (g ∘ f) (fun (lo hi : Fin n → ℝ) => Glo (Flo lo hi) (Fhi lo hi)) fun (lo hi : Fin n → ℝ) => Ghi (Flo lo hi) (Fhi lo hi)

Depth. Sound brackets compose exactly as their layers do — feed the first layer's output box into the second layer's bracket.

theorem Proofs.LipschitzCertDemo.denseE_boxSound {m n : ℕ} (W : Fin m → Fin n → ℝ) :

BoxSoundE (denseE W) (denseLo W) (denseHi W)

The interval bracket for a bias-free dense layer (denseLo_le + le_denseHi, packaged).

theorem Proofs.LipschitzCertDemo.reluE_boxSound {n : ℕ} :

BoxSoundE reluE (fun (lo x : Fin n → ℝ) => reluLo lo) fun (x hi : Fin n → ℝ) => reluHi hi

The interval bracket for ReLU (relu_box, packaged).

theorem Proofs.LipschitzCertDemo.certified_of_boxSound {n k : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} {Flo Fhi : (Fin n → ℝ) → (Fin n → ℝ) → Fin k → ℝ} (hs : BoxSoundE f Flo Fhi) {x : EuclideanSpace ℝ (Fin n)} {ε : ℝ} {y : Fin k} (hsep : ∀ (j : Fin k), j ≠ y → Fhi (fun (i : Fin n) => x.ofLp i - ε) (fun (i : Fin n) => x.ofLp i + ε) j < Flo (fun (i : Fin n) => x.ofLp i - ε) (fun (i : Fin n) => x.ofLp i + ε) y) :

CertifiedAtLinf f ε x y

Box separation ⇒ L∞ certificate, from ANY sound bracket. If the bracketing box's wrong-logit upper bounds all sit strictly below the true logit's lower bound on x ∓ ε, then every perturbation with |δ i| ≤ ε coordinatewise keeps class y the strict argmax. Boxes are data; separation is finitely many rational comparisons.

theorem Proofs.LipschitzCertDemo.mlp2_boxSound {n h k : ℕ} (W1 : Fin h → Fin n → ℝ) (W2 : Fin k → Fin h → ℝ) :

BoxSoundE (denseE W2 ∘ reluE ∘ denseE W1) (fun (lo hi : Fin n → ℝ) => denseLo W2 (reluLo (denseLo W1 lo hi)) (reluHi (denseHi W1 lo hi))) fun (lo hi : Fin n → ℝ) => denseHi W2 (reluLo (denseLo W1 lo hi)) (reluHi (denseHi W1 lo hi))

The interval bracket for dense ∘ relu ∘ dense — two .comps of the per-layer facts, no new argument.

theorem Proofs.LipschitzCertDemo.ibp2_certified_at_eps {n h k : ℕ} (W1 : Fin h → Fin n → ℝ) (W2 : Fin k → Fin h → ℝ) {x : EuclideanSpace ℝ (Fin n)} {ε : ℝ} {y : Fin k} (hcmp : ∀ (j : Fin k), j ≠ y → denseHi W2 (reluLo (denseLo W1 (fun (i : Fin n) => x.ofLp i - ε) fun (i : Fin n) => x.ofLp i + ε)) (reluHi (denseHi W1 (fun (i : Fin n) => x.ofLp i - ε) fun (i : Fin n) => x.ofLp i + ε)) j < denseLo W2 (reluLo (denseLo W1 (fun (i : Fin n) => x.ofLp i - ε) fun (i : Fin n) => x.ofLp i + ε)) (reluHi (denseHi W1 (fun (i : Fin n) => x.ofLp i - ε) fun (i : Fin n) => x.ofLp i + ε)) y) (δ : EuclideanSpace ℝ (Fin n)) (hδ : ∀ (i : Fin n), |δ.ofLp i| ≤ ε) (j : Fin k) :

j ≠ y → ((denseE W2 ∘ reluE ∘ denseE W1) (x + δ)).ofLp j < ((denseE W2 ∘ reluE ∘ denseE W1) (x + δ)).ofLp y

IBP L∞ certificate for dense ∘ relu ∘ dense. If the propagated output boxes separate — the upper bound of every wrong logit is strictly below the lower bound of the true one on the box x ∓ ε — then EVERY perturbation with |δ i| ≤ ε coordinatewise keeps class y the strict argmax. Boxes are data; separation is finitely many rational comparisons.

This is certified_of_boxSound at the interval bracket mlp2_boxSound; the generated instance files (LipschitzCertScorecardIBP*.lean) cite it in this shape, hypothesis-for-hypothesis.