Floating-Point Interval Semantics

Interval-domain semantics for IEEE32Exec neural networks.

This file formalizes the interval domain, concretization map, executable interval operators, and the exact-interval-image property used by the floating-point interval-approximation theorem of Hwang, Lee, Park, Park, and Saad, Floating-Point Neural Networks Are Provably Robust Universal Approximators (arXiv:2506.16065).

Basic aliases

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.F : Type

Shorthand for the executable binary32 float type used in this development.

IEEE32Exec is stored as a UInt32 bit-pattern, so the carrier is finite. We use this only to obtain Finset.univ for paper-style “finite hull” definitions; nothing is computed.

@[implicit_reducible]

instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.DecidableInstances.instDecidableRelFLe : DecidableRel fun (x y : F) => x ≤ y

instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.FintypeInstances.instFiniteUInt32_nN : Finite UInt32

@[implicit_reducible]

noncomputable instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.FintypeInstances.instFintypeUInt32_nN : Fintype UInt32

instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.FintypeInstances.instFiniteIEEE32Exec : Finite TorchLean.Floats.IEEE754.IEEE32Exec

@[implicit_reducible]

noncomputable instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.FintypeInstances.instFintypeIEEE32Exec : Fintype TorchLean.Floats.IEEE754.IEEE32Exec

Small helper lemmas about the IEEE32Exec order

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExecLemmas.compare_self_of_isNaN_false (x : F) (hx : TorchLean.Floats.IEEE754.IEEE32Exec.isNaN x = false) : TorchLean.Floats.IEEE754.IEEE32Exec.compare x x = some Ordering.eq

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExecLemmas.le_self_of_isNaN_false (x : F) (hx : TorchLean.Floats.IEEE754.IEEE32Exec.isNaN x = false) : x ≤ x

Interval domain I (Eq. 6)

inductive NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I : Type

• top : I
• range : F → F → I

@[implicit_reducible]

instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.instReprI : Repr I

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.instReprI.repr : I → ℕ → Std.Format

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.γI : I → Set F

Concretization γ for abstract intervals (Eq. 7).

@[implicit_reducible]

instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.instMembershipF : Membership F I

Membership in an abstract interval, via the concretization γI.

@[reducible, inline]

abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.Box (d : ℕ) : Type

Abstract boxes B ∈ I^d.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.γ {d : ℕ} (B : Box d) : Set (Fin d → F)

Concretization γ for boxes (Eq. 7).

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.InCube {d : ℕ} (B : Box d) : Prop

A box is in [-1,1]^d (paper: “abstract boxes in [-1,1]^d”).

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.mem_top (x : F) : x ∈ top

@[simp]

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.mem_range_iff (x a b : F) : x ∈ range a b ↔ a ≤ x ∧ x ≤ b

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.point (x : F) : I

Point interval ⟨x,x⟩.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.mem_point_of_isNaN_false (x : F) (hx : TorchLean.Floats.IEEE754.IEEE32Exec.isNaN x = false) : x ∈ point x

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.pointBox {d : ℕ} (x : Fin d → F) : Box d

Point box ⟨x,x⟩^d.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.I.mem_pointBox_of_isNaN_false {d : ℕ} (x : Fin d → F) (hx : ∀ (i : Fin d), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (x i) = false) : x ∈ γ (pointBox x)

Executable interval operators for +, *, and ReLU

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.min2 (x y : F) : F

Minimum of two IEEE32Exec values (NaN-aware, via IEEE32Exec.minimum).

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.max2 (x y : F) : F

Maximum of two IEEE32Exec values (NaN-aware, via IEEE32Exec.maximum).

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.min4 (a b c d : F) : F

Minimum of four IEEE32Exec values, computed via nested min2.

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.max4 (a b c d : F) : F

Maximum of four IEEE32Exec values, computed via nested max2.

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.hasNaN4 (a b c d : F) : Bool

Return true iff any of the four arguments is NaN.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.addSharpCorners : I → I → I

Corner-based interval addition for IEEE32Exec.add.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.mulSharpCorners : I → I → I

Corner-based interval multiplication for IEEE32Exec.mul.

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.relu (x : F) : F

Executable ReLU for IEEE32Exec, defined via IEEE32Exec.maximum.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.reluSharpEndpoints : I → I

Exact ReLU♯ for intervals, using monotonicity of ReLU: for ⟨a,b⟩, ReLU([a,b]) = [ReLU(a), ReLU(b)].

