Alive prouve formellement que les optimisations des compilateurs sont correctes

Lorsque l’on développe une application et que l’on rencontre un problème, la source la plus courante est le code que l’on écrit soi-même. Plus rarement, il s’agit d’un défaut dans les bibliothèques utilisées, exceptionnellement dans le compilateur, jamais dans le processeur. Du moins, c’est ce que bon nombre de programmeurs ont fini par intégrer. Il n’empêche que cette hiérarchie est assez optimiste. Par exemple, les processeurs n’exécutent pas toujours correctement les instructions qui leur sont passées : depuis la mauvaise implémentation de FDIV sur les premiers Pentium jusqu’à la technologie HyperThreading de la dernière génération de processeurs Intel Core ou un problème pas encore identifié sur les AMD Ryzen qui causent un bon nombre d’erreurs de segmentation avec GCC.

Les compilateurs ne font pas exception. Comme les fabricants de processeurs, les développeurs de compilateurs sont sous pression. Ils veulent augmenter la performance des applications compilées/exécutées, augmenter l’efficacité énergétique, etc. De plus, la complexité de ces projets ne fait qu’augmenter : il est impossible de dessiner l’entièreté des processeurs à la main pour leur conception depuis belle lurette, les compilateurs modernes font plusieurs millions de lignes de code qui évoluent rapidement. Ainsi, des défauts sont présents, tant au niveau des compilateurs que des processeurs — des défauts qui peuvent mener à des failles de sécurité béantes.

Un exemple : Heartbleed

Par exemple, pour accéder à une cellule d’un tableau en mémoire, il faut s’assurer que l’adresse est bien dans le tableau : sinon, on peut lire des données normalement inaccessibles pour ce morceau de code (c’est notamment le principe de Heartbleed, qui avait fait beaucoup de bruit en 2014). Pour un bon nombre de langages, ces vérifications sont effectuées à chaque accès au tableau, sauf s’il est possible de prouver que l’accès ne pose aucun problème. Si une optimisation du compilateur fait une erreur à ce moment, la sécurité du programme compilé est mise à mal.

Cette preuve peut se faire en déterminant la plage de valeurs possibles pour l’index et en la comparant à la taille du tableau, par exemple. Toutes les optimisations du compilateur doivent ainsi être écrites précisément : si l’une d’entre elles fait une petite erreur dans le calcul de la plage de valeurs possibles, tout le reste du château s’effondre.

Alive

C’est pourquoi une série de chercheurs s’est associée à Microsoft pour développer Alive, un outil de vérification formel des optimisations effectuées par un compilateur. Il faut tout d’abord décrire l’optimisation dans un langage précis ; ensuite, Alive utilise les technologies actuelles de preuve automatique de théorème (plus précisément, le solveur SMT Z3) pour déterminer si l’optimisation est correcte ou non. Les résultats ne se sont pas faits attendre : très rapidement, une dizaine de défauts ont été trouvés dans LLVM ; Alive a aussi empêché l’introduction d’optimisations fausses dans LLVM et le compilateur C++ de Microsoft.

La suite des travaux de ce groupe envisage une intégration dynamique au compilateur : au lieu de vérifier en amont qu’une optimisation est valide (peu importe le programme à compiler), il s’agit de vérifier si l’optimisation d’un programme s’est déroulée sans anicroche. Ce principe s’appelle validation de la traduction et permet de détecter d’autres types de problèmes, dans les cas où l’optimisation effectuée est hors de portée des programmes de vérification. Notamment, Microsoft déclare avoir déjà pu corriger quelques défauts dans son compilateur C++ grâce à cette méthode, malgré les autres analyses effectuées.

Il n’empêche que ces travaux n’ont pas beaucoup d’intérêt si la sémantique de la représentation intermédiaire (utilisée par les compilateurs pour effectuer les optimisations sans dépendre du langage compilé) n’est pas parfaitement définie : c’est là le prochain axe de recherche, déjà entamé en ce qui concerne les comportements indéfinis (notamment en C et C++).

Source : Getting compilers right: a reliable foundation for secure software.

Des nouveautés du côté de la compression

