A quoi sert LEIA ? Quel rapport entre la preuve formelle et l’intelligence artificielle ? En très résumé : la recherche d’éléments de lemmes permettant d’accélérer la preuve…

Contexte¶

LEIA signifie Learning-Enhanced Incremental Analyses. Il s’agit d’un projet de recherche réalisé avec le CEA dans le but d’améliorer les outils d’analyses formelles de code. Un des buts du projet est de créer une heuristique supplémentaire dans S3 basée sur l’intelligence artificielle pour aider les solveurs à prouver plus vite.

Objectif¶

La figure suivante présente un aperçu du processus utilisé pour accélérer le solveur. Les éléments de cette figure sont présentés plus en détails dans la partie Modèle.

L’idée principale est de réussir à guider le solveur en lui “proposant” les pistes les plus prometteuses pour la suite.

Deviner les prochaines clauses simplificatrices grâce au Deep Learning

Le but du solveur est de trouver la solution d’un système d’équation booléenne (SAT) ou de montrer qu’il n’y a pas de solution (UNSAT). Sur le schéma, un graphe représente un système d’équations, les losanges bleus et violets représentent les littéraux du système, et les ellipses blanches représentent les clauses formées avec les littéraux.

Pour résoudre ce système d’équations, le solveur fait des essais. Schématiquement, le solveur attribue une valeur à une des variables libres du système et propage sa valeur dans le reste des équations. S’il aboutit à une incohérence (conflict), il peut en déduire que la variable ne peut pas prendre cette valeur.

C’est dans le choix du prochain littéral à tester que réside la vitesse de résolution. Le but de l’intelligence artificielle est d’apprendre de problèmes déjà résolus l’ordre dans lequel il aurait fallu choisir les littéraux. Il peut alors suggérer les prochains choix à réaliser pour accélérer les prochaines résolutions !

L’idée derrière LEIA est que les problèmes industriels que nous traitons ont une structure commune qui pourrait être apprise et reconnue avec l’intelligence artificielle afin d’accélérer la découverte des meilleures clauses et d’accélérer S3.

S3 / CAE ¶

Le CAE est un ensemble d’outils et de méthodes basé sur une modélisation haut niveau d’un système (HLL) dans le but de prouver certaines bonnes propriétés du système. Dans le cadre d’un pilotage automatique de train par exemple, il s’agit de prouver qu’aucune situation nominale ne permet d’atteindre un danger. C’est la base de la méthodologie SxH. Voir par exemple le billet de blog S3 Formal Verification Solution — Instanciated Systems (4/4) qui en traite.

Pour prouver les propriétés, S3 (l’outil de preuve du CAE) se base sur le model checking de type SAT. SAT est un problème NP-complet, signifiant que la preuve d’une propriété du système passe par la recherche exhaustive d’un éventuel contre-exemple. En revanche, la vérification d’un contre-exemple est « facile » (temps polynomial).

Un des algorithmes de résolution est le CDCL (Conflict-driven clause learning), qui progresse dans sa résolution en proposant des valuations amenant à des contradictions (conflict-driven) et dont on peut déduire de nouvelles clauses (clause learning).

Les divers solveurs S3 sont basés sur des heuristiques dont le rôle est de trouver les bonnes clauses le plus rapidement possible. Le but est donc de proposer une nouvelle heuristique pour S3, basée sur l’IA.

Qu’est-ce que l’IA ? (rapidement)¶

Cette section n’a pas pour but de fournir une liste exhaustive des algorithmes d’Intelligence Artificielle mais plutôt quelques repères et mots-clefs.

Intelligence artificelle est un terme générique parfois réduit au Machine Learning mais qui englobe les méthodes qui permettent à une machine de résoudre des problèmes.

Une des propriétés fondamentales de ces méthodes est que leur fonctionnement est rarement valide à 100% (faux positifs, faux négatifs). Ils ne peuvent trouver la meilleure réponse dans tous les cas des problèmes qu’ils essaient de synthétiser.

Machine Learning¶

Le Machine Learning est une famille de méthodes et d’algorithmes qui apprennent par l’analyse de données. Un exemple simple est la régression linéaire. Cela inclut également les méthodes d’apprentissage par réseaux de neurones (Deep Learning ou non).

Le but est que la machine puisse apprendre à partir de données puis soit capable de généraliser, c’est-à-dire répondre correctement à une question proche de l’entrainement, mais dont la réponse est pour l’instant inconnue.

