Quand un compilateur peut déplacer les échelles MXFP4 sans risque
En termes simples
MXFP4 stocke de petits nombres dans des blocs qui partagent des échelles. Un compilateur peut appliquer ces échelles à chaque nombre avant de les additionner, ou faire l’addition d’abord puis appliquer les échelles ensuite.
En mathématiques ordinaires, les deux ordres donnent le même résultat, mais les arrondis et les dépassements de capacité propres aux calculs informatiques peuvent les faire diverger. L’article donne une condition qui indique quand un compilateur peut changer l’ordre sans risque pour un arbre d’addition fixé. Une preuve établit cette condition ; les vérifications par solveur montrent que sa limite est précise pour les arbres et les longueurs de bloc testés.
La recherche
Si deux calculs mathématiquement équivalents peuvent produire des résultats binary32 différents, quand un compilateur peut-il changer leur ordre sans modifier le produit scalaire d’un bloc ?
La réponse compte pour optimiser l’arithmétique MXFP4 : la réécriture est permise ou non selon les échelles et l’arbre utilisé pour additionner les produits.
Les auteurs encodent les arrondis binary32 sous forme de règles sur les entiers et prouvent une condition sur les codes d’échelle qui permet aux compilateurs de déplacer sans risque les échelles MXFP4 pour un arbre d’addition fixé.
Pour déterminer si un compilateur peut déplacer des échelles partagées à travers une réduction de produit scalaire MXFP4, il faut tenir compte des arrondis en binary32, des dépassements de capacité et de l’arbre d’addition choisi.
L’article transforme cette question d’équivalence en un modèle entier des deux calculs, puis prouve une plage suffisante pour les codes d’échelle et leur exposant combiné.
Pour un arbre fixé, la preuve maintient les sommes partielles de la forme directe sous le seuil de dépassement de capacité à chaque nœud intermédiaire hors racine. Les deux calculs donnent donc le même résultat à la racine, même s’ils dépassent tous deux la capacité à cet endroit.
Les vérifications par solveur indiquent que la limite est précise dans 26 configurations testées : aucune ne diverge à la limite, tandis que chacune présente un contre-exemple un exposant au-dessus.
La garantie vaut pour l’arithmétique binary32 indiquée, les sous-flux progressifs et un arbre de réduction certifié et fixe. Elle couvre la réécriture au sein d’un bloc ; une multiplication matricielle complète exige aussi que l’ordre et l’arithmétique de l’accumulation externe soient identiques.
Analyse
Détails
- Auteurs de l’article original
- Shreyas Vinayakumar
- Soumis à arXiv
- Licence
- CC BY 4.0