FP32 MLP Approximation #
This module builds on NN.Proofs.RuntimeApprox.FP32.Layers and packages end-to-end error bounds
for small MLP patterns that show up frequently in examples and verification pipelines.
The theorems here are intentionally architecture-shaped rather than fully generic. They are the readable bridge lemmas that downstream verification examples can cite: “this whole FP32 MLP is within some explicit real error budget of the corresponding real-spec MLP.”
The _fp32 suffix refers to the rounded-real model TorchLean.Floats.FP32 := NF binaryRadix fexp32 rnd32, not to Lean's Float32 or to the bit-level ExecFloat.Binary 8 23 model. Finite binary32
add/mul
refinements are in NN/Floats/IEEEExec/Bridge/Finite.lean; further arithmetic refinements are in
NN/Proofs/RuntimeApprox/IEEE32/Arithmetic.lean.
Explicit propagated error budget for Linear → tanh → Linear → tanh → Linear.
Instances For
Compositional FP32 approximation theorem for a 3-layer tanh MLP:
Linear → tanh → Linear → tanh → Linear.
Each parameter/input hypothesis is an approxTensor statement comparing the real-spec tensor with
the FP32 runtime tensor. The conclusion exposes the composed tanhMlp3ErrorBudget, built from the
NF backend's matrix-vector, activation, and addition bounds.
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.