In plain words
MXFP4 stores small numbers in blocks with shared scales. A compiler can apply those scales to every number before adding, or add first and apply the scales afterward. The two orders match in ordinary math, but rounding and overflow in computer arithmetic can make them differ.
The paper gives a condition for when a compiler may safely change the order for a fixed addition tree. A proof establishes the condition; solver checks show its limit is sharp for the tested trees and block lengths.
The research
If two mathematically equal calculations can return different binary32 results, when may a compiler change their order without changing a block dot product? The answer matters for optimizing MXFP4 arithmetic: the legal rewrite depends on the scales and on the tree used to add the products.
The authors encode binary32 rounding as integer rules and prove a scale-code condition that lets compilers move MXFP4 scales safely for a fixed addition tree.
To know whether a compiler can move shared scales across an MXFP4 dot-product reduction, it must account for binary32 rounding, overflow, and the chosen addition tree.
The paper turns that equivalence question into an integer model of the two calculations, then proves a sufficient range for the scale codes and their combined exponent.
For a fixed tree, the proof keeps direct-form partial sums at every proper, non-root node below overflow, so both calculations agree at the root, even if both overflow there.
Solver checks found the bound sharp for 26 tested configurations: none failed at the bound, while each had a counterexample one exponent step above it.
The guarantee is for the stated binary32 arithmetic, gradual underflow, and a fixed certified reduction tree. It covers the block-local rewrite; a full matrix multiplication also needs matching outer accumulation order and arithmetic.
Analysis
Deep
- Original paper authors
- Shreyas Vinayakumar
- Submitted to arXiv
- License
- CC BY 4.0