Eq. (8): exact interval hull on finite sets

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.toERealTotal (x : F) : EReal

Totalized extended-real interpretation (defaults to 0 only on NaN).

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.le_iff_toERealTotal_le_of_isNaN_false (x y : F) (hx : TorchLean.Floats.IEEE754.IEEE32Exec.isNaN x = false) (hy : TorchLean.Floats.IEEE754.IEEE32Exec.isNaN y = false) : x ≤ y ↔ toERealTotal x ≤ toERealTotal y

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.exists_chooseMin (s : Finset F) (hs : s.Nonempty) : ∃ x ∈ s, toERealTotal x = (Finset.image toERealTotal s).min' ⋯

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.exists_chooseMax (s : Finset F) (hs : s.Nonempty) : ∃ x ∈ s, toERealTotal x = (Finset.image toERealTotal s).max' ⋯

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.chooseMin (s : Finset F) (hs : s.Nonempty) : F

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.chooseMax (s : Finset F) (hs : s.Nonempty) : F

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.chooseMin_spec (s : Finset F) (hs : s.Nonempty) : chooseMin s hs ∈ s ∧ toERealTotal (chooseMin s hs) = (Finset.image toERealTotal s).min' ⋯

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.chooseMax_spec (s : Finset F) (hs : s.Nonempty) : chooseMax s hs ∈ s ∧ toERealTotal (chooseMax s hs) = (Finset.image toERealTotal s).max' ⋯

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.hull (s : Finset F) : I

Interval hull for a finite set of floats:

• ⊤ if the set contains a NaN (paper: ⊥ ∈ S), otherwise
• the interval ⟨min S, max S⟩.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.mem_hull_of_mem (s : Finset F) {x : F} (hx : x ∈ s) : x ∈ hull s

Interval ops ⊕♯/⊗♯/σ♯ instantiated from hull

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.γFinsetI : I → Finset F

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.γFinsetBox {d : ℕ} (B : I.Box d) : Finset (Fin d → F)

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.mem_γFinsetBox_iff {d : ℕ} (B : I.Box d) (x : Fin d → F) : x ∈ γFinsetBox B ↔ ∀ (i : Fin d), x i ∈ B i

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.box2 (A B : I) : I.Box 2

Build a 2D box from two intervals (coordinate 0 is A, coordinate 1 is B).

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.addSharp : I → I → I

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.mulSharp : I → I → I

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.reluSharp : I → I

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.sumSharp {n : ℕ} (ts : Fin n → I) : I

Interval summation ◦∑♯ from the paper: fold with addSharp.

OpsExact implements the finite interval semantics used for exact interval-image statements.