Au niveau algorithmique, la compression de données sans perte (à la ZIP, RAR, TAR.GZ, 7Z) n’a plus beaucoup évolué ces dernières années : il s’agit toujours d’un assemblage de dictionnaires, de code de Huffman, de codage arithmétique, de modèle statistique. Il n’empêche : ces techniques, bien maîtrisées, peuvent toujours s’améliorer petit à petit et donner des outils de compression redoutablement efficaces, comme Google Brotli, arrivé sur le marché début 2016.

Bien maîtrisées, ces techniques peuvent… faire d’énormes progrès ! C’est ainsi que RAD Games a annoncé de nouveaux outils de compression (propriétaires et payants) qui fonctionnent nettement mieux que la concurrence (principalement libre), en fonction du critère de comparaison. Au niveau de l’implémentation, rien de vraiment neuf, si ce n’est un soin tout particulier apporté par de fins connaisseurs du domaine de la compression, avec et sans pertes.

La société peut maintenant se targuer de proposer un outil de compression dont la principale caractéristique est une décompression extrêmement rapide (de trois à cinq fois plus que zlib) avec des taux de compression du même ordre que LZMA (en étant dix à trente fois plus rapide que ce dernier), nommé Kraken. Il donne aussi du fil à retordre à LZ4 : ce dernier reste le plus rapide sur tous les types de documents, mais Kraken s’en rapproche fortement tout en gardant une compression nettement meilleure que LZ4.

Deux dérivés (disponibles depuis cet été) de cet outil sont plus spécialisés, en compressant moins mais en décompressant (beaucoup) plus vite : Mermaid offre une compression moyenne (du même ordre que ZIP), tout en étant extrêmement rapide en décompression (de sept à douze fois plus que zlib, c’est-à-dire plus de deux fois plus rapide que Kraken) ; Selkie, au contraire, abandonne encore un peu de compression (entre ZIP et LZ4), pour dépasser LZ4 d’un facteur de presque deux (la décompression est très proche d’une copie en mémoire, ce qui est un tour de force technique pour une compression non triviale).

Les chiffres du terrain

Les chiffres donnés sont les officiels, reste encore à les confirmer par des extérieurs. Les comparaisons parfaitement équitables sont difficiles à obtenir, puisque les outils de compression ne sont pas si faciles à obtenir.

En comparant le ratio de compression avec les débits, ces trois outils sont collés du côté des hauts débits (même si Kraken n’y est que peu présent). Zlib occupe une place intermédiaire.

Ces algorithmes sont moins optimisés en temps pour la compression, il n’empêche qu’ils présentent de bons résultats. Ils sont nettement plus éloignés de leurs meilleurs concurrents (comme LZ4… ou zlib).

Du côté algorithmique ?

Ces outils étant propriétaires, difficile d’aller lire leur code source pour comprendre les améliorations proposées. Cependant, certains s’avancent et proposent des pistes qui auraient permis d’atteindre ces nouveaux sommets. Le décodage très rapide pourrait venir d’une utilisation très judicieuse de la hiérarchie mémoire des processeurs actuels : autant de données que possible sont stockées dans les caches du processeur afin de limiter les accès à la mémoire vive (qui sont extrêmement lents).

Une tout autre piste suit la théorie des langages formels, en tentant de construire une grammaire dont le seul mot accepté est le fichier à compresser : les promesses de l’algorithme GLZ sont d’atteindre des taux de compression dignes des algorithmes de prédiction par reconnaissance partielle (la probabilité de rencontrer un symbole — par exemple, un octet — dépend d’un certain nombre de symboles déjà lus) tout en gardant la rapidité des algorithmes de la famille LZ (qui fonctionnent avec des dictionnaires). Les grammaires ainsi générées ont pour particularité d’avoir une entropie faible, c’est-à-dire qu’elles se compressent très bien par d’autres algorithmes.

Toutefois, il semblerait que ces pistes n’aient pas été suivies pour le développement de ces algorithmes. Peut-être nourriront-elles la prochaine génération d’outils de compression ? Cependant, les compromis subsisteront probablement : la révolution d’un algorithme qui compresse très vite et très bien et qui décompresse au moins aussi vite n’est pas encore en vue.

Sources : site officiel d’Oodle, nouveautés d’Oodle 2.3.0 (dont images), Kraken compressor , Grammatical Ziv-Lempel Compression: Achieving PPM-Class Text Compression Ratios With LZ-Class Decompression Speed, RAD’s ground breaking lossless compression product benchmarked (dont images).
Voir aussi : le blog de Charles Bloom, développeur de Kraken, Mermaid et Selkie.

