Mixing Condition Numbers and Oracles for Accurate Floating-point Debugging

Titre : Mélange des nombres de condition et des oracles pour un débogage précis en virgule flottante

1. Problématique

Les nombres en virgule flottante approximent les valeurs réelles mais introduisent des erreurs subtiles (arrondis, débordements, sous-débordements) qui peuvent avoir des conséquences catastrophiques. Deux approches principales existent pour détecter ces erreurs, mais chacune présente des limites majeures :

• Les outils de débogage dynamiques (basés sur des oracles) : Des outils comme Herbgrind ou EFTSanitizer utilisent des calculs en haute précision (souvent en "double-double") pour servir de référence (oracle) et comparer le résultat flottant.
  • Limite : Les oracles en double-double souffrent des mêmes erreurs d'arrondi que le calcul original dans certains cas critiques (ex: $\sqrt{x+1} - \sqrt{x}$ pour $x$ très grand), entraînant de faux négatifs (erreurs non détectées). De plus, ils ne gèrent pas correctement les débordements (overflow) et sous-débordements (underflow) car leur plage d'exposants est identique à celle du double standard.
• Les outils d'analyse statique (basés sur les nombres de condition) : Des outils comme FPTaylor utilisent des bornes d'erreur dérivées de séries de Taylor et de nombres de condition pour estimer l'erreur maximale sur un domaine d'entrée.
  • Limite : Ces méthodes peinent à gérer les débordements et sous-débordements de manière propre. De plus, elles sont souvent trop lentes pour un débogage interactif et ne localisent pas toujours l'erreur à l'opération spécifique.

Le défi : Combiner la rapidité des outils de débogage et la précision des analyses statiques pour obtenir un outil à la fois rapide, précis et capable de gérer tous les types d'erreurs flottantes.

2. Méthodologie : EXPLANIFLOAT

L'article présente EXPLANIFLOAT, un outil de débogage hybride qui fusionne les techniques de nombres de condition et d'oracles pour surmonter les limites des approches précédentes.

A. Détection des erreurs d'arrondi via les nombres de condition
Au lieu de comparer directement la valeur flottante à une valeur oracle (ce qui est sujet aux erreurs d'arrondi de l'oracle lui-même), EXPLANIFLOAT calcule le nombre de condition de chaque opération.

• Le nombre de condition $\Gamma_f(x)$ mesure l'amplification de l'erreur relative d'entrée par la fonction $f$.
• Si le nombre de condition dépasse un seuil, l'opération est signalée comme potentiellement instable.
• Avantage : Cette méthode est robuste car elle ne dépend pas de la précision d'un oracle pour la détection, mais uniquement de la propriété mathématique de la fonction.
• Affinement : Pour éviter les faux positifs sur des fonctions comme $\sin(x)$ (qui ont un nombre de condition élevé pour de grandes entrées ou près de multiples de $\pi$), l'outil scinde les nombres de condition en deux parties :
  • Stabilité : Liée à la magnitude de l'entrée (ex: $|x|$ pour $\sin$).
  • Annulation (Cancellation) : Liée à la proximité d'une valeur critique (ex: $|\cot(x)|$ pour $\sin$).
  • L'outil ne signale une erreur que si l'une de ces composantes dépasse le seuil, en ignorant les cas où les arguments sont des constantes exactes.

B. Détection des débordements et sous-débordements via un oracle logarithmique
Les nombres de condition échouent à détecter les débordements car les bornes d'erreur relatives ne s'appliquent plus lorsque le résultat est infini.

• EXPLANIFLOAT introduit un oracle logarithmique séparé.
• Au lieu de stocker la valeur $x$, il stocke $\log_2(|x|)$ (plus le signe).
• Cela permet de représenter des nombres extrêmement grands ou petits sans débordement.
• Logique de détection : Si une opération produit un résultat hors de la plage flottante standard, mais que l'oracle logarithmique indique que la valeur réelle (après renormalisation) serait dans la plage flottante, l'outil vérifie si le résultat flottant diverge de la réalité.
  • Exemple : Si $x^2$ déborde en $\infty$ mais que $\sqrt{1+x^2}$ devrait être fini, l'oracle logarithmique détecte que la divergence est réelle et signale l'erreur.
  • Des exceptions sont faites pour les cas bénins (ex: $1 + \text{underflow}$) où l'erreur est annulée par une opération ultérieure.