La réponse attendue peut être une classification (identifier des familles d’objets comme « reconnaître un passage piéton sur une photo »), ou une grandeur continue (par exemple, la probabilité de réussite d’une variable aléatoire).

On distingue les grandes familles de machine learning suivantes (détaillées après) :

supervised learning : on entraîne le modèle avec des entrées connues (on sait répondre à la question directement à partir des données),
reinforcement learning : on entraîne avec un objectif à minimiser (les données ne permettent pas de savoir répondre à la question directement, car par exemple la réponse dépend de l’état courant),
unsupervised learning : on entraîne avec des données sans donner les réponses.

Supervised Learning¶

Voir aussi l’article Wikipedia : Supervised Learning.

Dans cette famille, on trouve :

les régressions : linéaires, normales, logistiques, …
les réseaux bayésiens dont le but est de donner la probabilité d’un événement sachant partiellement ou complètement l’état,
les arbres de décisions (decision tree) ; leur but est d’apprendre automatiquement comment classifier les entrées ; un algorithme connu est le random forest qui crée de multiples arbres de décisions pour les mêmes entrées (avec des variations aléatoires), afin de produire un résultat donnant une probabilité pour chaque catégorie en sortie, ce qui lui permet de généraliser plus efficacement,
les réseaux de neurones.

Les réseaux de neurones sont au coeur du projet LEIA. Ils sont composés par couches. Chaque neurone d’une couche est relié aux neurones de la couche suivante. On trouve la couche des neurones d’entrée que l’on utilise pour stimuler le réseau et la couche des neurones de sorties qui répondent à la question posée.

Un exemple est la reconnaissance de chiffres écrits à la main sur une image. L’entrée est formée des pixels de l’image en niveaux de gris, les sorties sont l’avis du réseau pour chacun des 10 chiffres.

Leur fonctionnement est opaque : une fois entraînés, on ne sait pas comment ils obtiennent une bonne réponse.

Ils peuvent être composés de couches intermédiaires cachées (hidden layers). On parle alors de deep learning. Des sites comme celui-ci proposé par TensorFlow peuvent permettre de mieux visualiser les choses en jouant avec la configuration de petits réseaux de neurones.

La variété des algorithmes des réseaux de neurones et des résultats d’apprentissages en font un sujet très vaste. Souvent, l’architecture des réseaux de neurones est adaptée au problème à résoudre. Par exemple :

les réseaux convolutifs (Convolutional Neural Network) sont bien adaptés à la reconnaissance d’image parce que la convolution est un outil pertinent pour détecter les éléments structurants de l’image (features) comme les bords, les droites ou les courbes, les textures, …,
les réseaux récurrents (Recurrent Neural Network) ou les Long Short-Term Memory networks le sont à la reconnaissance de la parole par leur aptitude à lier une information à son contexte,
les transformeurs introduisent un mécanisme d’attention (BERT/CammeBERT/FlauBERT, GPT-1/2/3, …) qui est très efficace dans les tâches d’analyse de texte comme le fait de prédire la prochaine phrase d’un texte donné (ce qui permet par exemple d’écrire un texte « à la manière de »),
les Generative Adversarial Network (GANs) utilisent deux modèles : un modèle génératif (dont le but est par exemple de générer des visages humains), et un modèle discriminant dit « adversaire » qui doit apprendre à différencier les vraies images (venant d’un corpus d’apprentissage) des fausses images (provenant du modèle génératif) ; les deux modèles sont en compétition permanente et deviennent experts dans la génération et la discrimination ; voir par exemple la génération de fausses photos de visages, application d’un style de peinture sur des photos existantes,
la Stable Diffusion qui combine un modèle texte et un modèle image pour proposer une image qui correspond au texte (testable ici),
…

La recherche sur ces sujets évolue en permanence et remet parfois en question des éléments jusque-là sûr. Par exemple sur la taille minimale ou maximale des réseaux.

Reinforcement Learning ¶

Dans cette famille, on trouve les algorithmes qui permettent de minimiser ou maximiser une fonction objectif après application de plusieurs décisions. Il est nécessaire d’avoir un modèle d’environnement, qui permet de calculer cette fonction objectif. Ces méthodes sont particulièrement efficaces lorsque l’état courant ne permet pas de décider si la réponse fournie est bonne ou non.

Des exemples d’algorithmes sont :