Compression : zlib obsolète ?

zlib est une bibliothèque de compression très largement utilisée dans bon nombre d’applications : les consoles de jeu les plus récentes (Playstation 3 et 4, Xbox 360 et One, notamment), mais aussi le noyau Linux, les systèmes de gestion des versions comme SVN ou Git ou le format d’image PNG. Sa première version publique a été publiée en 1995 par Jean-Loup Gailly et Mark Adler en implémentant la technique DEFLATE. Son succès est notamment dû à l’absence de brevets logiciels (ce qui a principalement un intérêt aux États-Unis) sur ses algorithmes, mais aussi à des débits en compression et décompression relativement élevés pour une utilisation en ressources assez faible et un bon taux de compression.

Fonctionnement de zlib

Au niveau algorithmique, DEFLATE utilise des techniques éprouvées des années 1990, principalement un dictionnaire (selon l’algorithme LZ77) et un codage de Huffman. Le principe d’un dictionnaire est de trouver des séquences de mots répétées dans le fichier à compresser et de les remplacer par un index dans un dictionnaire. Le codage de Huffman fonctionne avec un arbre pour associer des codes courts à des séquences de bits très fréquentes. Ces deux techniques s’associent pour former la technique de compression standard actuelle.

Concurrents modernes

Cependant, depuis le développement de ces techniques, la recherche au niveau de la compression sans perte a fait de grands progrès. Par exemple, LZMA (l’algorithme derrière 7-Zip et XZ) exploite des idées similaires (plus la probabilité de retrouver des suites de bits dans le fichier à compresser, plus la manière compressée de l’écrire doit être courte), mais avec une dépendance entre différentes séquences de bits (chaîne de Markov), ainsi qu’un codage arithmétique. Le résultat est un taux de compression souvent bien meilleur que DEFLATE, mais le processus de compression est bien plus lent, tout en gardant une décompression rapide et sans besoins extravagants en mémoire. LZHAM est aussi basé sur les mêmes principes avec des améliorations plus modernes et vise principalement une bonne vitesse de décompression (au détriment de la compression).

Cependant, pour un usage plus courant, les débits en compression et décompression sont aussi importants l’un que l’autre, avec un aussi bon taux de compression que possible. Par exemple, pour des pages Web d’un site dynamique, le serveur doit compresser chaque page indépendamment, puisque le contenu varie d’un utilisateur à l’autre. Plusieurs bibliothèques de compression sont en lice, comme LZ4 (qui se propose comme une bibliothèque très généraliste, comme zlib, mais très rapide en compression et décompression), Brotli (proposé par Google pour un usage sur le Web) ou encore BitKnit (proposé par RAD pour la compression de paquets réseau — cette bibliothèque est la seule non libre dans cette courte liste). Ces deux dernières se distinguent par leur âge : elles ont toutes deux été annoncées en janvier 2016, ce qui est très récent.

Une première comparaison concerne la quantité de code de chacune de ces bibliothèques : avec les années, zlib a accumulé pas loin de vingt-cinq mille lignes de code (dont trois mille en assembleur), largement dépassé par Brotli (pas loin de cinquante mille lignes, dont une bonne partie de tables précalculées). Les deux derniers, en comparaison, sont très petits : trois mille lignes pour LZ4 ou deux mille sept cents pour BitKnit (en incluant les commentaires, contrairement aux autres !).

Tentative de comparaison

Rich Geldreich, spécialiste de la compression sans perte et développeur de LZHAM, propose une méthodologie pour comparer ces bibliothèques : au lieu d’utiliser un jeu de données standard mais sans grande variété (comme un extrait de Wikipedia, c’est-à-dire du texte en anglais sous la forme de XML), il propose un corpus de plusieurs milliers de fichiers (ce qui n’a rien de nouveau, Squash procédant de la même manière) et présente les résultats de manière graphique. Cette visualisation donne un autre aperçu des différentes bibliothèques.

Ce graphique montre, sur l’axe horizontal (logarithmique), les débits en décompression (plus un point est à droite, plus la décompression est rapide) et, sur l’axe vertical (logarithmique aussi), le taux de compression (plus il est élevé, plus le fichier a été réduit en taille). Chaque couleur correspond à un algorithme : vert pour zlib, noir pour LZHAM, rouge pour Brotli, bleu pour BitKnit et jaune pour LZ4.

