IEEE32 executable ReLU approximation #
IEEE32Exec-facing theorems for combining:
- real-valued hinge-network approximation results, and
- a proved rounding/error bound for executing that hinge network with IEEE binary32 rounding.
The file is organized as a refinement stack:
hingeFunIeeedefines the executable network using IEEE-754 binary32 operations;HingeSumFiniterecords the exact finiteness obligations needed to rule out NaN/Inf paths;- bridge lemmas connect the executable values, via
IEEE32Exec.toReal, to the rounded-ℝFP32semantics; and - the final theorem packages real approximation, FP32 rounding, and IEEE execution into one certified error bound.
The construction exposes the finite-execution hypotheses at theorem boundaries: they are the
precise trust boundary between mathematical approximation and concrete floating-point execution.
The floating-point viewpoint follows IEEE Std 754-2019 and the standard analyses of
Goldberg and Higham; the approximation side reuses the constructive hinge-network development in
UniversalApproximation and UniversalApproximationFP32.
FP32 model type (rounded ℝ) used as the comparison target for IEEE32Exec error bounds.
Instances For
Embedding IEEE32Exec values into the FP32 (rounded-ℝ) model #
Instances For
Pointwise embedding of a vector of IEEE32Exec values into the FP32 model.
Instances For
IEEE32Exec hinge network (same shape as hinge_fun_fp32) #
One hinge term cᵢ * ReLU(x - tᵢ) evaluated in the executable IEEE32Exec backend.
Instances For
Fold step for summing hinge terms, used by hinge_sum_ieee.
Instances For
Executable IEEE32Exec sum of hinge terms, in the fixed List.finRange order.
Instances For
Executable IEEE32Exec hinge network: sum hinge terms, then add the executable bias.
Instances For
A finiteness witness for IEEE evaluation (no NaN/Inf intermediates) #
- nil {n : ℕ} {t c : Fin n → TorchLean.Floats.IEEE754.IEEE32Exec} {x acc : TorchLean.Floats.IEEE754.IEEE32Exec} (hacc : acc.isFinite = true) : HingeSumFinite t c x acc []
- cons {n : ℕ} {t c : Fin n → TorchLean.Floats.IEEE754.IEEE32Exec} {x acc : TorchLean.Floats.IEEE754.IEEE32Exec} {i : Fin n} {xs : List (Fin n)} (hsub : (x.sub (t i)).isFinite = true) (hmax : ((x.sub (t i)).maximum Numbers.zero).isFinite = true) (hmul : (hingeTermIeee c t x i).isFinite = true) (hadd : (acc.add (hingeTermIeee c t x i)).isFinite = true) (hrest : HingeSumFinite t c x (acc.add (hingeTermIeee c t x i)) xs) : HingeSumFinite t c x acc (i :: xs)
Instances For
Discharging HingeSumFinite for concrete networks by computation #
For typical verification workflows, t, c, and x are concrete IEEE32Exec constants
coming from a compiled model artifact. In that setting, the easiest way to satisfy the
HingeSumFinite … hypotheses is to compute the IEEE32Exec kernel and check finiteness at
every intermediate.
instDecHingeSumFinite provides a Decidable instance generator for HingeSumFinite ….
This enables proofs like:
classical
haveI := IEEE32ExecReLUApprox.instDecHingeSumFinite (t := t) (c := c) (x := x)
(acc := (Numbers.zero : IEEE32Exec)) (xs := List.finRange n)
have hSum : HingeSumFinite t c x (Numbers.zero : IEEE32Exec) (List.finRange n) := by
decide
This does not solve the symbolic “no overflow for all x” problem, but it makes the pointwise theorems in this file directly usable for concrete executions.
Instances For
A compact finiteness hypothesis bundle (pointwise) #
Instances For
Unpack the compact pointwise finiteness bundle.
The executable bridge lemmas need separate finiteness facts for the input, parameters, fold state, and final output. Keeping the bundled form at theorem boundaries makes user-facing statements shorter, while this projection feeds the stepwise IEEE-754 refinement proofs.
Refinement: IEEE32Exec execution equals FP32 rounded-ℝ execution (as reals) #
Refine an executable IEEE hinge-term fold to the FP32 rounded-ℝ fold with the same order.
Floating-point addition is not associative, so the theorem preserves the exact List.finRange
evaluation order. This is why the proof is fold-based rather than rewriting directly to an
unordered finite sum.
Refine the whole executable hinge network to the FP32 rounded-ℝ network.
The theorem composes the fold refinement with the final rounded bias addition. Its hypotheses are exactly the finiteness obligations needed by the IEEE-754 bridge lemmas.
IEEE32Exec error bound inherited from the FP32 bound #
Lift the FP32 hinge-network rounding error bound to executable IEEE32Exec evaluation.
Once toReal_hinge_fun_ieee_eq_fp32_val identifies the executable result with the FP32 model, the
already-proved FP32 error bound transfers directly.
“Approximation error + rounding error” (pointwise) #
Pointwise triangle bound: target error to executable output is bounded by real approximation error plus the certified FP32/IEEE rounding error.
Strict version of hinge_fun_total_abs_error_ieee_le, useful for approximation theorems.
IEEE32Exec pointwise ReLU approximation packaging (1D) #
1D ReLU approximation statement over IEEE32Exec values.
This is not a full universal approximation theorem, because it does not construct IEEE weights
from a real target. Instead it packages the already-proved pointwise inequality
hinge_fun_total_abs_error_ieee_lt into an existence/for-all form:
- assume there exist IEEE32Exec hinge parameters
(t,c,b0)that approximatefat the real level (viahinge_fun_realon the embedded reals), - and assume a finiteness/no-NaN/no-Inf witness for IEEE32Exec evaluation,
- then IEEE32Exec evaluation approximates
fwith an explicit extra rounding termhinge_fun_error_bound.
Real approximation + quantization + IEEE rounding (1D, pointwise) #
1D IEEE32Exec ReLU approximation with an explicit 3-term error decomposition:
- Real approximation error:
|f(r) - hinge_fun … r| < εApprox - Quantization/reference error:
|hinge_fun … r - hinge_fun_real (embed IEEE-params) (embed r)| ≤ εQ - IEEE rounding error (proved):
hinge_fun_error_bound …
To obtain a fully synthesized IEEE32Exec approximation theorem, callers must additionally:
- construct IEEE32Exec parameters
(t,c,b0)from the real hinge parameters, and - prove the finiteness/no-NaN/no-Inf witnesses (
HingeSumFinite+ finite output), and - prove a uniform bound
εQfor the parameter-quantization step.
Pointwise wrappers that take HingeEvalFiniteProp #
Pointwise strict error theorem using the compact finiteness bundle.
Use this form when a checker or proof generator has produced one HingeEvalFiniteProp certificate
instead of separate hypotheses for input, parameter, fold, and output finiteness.
Same 3-term theorem, but with an explicit real bias parameter #
Three-term IEEE32Exec approximation theorem with a caller-supplied real bias.
reluApproximationIccIEEE32Exec_threeTerm uses f a as the real hinge-network bias because that
is what the constructive one-dimensional interpolation theorem emits. This variant is the more
general numerical-analysis statement: any real reference bias bR may be compared with the
executable bias b0.
Dyadic (roundDyadicToIEEE32) quantization helpers #
Generic half-ulp absolute-error bound for the rounded-ℝ binary32 model.
This is the standard floating-point local rounding statement specialized to TorchLean's FP32 format parameters. It is the bridge from abstract approximation coefficients to explicit quantization budgets.
Half-ulp error bound for dyadic values rounded into executable IEEE32Exec values.
The finiteness hypothesis excludes overflow/NaN paths, after which roundDyadicToIEEE32 agrees
with the same real fp32Round operation used by the FP32 model.
Real hinge network sensitivity to parameter rounding (for a compact input domain) #
This is the “εQ quantization” step for
reluApproximationIccIEEE32Exec_threeTerm.
The lemma below uses the compact-domain assumption that the reference knot locations tR
lie in the input interval [a,b], then bounds the output perturbation using:
- a width term
|b-a|to boundrelu(x - tR i)on the interval, and relu_lipschitzto control the sensitivity to perturbingt.
Sensitivity of a real hinge network to perturbing all parameters on a compact interval.
The bound decomposes into a bias perturbation, a coefficient perturbation weighted by the interval
width, and a knot perturbation weighted by the absolute executable coefficients. This is the real
analysis step that supplies the quantization term εQ.
Uniform version of hinge_fun_abs_error_le_of_params_Icc.
Instead of summing per-neuron perturbation bounds, this theorem uses uniform coefficient and knot
budgets Δc, C, and Δt, producing the simpler expression
|bR-bI| + n * (Δc * |b-a| + C * Δt).
Removing the quantization term when reals are exactly representable #
The embedded FP32/IEEE real reference is exactly the ordinary real hinge network evaluated on
entrywise IEEE32Exec.toReal parameters.
Uniform quantization-error bound between a real hinge network and executable IEEE parameters.
This is the user-facing εQ discharge lemma when callers can bound coefficient and knot rounding
errors uniformly.
Dyadic-to-IEEE32Exec quantization bound (εQ) #
This lemma is a drop-in way to discharge the εQ premise of
reluApproximationIccIEEE32Exec_threeTerm when IEEE parameters are obtained by
rounding dyadic rationals via roundDyadicToIEEE32.
Dyadic quantization error for a hinge network on [a,b].
The real reference uses exact dyadic parameters, while the executable reference uses those dyadics rounded to IEEE32Exec values. The result is still expressed as a sum of concrete per-parameter rounding errors.
Dyadic quantization error with each per-parameter rounding error bounded by a half-ulp term.
This is the more automated version of hinge_fun_dyadic_quantization_error_le_Icc: callers provide
finiteness of every rounded dyadic value, and the theorem substitutes the standard half-ulp bounds.
Packaged “dyadic quantization + IEEE rounding” theorem (1D, pointwise) #
This is the “dyadic next step”: it replaces the abstract εQ premise of
reluApproximationIccIEEE32Exec_threeTerm_bias with a concrete bound coming from:
- dyadic→FP32 rounding (
≤ 1/2 ulp), and - a Lipschitz-style sensitivity bound for the real hinge network on
x ∈ [a,b].
It still assumes the IEEE finiteness witnesses for evaluation (HingeSumFinite + finite output).
Two-term 1D IEEE32Exec ReLU approximation statement:
- assume the real hinge network built from the IEEE parameters’
toRealvalues already approximatesfontoRealinputs in[a,b], - and assume finiteness/no-NaN/no-Inf witnesses,
- then IEEE execution approximates
fwith an explicit IEEE rounding term.
This is a specialization of the 3-term theorem with εQ = 0.