Proving its soundness for IEEE32Exec (+/*/ReLU) is substantial work. This file isolates that work behind an explicit interface, so higher-level semantic proofs can be completed once op-level soundness lemmas are available.

class NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.Sound : Prop

• add_sound {A B : I} {x y : F} : x ∈ A → y ∈ B → TorchLean.Floats.IEEE754.IEEE32Exec.add x y ∈ addSharp A B
• mul_sound {A B : I} {x y : F} : x ∈ A → y ∈ B → TorchLean.Floats.IEEE754.IEEE32Exec.mul x y ∈ mulSharp A B
• relu_sound {A : I} {x : F} : x ∈ A → relu x ∈ reluSharp A

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.add_sound (A B : I) {x y : F} : x ∈ A → y ∈ B → TorchLean.Floats.IEEE754.IEEE32Exec.add x y ∈ addSharp A B

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.mul_sound (A B : I) {x y : F} : x ∈ A → y ∈ B → TorchLean.Floats.IEEE754.IEEE32Exec.mul x y ∈ mulSharp A B

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.relu_sound (A : I) {x : F} : x ∈ A → relu x ∈ reluSharp A

instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.instSound : Sound

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.sumSharp_sound [Sound] {n : ℕ} (ts : Fin n → I) (t : Fin n → F) (ht : ∀ (i : Fin n), t i ∈ ts i) : List.foldl (fun (acc : TorchLean.Floats.IEEE754.IEEE32Exec) (i : Fin n) => acc.add (t i)) Numbers.zero (List.finRange n) ∈ sumSharp ts

Exact interval-image property for rounded targets

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExactImage.Icc (a b : F) : Set F

Float interval set {x | a ≤ x ∧ x ≤ b} (avoids needing Preorder).

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExactImage.IsMinOn {X : Type} (g : X → F) (S : Set X) (m : F) : Prop

m is a minimum of g on the set S, stated without choosing a canonical min.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExactImage.IsMaxOn {X : Type} (g : X → F) (S : Set X) (M : F) : Prop

M is a maximum of g on the set S, stated without choosing a canonical max.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExactImage.ExactIntervalImage {d : ℕ} (g _ν : (Fin d → F) → F) (nuInt : I.Box d → I) : Prop

For each box B, the abstract output interval is exactly the interval hull of the rounded target's direct image on γ(B), expressed via existential min/max witnesses.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExactImage.exactIntervalImage_constant {d : ℕ} (c : F) (hc : TorchLean.Floats.IEEE754.IEEE32Exec.isNaN c = false) : ExactIntervalImage (fun (x : Fin d → F) => c) (fun (x : Fin d → F) => c) fun (x : I.Box d) => I.range c c

Two-layer interval evaluator using OpsExact

structure NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.Net (d h : ℕ) : Type

Parameters of a 2-layer MLP of shape d → h → 1 for the exact interval semantics (OpsExact).

• W1 : Fin h → Fin d → F

  Weight matrix for layer 1.

• b1 : Fin h → F

  Bias for layer 1.

• W2 : Fin 1 → Fin h → F

  Weight matrix for layer 2.

• b2 : Fin 1 → F

  Bias for layer 2.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.aff {d m : ℕ} (W : Fin m → Fin d → F) (b : Fin m → F) (x : Fin d → F) : Fin m → F

Apply an affine layer to an input vector using IEEE32Exec arithmetic.

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.eval {d h : ℕ} (net : Net d h) (x : Fin d → F) : F

Evaluate a 2-layer ReLU MLP on a concrete input, using the exact op wrappers (OpsExact.relu).

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.affSharp {d m : ℕ} (W : Fin m → Fin d → F) (b : Fin m → F) (B : I.Box d) : I.Box m

Interval affine transform aff♯ using corner multiplication and interval summation.

noncomputable def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.evalSharp {d h : ℕ} (net : Net d h) (B : I.Box d) : I

Interval semantics ν♯ for 2-layer ReLU MLPs.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.aff_sound [OpsExact.Sound] {d m : ℕ} (W : Fin m → Fin d → F) (b : Fin m → F) (B : I.Box d) (hW : ∀ (i : Fin m) (j : Fin d), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (W i j) = false) (hb : ∀ (i : Fin m), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (b i) = false) {x : Fin d → F} : x ∈ I.γ B → aff W b x ∈ I.γ (affSharp W b B)

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.eval_sound [OpsExact.Sound] {d h : ℕ} (net : Net d h) (B : I.Box d) (hW1 : ∀ (i : Fin h) (j : Fin d), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.W1 i j) = false) (hb1 : ∀ (i : Fin h), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.b1 i) = false) (hW2 : ∀ (i : Fin 1) (j : Fin h), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.W2 i j) = false) (hb2 : ∀ (i : Fin 1), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.b2 i) = false) {x : Fin d → F} : x ∈ I.γ B → eval net x ∈ evalSharp net B

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.interval_semantics_sound [OpsExact.Sound] {d h : ℕ} (net : Net d h) (B : I.Box d) (hW1 : ∀ (i : Fin h) (j : Fin d), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.W1 i j) = false) (hb1 : ∀ (i : Fin h), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.b1 i) = false) (hW2 : ∀ (i : Fin 1) (j : Fin h), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.W2 i j) = false) (hb2 : ∀ (i : Fin 1), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.b2 i) = false) : eval net '' I.γ B ⊆ (evalSharp net B).γI

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.MLP2Exact.eval_sound_pointBox [OpsExact.Sound] {d h : ℕ} (net : Net d h) (x : Fin d → F) (hx : ∀ (i : Fin d), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (x i) = false) (hW1 : ∀ (i : Fin h) (j : Fin d), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.W1 i j) = false) (hb1 : ∀ (i : Fin h), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.b1 i) = false) (hW2 : ∀ (i : Fin 1) (j : Fin h), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.W2 i j) = false) (hb2 : ∀ (i : Fin 1), TorchLean.Floats.IEEE754.IEEE32Exec.isNaN (net.b2 i) = false) : eval net x ∈ evalSharp net (I.pointBox x)