Deux nuages de points sortent du lot : LZ4, tout à droite, est extrêmement rapide en décompression, tout l’opposé de LZHAM, qui propose néanmoins de bien meilleurs taux de compression. zlib montre un comportement assez étrange : le débit de décompression n’augmente plus à partir d’un certain point, contrairement aux autres bibliothèques. L’auteur propose des comparaisons plus spécifiques des taux de compression de chaque bibliothèque en fonction des fichiers.

Et donc ?

Cette comparaison montre que les différentes bibliothèques ne sont pas toujours meilleures les unes que les autres, tout dépend du contenu du fichier, de sa taille, des ressemblances par rapport aux estimations des concepteurs (plus particulièrement dans le cas d’algorithmes qui ne s’adaptent pas dynamiquement au contenu et préfèrent utiliser des tables prédéfinies, ce qui évite de transmettre une série d’informations).

Notamment, Brotli est prévu pour le Web : il fonctionne particulièrement bien sur des données textuelles. Tout comme zlib, il utilise des tables précalculées, ce qui lui donne un avantage sur des fichiers plus petits. Au contraire, BitKnit fonctionne très bien sur du contenu binaire, bien plus courant pour les données de jeux vidéo. Ces deux bibliothèques ont donc chacune leurs points forts selon les domaines d’application prévus et y sont meilleures que zlib.

Sources : zlib in serious danger of becoming obsolete.

Pourquoi l’apprentissage profond et les réseaux neuronaux sont-ils si prometteurs ?

L’apprentissage profond et les réseaux neuronaux sont à la mode pour le moment dans le domaine de l’apprentissage automatique : Google, NVIDIA et plus récemment Microsoft proposent des bibliothèques, plus ou moins ouvertes, pour faciliter leur utilisation.

De fait, l’apprentissage profond accumule les succès ces derniers temps, y compris pour battre des humains au jeu de go — même si le meilleur joueur au monde, selon les classements actuels, Lee Sedol, estime encore pouvoir battre ce système d’intelligence artificielle. L’intérêt du jeu de go est sa complexité, malgré des règles relativement simple : il existe approximativement 10^{761} parties de go, contre « à peine » 10^{120} parties de jeu d’échecs (un nombre bien plus abordable actuellement).

Apprentissage d’un réseau

Cependant, de manière théorique, rien ne pouvait justifier les succès des réseaux neuronaux, qui sont l’outil principal derrière l’apprentissage profond. Depuis la première vague d’intérêt de la part du monde académique, dans les années 1990, leur étude avait montré la présence de nombreux minima locaux de l’erreur totale. L’apprentissage d’un réseau neuronal se fait en définissant la pondération des entrées de chaque neurone : changer un peu ces poids peut avoir un grand impact sur la prédiction du réseau.

Pour choisir cette pondération, tous les algorithmes testent le réseau sur des données pour lesquelles le résultat est connu : par exemple, un son et les mots auxquels il correspond ; la différence correspond à l’erreur commise par le réseau. La présence de ces minima locaux signifie que, une fois l’exécution de l’algorithme terminée, la pondération n’est pas forcément idéale : en changeant quelques valeurs, il peut être possible de diminuer drastiquement l’erreur totale. L’objectif des algorithmes d’apprentissage est d’atteindre le minimum global d’erreur.

Premières analyses et verre de spin

Jusqu’à présent, l’analyse théorique des réseaux neuronaux s’était portée sur des réseaux de quelques neurones : ces minima locaux sont alors présents en grand nombre et sont assez éloignés les uns des autres. Cette caractéristique menace alors la performance des réseaux, puisque le minimum local après apprentissage peut être très éloigné du minimum global.

Ce comportement correspond, en physique, à celui des verres de spin, « des alliages métalliques comportant un petit nombre d’impuretés magnétiques disposées au hasard dans l’alliage » : l’énergie du matériau dépend fortement de la configuration des impuretés, qui présente un grand nombre de minima locaux éloignés du minimum globale. Ce verre de spin est alors coincé dans une configuration dite métastable : en réorganisant très légèrement les impuretés, l’énergie globale pourrait baisser assez fortement.

