Floating-Point Interval Semantics

Interval-domain semantics for ExecFloat.Binary 8 23 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.

ExecFloat.Binary 8 23 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.

@[instance_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

UInt32 is finite, via the injection into Fin (2 ^ 32).

@[instance_reducible]

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

Hence a Fintype, classically.

instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.FintypeInstances.instFiniteBinaryOfNatNatIeeeDefaultBias_nN : Finite (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) F._proof_1 F._proof_2 F._proof_3 F._proof_4)

Binary32 is finite, since it is determined by its bits.

@[instance_reducible]

noncomputable instance NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.FintypeInstances.instFintypeBinaryOfNatNatIeeeDefaultBias_nN : Fintype (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) F._proof_1 F._proof_2 F._proof_3 F._proof_4)

Hence a Fintype. This is what makes the interval hull below a Finset construction and the abstract operators exact rather than approximate: the whole float type can be enumerated.

Small helper lemmas about the ExecFloat.Binary 8 23 order

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExecLemmas.compare_self_of_isNaN_false (x : F) (hx : FloatLib.Floats.ExecFloat.Binary.isNaN x = false) : FloatLib.Floats.ExecFloat.compare x x = some Ordering.eq

Comparing a non-NaN float with itself yields eq, infinities included.

theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ExecLemmas.le_self_of_isNaN_false (x : F) (hx : FloatLib.Floats.ExecFloat.Binary.isNaN x = false) : x ≤ x

Reflexivity of ≤ away from NaN, which is as much as IEEE 754 order gives.

Interval domain I (Eq. 6)

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

The interval abstract domain of Eq. 6: either the top element or a pair of float endpoints.

• top : I

  No information: every float is possible.

• range : F → F → I

  The floats between the two endpoints, inclusive.

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

@[instance_reducible]

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

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

Concretization γ for abstract intervals (Eq. 7).

@[instance_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

Everything is in ⊤, NaN included; that is what makes ⊤ the sound fallback.

@[simp]

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

Membership in a range interval unfolds to the two float comparisons.

@[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 : FloatLib.Floats.ExecFloat.Binary.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), FloatLib.Floats.ExecFloat.Binary.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 ExecFloat.Binary 8 23 values (NaN-aware, via min).

@[inline]

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

Maximum of two ExecFloat.Binary 8 23 values (NaN-aware, via max).

@[inline]

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

Minimum of four ExecFloat.Binary 8 23 values, computed via nested min2.

@[inline]

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

Maximum of four ExecFloat.Binary 8 23 values, computed via nested max2.

@[inline]

def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.OpsExact.hasNaNAmongFour (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 ExecFloat.add.

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

Corner-based interval multiplication for ExecFloat.mul.

@[inline]

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

Executable ReLU for ExecFloat.Binary 8 23, defined via max.

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 : FloatLib.Floats.ExecFloat.Binary.isNaN x = false) (hy : FloatLib.Floats.ExecFloat.Binary.isNaN y = false) : x ≤ y ↔ toERealTotal x ≤ toERealTotal y

Away from NaN, float comparison agrees with the order on EReal under the total embedding.

This is the lemma that buys the whole development a linear order to take minima and maxima in: ExecFloat.Binary 8 23 itself has no LinearOrder, but its non-NaN part embeds into one.

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

A nonempty finite set of floats has an element attaining the minimum of its EReal image.

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

Dually, an element attaining the maximum.

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

A minimizing element of s, chosen classically.

Choice rather than computation because several distinct floats can share one EReal value (the two zeros), so "the" minimum is not well defined as a float; every use below only needs some minimizer.

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

A maximizing element of s, chosen classically.

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' ⋯

chooseMin is in the set and attains the minimum of the image.

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' ⋯

chooseMax is in the set and attains the maximum of the image.

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

The hull contains every element of the set it was built from. All three soundness proofs below reduce to this one fact.

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

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

Concretization of an interval as a Finset, by filtering the (finite) float type.

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

Concretization of a box as a Finset of points. Finite because F is, which is what lets the abstract operators be defined as images of concrete ones rather than by endpoint formulas.

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

Membership in the Finset concretization is coordinatewise interval membership.

@[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

Abstract addition +♯: the hull of float addition over the whole input box.

Defined as an image rather than by adding endpoints, because float addition is not monotone in the presence of NaN and signed zeros, so an endpoint formula would not be exact. ⊤ absorbs.

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

Abstract multiplication *♯, again as the hull of the concrete image over the box.

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

Abstract ReLU, the hull of the concrete image.

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.

The Sound class isolates the operation-level obligations used by higher-level semantic proofs. The addition, multiplication, and ReLU obligations are proved below, followed by the canonical ExecFloat.Binary 8 23 instance.

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

The per-operation soundness obligations the interval semantics rests on: every abstract operation must contain the concrete result of any pair of members of its arguments.

• add_sound {A B : I} {x y : F} : x ∈ A → y ∈ B → FloatLib.Floats.ExecFloat.add x y ∈ addSharp A B

  Abstract addition contains every concrete sum of members.

• mul_sound {A B : I} {x y : F} : x ∈ A → y ∈ B → FloatLib.Floats.ExecFloat.mul x y ∈ mulSharp A B

  Abstract multiplication contains every concrete product of members.

• relu_sound {A : I} {x : F} : x ∈ A → relu x ∈ reluSharp A

  Abstract ReLU contains the concrete ReLU of every member.

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

Soundness of abstract addition: concrete sums of members stay in the abstract sum.

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

Soundness of abstract multiplication.

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

Soundness of abstract ReLU.

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 : FloatLib.Floats.ExecFloat (FloatLib.Floats.ExecFloat.Binary.Family 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) F._proof_1 F._proof_2 F._proof_3 F._proof_4)) (i : Fin n) => acc.add (t i)) 0 (List.finRange n) ∈ sumSharp ts

Soundness of the interval sum ◦∑♯: folding concrete additions stays inside the folded intervals.

Proved by induction on the list rather than on Fin n, so that the accumulator interval can vary; the base case needs 0 ∈ ⟨0, 0⟩, which is where the non-NaN side condition on zero comes in.

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 : FloatLib.Floats.ExecFloat.Binary.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

A constant target has an exact interval image: the point interval ⟨c, c⟩.

The easiest instance of the exactness property, and the one the constant-target construction of the paper needs; the nonemptiness hypothesis is what supplies the min and max witnesses.

Two-layer interval evaluator using OpsExact

structure NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.TwoLayerMLPExact.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.TwoLayerMLPExact.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.TwoLayerMLPExact.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.TwoLayerMLPExact.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.TwoLayerMLPExact.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.TwoLayerMLPExact.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), FloatLib.Floats.ExecFloat.Binary.isNaN (W i j) = false) (hb : ∀ (i : Fin m), FloatLib.Floats.ExecFloat.Binary.isNaN (b i) = false) {x : Fin d → F} : x ∈ I.γ B → aff W b x ∈ I.γ (affSharp W b B)

The abstract affine transform is sound, given that no weight or bias is NaN.

Weights enter as point intervals, so the proof is mulSharp soundness coordinatewise, then sumSharp soundness, then one addSharp for the bias, in exactly the order aff computes.

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

The abstract semantics ν♯ of a two-layer ReLU network overapproximates the concrete one.

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

Set-level restatement: the image of the concretization is contained in the abstract output.

This is the form the approximation theorem cites, since it speaks about images of sets rather than about individual points.

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

Specialization to a point box: the abstract semantics contains the concrete value at x.

Worth stating separately because it says the abstraction has no false negatives at single inputs, which is what a verifier reports back to a user.