les algorithmes génétiques : chaque élément d’une population est évalué face à l’environnement, puis les meilleurs sont favorablement sélectionnés pour être parents, menant à une population qui optimise son score face à l’environnement,
l’algorithme de colonies de fourmis : favorise les parcours menant plus directement aux objectifs,
le Q-learning : suite à des essais successifs, créée une matrice de décision qui a un état du système associe la décision à prendre, les décisions favorables ayant menées à un score plus grand, la matrice finit par contenir la décision optimale quelle que soit la situation.

Note : il existe également le Deep Reinfrocement Learning, combinant le DL et le RL comme son nom l’indique. Ces algorithmes peuvent montrer de bons résultats sur la planification de décisions complexes (comme pour le jeu de go avec AlphaZero capable de battre les meilleurs joueurs humains et artificiels).

LEIA et CDCL¶

La question est comment réaliser l’apprentissage pour aider le CDCL ? Nous avons été accompagnés par Jolibrain qui a réalisé la majorité des études et essais sur la partie apprentissage.

Choix du modèle¶

Le choix du modèle pour représenter une équation booléenne est influencé d’une part par la manière dont les solveurs se représentent ces équations, et d’autre part par ce qu’on suppose pouvant permettre un bon apprentissage.

Dans une équation booléenne, l’ordre ou le nom des variables booléennes n’a pas d’influence sur le résultat de l’équation, et il n’y a rien qui différencie les variables les unes des autres (elles sont toutes booléennes). Ce sont les connexions entre variables (opérateurs logiques « et » et « ou », opérateurs « non ») — données locales — qui vont avoir une influence sur l’ensemble de l’équation — donnée globale. Ceci ressemble (de très loin) à de l’analyse d’image.

Un outil qui fonctionne bien pour la reconnaissance d’image en IA est la convolution. La convolution est l’extraction de caractéristiques localisées (par exemple, la détection de bord par analyse du contraste, c’est-à-dire la différence entre deux valeurs de pixels voisins). En appliquant plusieurs convolutions successives (de l’ordre de la dizaine) et parallèles (de l’ordre de la centaine), on obtient un Deep Neural Network capable d’extraire des informations pertinentes d’image (features), pour, par exemple, réaliser de la détection d’objet dans des images. A ce sujet, voir AlexNet, SqueezeNet, ou plus généralement les résultats publics sur la database ImageNet.

De l’autre côté, la représentation des équations booléennes de nos solveurs est la CNF (« et » de clauses, une clause étant une disjonction de littéraux, c’est-à-dire un « ou » de variable ou négation d’une variable). La CNF est facile à représenter en graphe non orienté : des nœuds pour les littéraux et d’autres nœuds pour les clauses. Les arcs entre une clause et un littéral stipulent que le littéral apparaît dans la clause. L’équation est représentée par l’ensemble des clauses : elles doivent toutes être satisfaites. Note : ce graphe est bipartite, puisqu’il n’existe de liens qu’entre littéraux et clauses (il n’y a pas de liens entre littéraux, ni de liens entre clauses).

Il existe des algorithmes de Deep Learning utilisant la convolution, mais appliqués aux graphes. On parle de Graph Convolutional Network (GCN). La convolution appliquée au graphe est le « message passing » : chaque nœud extrait des informations de ses voisins (un message). De proche en proches, le message peut circuler dans le graphe, d’une étape par convolution. L’image suivante illustre le processus de voisins de proches en proches. Un message vert met 3 convolutions à atteindre les nœuds rouges.

Parmi les essais réalisés, nous avons utilisé les Graph Attention Network (GAT) (convolutions avec un mécanisme d’attention pour identifier le bon nœud à chaque convolution), et les GasSAT basés sur les GNN AutoScale (GAS) pour répondre à la problématique de passage à l’échelle (consommation mémoire liée au nombre de couches de convolutions).

Note : plus de détails sont disponibles dans le wiki du gitlab interne dédié à LEIA.

Étapes de l’apprentissage¶

Afin de mieux comprendre la variété des essais et les différents problèmes rencontrés, voici un aperçu du processus d’apprentissage :

Aperçu des grandes étapes de l’apprentissage

Les grandes étapes de l’apprentissage sont :

construction des graphes à partir des CNF (on obtient une matrice dont l’ordre de grandeur est le million de lignes et la dizaine de colonnes),
passe d’évaluation du graphe (classiquement appelée « forward ») : le calcul « traverse » chaque couche du modèle pour obtenir la prédiction du modèle pour ce graphe,
calcul de l’écart entre la prédiction et l’attendu (ce qu’aurait dû donner le modèle pour ce graphe s’il connaissait la réponse), c’est la « loss »,
calcul des gradients à chaque étape du calcul forward à partir de la loss ; ces gradients donnent la direction dans laquelle doivent évoluer les paramètres du modèle pour réduire la loss,
modification des paramètres du modèle pour effectivement réduire la loss, c’est l’apprentissage.

