FP32 MLP Approximation #
Compose the generic layer and activation bounds for a three-layer tanh MLP and a two-layer
ReLU MLP. These are rounded-real TorchLean.Floats.FP32 bounds, not native kernel guarantees;
the numerical model and separate IEEE refinements are described in
NN.Proofs.RuntimeApprox.FP32.Layers.
Error budget for Linear → tanh → Linear → tanh → Linear.
Each tanh uses the coarse boundedness estimate 2 + ULP/2, independent of its input-error
magnitude. Thus the first two layers' error magnitudes do not affect the final budget; they are
not propagated through a Lipschitz estimate.
Instances For
Compositional FP32 approximation theorem for a 3-layer tanh MLP:
Linear → tanh → Linear → tanh → Linear.
The parameter/input hypotheses compare real-spec tensors with rounded-real tensors. The
conclusion uses tanhMlp3ErrorBudget, including its coarse tanh estimates rather than tight
propagation of the earlier layers' errors.
2-layer ReLU MLP #
This is the FP32 analogue of the 2-layer ReLU MLP used by CROWN/IBP:
Linear → ReLU → Linear.
Note: the runtime ReLU here is the rounded variant reluR used by the NFBackend forward
approximation framework (apply max · 0 in $\mathbb R$, then round once).
Explicit propagated error budget for Linear → ReLU → Linear.
Instances For
Compositional FP32 approximation theorem for a 2-layer ReLU MLP:
Linear → ReLU → Linear.
This is the network-level bound consumed by the CROWN/IBP integration in
NN.Proofs.RuntimeApprox.FP32.CROWN.