Nouvelles analyses

Le seul résultat théorique dont on disposait jusque l’année dernière était que certains réseaux neuronaux correspondent exactement aux verres de spin. Cependant, le résultat obtenu par l’équipe de Yann LeCun (directeur du laboratoire d’intelligence artificielle de Facebook) montre, au contraire, que, pour un très grand nombre de neurones, la fonction d’erreur a plutôt la forme d’un entonnoir : les minima locaux sont très rapprochés du minimum global. Plus le réseau est grand, plus ces points sont rassemblés autour du minimum global. Or, justement, l’apprentissage profond propose d’utiliser un très grand nombre de ces neurones, plusieurs millions : le résultat d’un apprentissage n’est donc jamais loin du minimum global.

Plus précisément, les algorithmes d’apprentissage convergent vers des points critiques. Les chercheurs ont montré que la majorité de ces points critiques sont en réalité des points de selle et non des minima : ils correspondent à une zone plate, avec des directions montantes et descendantes. Il est donc relativement facile de s’en échapper, en suivant la direction descendante (en termes d’erreur). Globalement, les vrais minima (qui correspondent à des cuvettes : seulement des directions qui augmentent l’erreur) sont assez rares — et proches de la meilleure valeur possible.

Physiquement, les réseaux neuronaux correspondent donc plus à des « entonnoirs de spin », avec des formes plus sympathiques : l’énergie de la configuration varie de manière abrupte, sans véritablement offrir de minimum local. Ces matériaux trouvent bien plus facilement leur configuration native (avec une énergie minimale).

Ces résultats confirment donc que des techniques comme la descente de gradient stochastique (SGD) peuvent fonctionner : la fonction d’erreur d’un réseau neuronal est à peu près convexe. Cependant, les réseaux modernes sont souvent plus complexes que ceux étudiés, afin d’éviter le surapprentissage (correspondre trop bien aux données pour l’apprentissage, mais avoir du mal à reconnaître des données qui n’en font pas partie).

Néanmoins, la chimie théorique et la physique de la matière condensée proposent d’ores et déjà un panel d’outils mathématiques pour comprendre la structure de ces entonnoirs de spin et des variations plus complexes, notamment dans le cas du pliage de protéines (elles prennent une forme qui minimise cette énergie). Cette étude propose ainsi de nouveaux mécanismes d’étude des réseaux neuronaux, mais peut-être aussi de nouveaux algorithmes d’apprentissage ou techniques pour éviter le surapprentissage.

Sources : C’est la fin d’une croyance sur les réseaux de neurones, Why does Deep Learning work? (image).
Plus de détails : The Loss Surfaces of Multilayer Networks, Why does Deep Learning work?, The Renormalization Group.

Un algorithme quasipolynomial pour l’isomorphisme de graphes

La théorie de la complexité, en informatique, classifie les problèmes selon leur difficulté intrinsèque, c’est-à-dire selon la complexité en temps de l’algorithme le plus efficace pour les résoudre. Par exemple, pour trier un tableau, il existe une multitude d’algorithmes : le tri par insertion, le tri par fusion, le tri par tas ou encore, le plus célèbre, le tri rapide. Les plus efficaces ont une complexité pseudolinéaire : pour trier n éléments, il leur faudra Thetaleft( n log n right ) opérations ; d’autres algorithmes, comme le tri par insertion, ont une complexité quadratique : le nombre d’opérations évolue comme mathcal{O}left( n^2 right ). Les premiers algorithmes pourront trier des tableaux beaucoup plus grands que les seconds, peu importe le langage de programmation utilisé ou la minutie d’implémentation.

Classes de complexité

En réalité, la théorie de la complexité distingue deux catégories principales de problèmes : ceux qui acceptent une solution en un temps polynomial (des problèmes “faciles”), comme le tri, la recherche de plus court chemin, la multiplication matricielle (ils forment l’ensemble mathcal{P}), puis ceux pour lesquels aucun algorithme polynomial n’est connu, comme le voyageur de commerce ou l’analyse de formules en logique (mathcal{NP}). Une contrainte supplémentaire pour être dans mathcal{NP} est qu’il soit possible de vérifier si une réponse est acceptable en un temps polynomial : pour le voyageur de commerce, il suffit de vérifier que toutes les villes sont visitées. Par contre, pour trouver la solution optimale, il n’y a pas de technique qui soit vraiment meilleure que d’explorer toutes les possibilités (du moins, d’un point de vue théorique : il reste possible de résoudre de grandes instances en des temps raisonnables).