Toutes ces étapes sont implémentées dans la bibliothèque de machine learning qu’on utilise. L’étape de calcul des gradients est réalisée par une bibliothèque de programmation différentielle (autodiff/autograd) sur laquelle sont basés les autres modules. Ils automatisent le processus de rétropropagation du gradient (backpropagation).

Problèmes rencontrés¶

Les problèmes rencontrés sont de deux ordres. Le premier est la complexité du problème à résoudre : le SAT étant NP-complet, l’apprentissage a peu de chance de réussir à généraliser la résolution de l’ensemble des problèmes SAT. Cependant, l’attendu de l’apprentissage est de pouvoir reconnaître des problèmes appartenant à une même classe et proposer leur résolution plus rapidement. Cette généralisation fonctionne, mais pas suffisamment : sur des problèmes qui se ressemblent fortement (type sudoku) on obtient des accélérations, sur d’autres problèmes industriels, les résultats ne sont pas probants.

Cette difficulté nous impose de générer des cas d’apprentissage réalistes et suffisamment diversifiés pour couvrir les problèmes que l’on veut pouvoir résoudre au plus vite. Les problèmes types « sudoku » qui sont faciles à changer d’échelle ne sont pas les plus pertinents pour réaliser un apprentissage capable de généraliser efficacement sur les problèmes industriels.

Le second problème est lié à la taille des CNF (plus de 10 millions de nœuds). Ce problème n’est pas évident à visualiser.

Pour résumer, chaque matrice représentée dans l’aperçu de l’apprentissage doit être gardée en mémoire jusqu’à la fin de l’étape de backward. Pour un graphe de 30M de nœuds, on estime que chaque matrice intermédiaire occupe en mémoire 1 Go. 30M de nœuds représente nos plus gros exemples (sur le ZC, une CNF avec 19M de clauses sur 3.6M de variables). Les graphes ont 60M d’arcs. Il y a deux de ces matrices intermédiaires par couche de convolution (une pour le sens forward, une pour stocker les gradients résultats de l’autograd et permettre le backward). Pour 20 couches de convolutions, on atteint environ 80 Go de mémoire (rentre en mémoire centrale de la machine leia qui a 256 Go de RAM mais pas sur une carte graphique en un seul morceau). Pour ces problèmes, 20 couches ne suffisent pas.

Conclusions et perspectives¶

L’apprentissage a montré sur des résultats pertinents sur de petits exemples. Cependant, le passage à l’échelle pose problème.

Afin d’aller plus loin dans l’apprentissage et le nombre de couches du modèle, il est possible d’avoir recours à des solutions dont le coût en temps est plus grand, mais l’empreinte mémoire plus faible. Parmi ces solutions, certaines ont déjà été testées, mais non pas permis de conclure quant à la faisabilité de l’apprentissage. On peut citer l’emploi d’historiques locaux (déjà testé, GasSAT), le découpage de la CNF (avec risque de perdre des liens intéressants), et la distribution de l’apprentissage sur plusieurs machines (avec éventuellement de nouveau une découpe du graphe sur lequel apprendre).

Une autre piste prometteuse est de changer le modèle d’apprentissage. Le modèle courant a peu de paramètres (de l’ordre de la dizaine de milliers), là où un modèle d’apprentissage pour les images en compte des millions. On s’aperçoit que le ratio « taille des entrées » rapportée à la taille du modèle d’apprentissage est probablement défavorable pour notre modèle courant : pour les images, 256x256 → 130k arcs, modèle d’apprentissage 1M de paramètres, pour une CNF, 60M arcs pour un modèle de 10k paramètres). Une des possibilités est que le modèle actuel ne puisse pas généraliser faute de mémoire.

Le choix de changer la convolution est secondé par le constat que la majorité des clauses d’un système réaliste comme le ZC font intervenir peu de littéraux (92% des clauses ont 4 littéraux ou moins). Il est possible que la succession des couches de convolution ne permette pas d’extraire les features intéressantes, comme il était espéré au départ.

Parmi les pistes envisagées, on peut citer les Topology Graph Network, spécifiquement conçus pour être sensibles à l’arrangement des nœuds du graphe.