Configured binary two-layer ReLU approximation bound #
This file proves the reusable three-term error decomposition for executing a single-hidden-layer ReLU MLP over any configured executable binary format and model codec.
The theorem separates the three mathematically different sources of error:
- real approximation: the ideal real-valued ReLU MLP approximates the target,
- parameter quantization: the real MLP is close to the real interpretation of the binary parameters, and
- execution: the executable graph, interpreted back into $\mathbb{R}$, is close to the real graph with those interpreted parameters.
This is the finite-dimensional analogue of the hinge-network executable bound in
UniversalApproximationBinaryExec. The decomposition follows the standard numerical-analysis
pattern for floating-point algorithms: prove the real algorithm correct, bound data/parameter
rounding, and bound arithmetic rounding separately. For background, see IEEE Std 754-2019,
Goldberg (1991), Higham (2002), and the ReLU density literature of Cybenko, Hornik, Leshno, and
Pinkus.
Three-term bound #
Read this as:
Given a configured binary input xI, let $x_R$ be its real interpretation (toReal elementwise).
If:
- the target $f$ is approximated by a real two-layer ReLU MLP with error at most $\varepsilon_{\mathrm{approx}}$,
- the real MLP is close to the real interpretation of the binary parameters, with error at most $\varepsilon_Q$,
- executing the binary MLP and then mapping to reals is close to the real interpretation of those binary parameters, with error at most $\varepsilon_R$,
then the binary execution approximates $f$ within $\varepsilon_{\mathrm{approx}}+\varepsilon_Q+\varepsilon_R$.
Combine real approximation, parameter quantization, and execution error on a set of inputs.
The execution bound is a hypothesis about Model.toReal, including its treatment of exceptional
values; this theorem does not supply a rounding or finiteness bound.