Quando i compilatori possono spostare in sicurezza le scale MXFP4

Se due calcoli matematicamente equivalenti possono dare risultati binary32 diversi, quando può un compilatore cambiarne l’ordine senza cambiare il prodotto scalare di un blocco?

La risposta è importante per ottimizzare l’aritmetica MXFP4: la riscrittura è consentita solo in funzione delle scale e dell’albero usato per sommare i prodotti.

Gli autori codificano l’arrotondamento binary32 con regole intere e dimostrano una condizione sui codici di scala che permette ai compilatori di spostare in sicurezza le scale MXFP4 per un albero di addizioni fisso.

Per stabilire se un compilatore possa spostare le scale condivise attraverso una riduzione del prodotto scalare in MXFP4, occorre considerare l’arrotondamento binary32, l’overflow e l’albero di addizioni scelto.

L’articolo trasforma la domanda di equivalenza in un modello intero dei due calcoli, poi dimostra un intervallo sufficiente per i codici di scala e per la somma dei loro esponenti.

Per un albero fisso, la dimostrazione mantiene al di sotto dell’overflow le somme parziali della forma diretta in ogni nodo interno, esclusa la radice, così che i due calcoli coincidano alla radice anche se entrambi vanno in overflow.

Le verifiche con un solver hanno mostrato che il limite è preciso nelle 26 configurazioni testate: nessuna ha dato un controesempio al limite, mentre ognuna ne ha dato uno al valore dell’esponente immediatamente superiore.

La garanzia vale per le operazioni binary32 indicate, con underflow graduale e un albero di riduzione certificato e fisso. Copre la riscrittura all’interno del blocco; per una moltiplicazione di matrici completa servono anche lo stesso ordine di accumulo esterno e le stesse operazioni aritmetiche.