C. Architecture d'implémentation (DSL)
L'outil utilise une mémoire "ombre" (shadow memory) pour chaque valeur intermédiaire, représentée par un système numérique hybride appelé DSL (Double-Double, Signe, Logarithme) :

• $(\hat{x}, \hat{r}, s, \hat{e})$ où $\hat{x}$ est la valeur flottante, $\hat{r}$ le résidu (double-double), $s$ le signe, et $\hat{e}$ le logarithme de la magnitude.
• Gestion dynamique :
  • Si la valeur est dans la plage flottante, le composant Double-Double est actif pour le calcul précis des nombres de condition.
  • Si la valeur sort de la plage, le composant Logarithmique prend le relais.
• Bibliothèque : L'implémentation repose sur la bibliothèque qd (pour le double-double) et des algorithmes de réduction de domaine (Payne-Hanek) adaptés pour garantir la précision des fonctions transcendantes (sin, cos, log) sur toute la plage d'entrée, sans utiliser de bibliothèques de précision arbitraire lourdes (comme MPFR) pour les opérations courantes.

3. Contributions Clés

1. Algorithme de débogage basé sur les nombres de condition : Remplacement de la comparaison directe avec un oracle par une analyse de stabilité via les nombres de condition, réduisant les faux négatifs liés aux erreurs d'arrondi de l'oracle.
2. Oracle logarithmique pour les débordements : Une nouvelle méthode pour suivre précisément les valeurs hors de portée et détecter les débordements/sous-débordements réels sans utiliser de précision arbitraire.
3. Implémentation hybride (DSL) : Une architecture efficace combinant double-double et logarithmes, utilisant uniquement des instructions matérielles flottantes standard pour les opérations, assurant ainsi des performances élevées.

4. Résultats Expérimentaux

L'évaluation a été réalisée sur la suite de benchmarks Herbie 2.1 (546 problèmes numériques complexes).

• Précision et Rappel (Performance) :
  • EXPLANIFLOAT : Précision de 80,0 % et Rappel de 96,1 %.
  • Oracle Double-Double (État de l'art) : Précision de 56,5 % et Rappel de 65,4 %. (Beaucoup de faux négatifs dus aux erreurs d'arrondi de l'oracle).
  • Base de référence Précision Arbitraire (Ground Truth) : Précision de 83,2 % et Rappel de 98,1 %.
• Performance (Vitesse) :
  • EXPLANIFLOAT est 4,24 fois plus rapide que l'approche utilisant une bibliothèque de précision arbitraire (Rival/MPFR).
  • Il évite les allocations mémoire et les calculs lourds, se rapprochant de la vitesse des outils purement flottants.
• Analyse des cas limites :
  • L'outil gère correctement des cas complexes comme les annulations dans des sommes de grands nombres ou les sous-débordements résiduels, là où les oracles classiques échouent.
  • Quelques faux positifs subsistent (ex: erreurs minimes amplifiées par un grand nombre de condition mais négligeables dans le résultat final), mais ils sont rares.

5. Signification et Conclusion

Ce papier démontre qu'il est possible de combiner les techniques de débogage dynamique (rapides) et d'analyse statique (précises) pour créer un outil de débogage numérique supérieur.

• Innovation : Le passage d'une logique de "comparaison de valeurs" à une logique de "mesure de sensibilité" (nombres de condition) pour les erreurs d'arrondi, couplée à une logique logarithmique pour les extrêmes, résout le compromis historique entre vitesse et précision.
• Impact : EXPLANIFLOAT offre une alternative viable aux outils lents de précision arbitraire, permettant un débogage interactif et fiable pour des programmes numériques complexes, tout en évitant les pièges des oracles en double-double.
• Ouverture : Bien que l'implémentation actuelle soit orientée vers la débogabilité plutôt que la performance maximale, les résultats suggèrent un potentiel énorme pour l'intégration dans des compilateurs ou des environnements de développement pour la science des données et le calcul scientifique.