En informatique théorique, un problème récurrent est de savoir si mathcal{P}=mathcal{NP}. Aucune preuve n’a pu être avancée jusqu’à ce jour, malgré des dizaines d’années d’essais. Si cette égalité était vérifiée, il deviendrait possible de résoudre tous ces problèmes “difficiles” en un temps polynomial — ce qui pourrait changer la face du monde. Rares sont ceux, cependant, qui croient que ces deux classes coïncident : si tel était le cas, on aurait déjà trouvé un algorithme polynomial pour ces problèmes.

Isomorphisme de graphe

Il existe également des problèmes dont on ne sait pas encore s’ils sont dans mathcal{P} ou mathcal{NP}, comme l’isomorphisme de graphes. Il s’agit de déterminer si deux graphes ont la même structure (ils sont alors dits isomorphes), c’est-à-dire si leurs points peuvent correspondre entre eux tout en gardant les liens entre ces points. (Par exemple, les relations d'”amitié” dans un réseau social comme Facebook peuvent être représentées avec des points pour les individus et des liens pour ceux qui se sont déclarés “amis”.)

Les applications de ces isomorphismes sont nombreuses, telle la reconnaissance de l’unicité d’un visiteur sur un site Web de par son comportement ou l’identification de régions pour implanter des infrastructures lors d’une réflexion urbanistique. Un bon nombre de ces applications est cependant de haut vol, comme pour l’optimisation du code dans un compilateur ou, en informatique théorique, la vérification de programmes, notamment dans des contextes parallèles, ou encore l’égalité des langages reconnus par des automates.

L’avancée de László Babai

Récemment, László Babai a prouvé qu’il existait un algorithme de complexité quasipolynomiale pour résoudre ce problème d’isomorphisme, c’est-à-dire qu’il nécessite un nombre d’opérations mathcal{O}left( exp left( log^c n right ) right ) (le cas où c=1 étant polynomial), par rapport à mathcal{O}left( exp sqrt{n log n} right ) précédemment. Même si l’avancée semble faible, ce résultat montre que l’isomorphisme a une classe de complexité inférieure à mathcal{NP} (mais n’est pas forcément dans mathcal{P}).

Toutefois, cet algorithme et les détails de la preuve ne sont pas très accessibles, exploitant la théorie des groupes et les automorphismes de mots. De plus, ce résultat n’aura pas beaucoup d’implications pratiques à court terme : ceux qui en ont besoin peuvent d’ores et déjà résoudre des isomorphismes suffisamment rapidement pour leurs besoins. Certes, ce nouvel algorithme a des garanties théoriques, mais il n’a pas encore fait ses preuves en pratique pour les cas les plus courants.

Et alors ?

László Babai a reçu le prix Knuth cette année, décerné par l’ACM, pour ses “contributions fondamentales dans les domaines de la conception d’algorithmes et d’analyse de la complexité”. Le résultat obtenu pour les isomorphismes de graphes est important pour plusieurs raisons, principalement théoriques. Notamment, le lien entre propriétés des groupes et des graphes (les principes sous-jacents pourraient mener rapidement à d’autres résultats du même genre en théorie de la complexité, peut-être même pour donner un algorithme polynomial pour les isomorphismes de graphes). Il faut aussi remarquer que la preuve n’a pas encore été publiée dans une revue avec comité de relecture, mais sur arXiv.

Ce résultat a donc principalement des vertus théoriques. Il pourrait aussi, en pratique, éliminer les parties aléatoires des heuristiques utilisées pour résoudre ces isomorphismes pour n’utiliser que des algorithmes plus classiques dans leur manière de fonctionner ; l’avantage serait alors une bien meilleure prédictibilité des résultats. Il pourrait aussi questionner les pratiques actuelles en cryptographie, en abaissant la classe de complexité du problème de factorisation des nombres entiers.

Voir aussi l’article de László Babai.

Sources : Comparaison de graphes, what are the applications of the isomorphic graphs?, A Big Result On Graph Isomorphism.