Mois : mai 2025

  • L’IA pour la cybersécurité : entre promesses et limites actuelles

    La Société Informatique de France (SIF) partage sur binaire un cycle d’interviews sur l’impact de l’intelligence artificielle (IA) sur les métiers. Ici sur le domaine de la cybersécurité, grâce à une interview de Ludovic Mé, directeur du programme cybersécurité de l’agence de programme chez Inria. Interview réalisée Erwan Le Merrer, président du conseil scientifique de la SIF, Serge Abiteboul et Pierre Paradinas.

    Bonjour Ludovic, pouvez-vous vous présenter ?

    J’ai consacré toute ma carrière professionnelle à la cybersécurité, depuis ma thèse portant sur la détection d’intrusions. À cette époque, j’utilisais des outils nommé « algorithmes génétiques », que l’on pourrait classer dans le domaine de l’intelligence artificielle aujourd’hui. J’ai soutenu cette thèse en 1994, puis j’ai suivi une carrière classique d’enseignant-chercheur, à Supélec puis à CentraleSupélec. J’ai encadré mes premiers doctorants, obtenu une habilitation à diriger des recherches, puis été nommé professeur. J’ai ensuite créé une équipe qui a d’abord été une équipe propre à CentraleSupélec, puis une équipe d’accueil (EA 4034) et, enfin, une équipe Inria à partir de 2011. En 2015, tout en restant à CentraleSupélec, je suis devenu délégué scientifique du centre Inria à Rennes. Enfin, à partir de 2019, je suis devenu adjoint de Jean-Frédéric Gerbeau à la direction scientifique d’Inria, fonction que j’ai occupée jusqu’en mars 2025, date à laquelle j’ai été nommé directeur du programme cybersécurité de l’agence de programme du numérique.

    Qui/qu’est-ce qui sera impacté par l’IA dans la cybersécurité ?

    La cybersécurité se compose de divers sous-domaines, assez disjoints les uns des autres du point de vue de leurs objectifs et des outils qu’ils emploient. Citons par exemple la cryptographie, la sécurité des systèmes d’exploitation, la sécurité des réseaux, la supervision de la sécurité. L’impact de l’intelligence artificielle (IA), ou plus précisément de l’apprentissage automatique, varie considérablement selon les sous-domaines.

    Par exemple, en cryptographie, l’impact est, me semble-t-il, quasi-inexistant. En effet, il est peu probable qu’un nouveau mécanisme cryptographique soit développé grâce à l’apprentissage automatique. La mise au point d’un tel mécanisme nécessite un travail d’identification de problèmes mathématiques complexes et de conception d’algorithmes de chiffrement basées sur ces problèmes. Il faut également dimensionner correctement les constantes qui entrent en jeu, comme bien évidemment la taille des clés, afin de garantir une marge de sécurité suffisante, compte tenu de la puissance de calcul nécessaire pour « casser » ces algorithmes de chiffrement. Il y a donc peu de place pour l’apprentissage automatique dans ce domaine, et je doute qu’il y en ait à court terme. De même, le « cassage » d’un algorithme (ce qu’on appelle la cryptanalyse) repose sur des méthodes spécifiques qui, à ma connaissance, ne peuvent être remplacées par l’apprentissage automatique.

    À l’inverse, le domaine de la supervision de la sécurité (détection des attaques en cours sur un système informatique) est assez fortement impacté. Dans le monde industriel, jusqu’à aujourd’hui, les techniques principales de détection d’intrusions sont dites à base de signatures. Il s’agit de spécifier les symptômes des attaques, puis de rechercher des traces de ces symptômes dans les données à analyser, qui peuvent être des journaux système, des journaux applicatifs ou du trafic réseau. Ce dernier type de données est généralement utilisé, car il a un impact minimal sur les systèmes. Ainsi, si certains symptômes sont observés, par exemple dans les en-têtes des paquets réseau, des alertes sont déclenchées et envoyées à des experts pour analyse. En particulier, l’objectif de ces experts est d’éliminer les fausses alertes, qui sont très nombreuses. Dans cette démarche globale de « supervision de la sécurité », plusieurs opportunités s’ouvrent pour l’apprentissage automatique, tant pour la production d’alertes que pour le tri de ces alertes.

    Premièrement, en ce qui concerne la production, au lieu de se baser sur l’identification de symptômes d’attaque (notons que l’intelligence artificielle dite « symbolique » pourrait le faire), il est possible de raisonner par la négation. Il s’agit alors de définir ce qu’est la normalité du fonctionnement d’un système et d’identifier ensuite les déviations par rapport à cette normalité. C’est ce que l’on appelle la détection d’anomalies, technique connue depuis longtemps. Pour effectuer une détection d’anomalies, des statistiques étaient classiquement utilisées. Aujourd’hui, au lieu de se baser uniquement sur des mathématiques, on utilise plutôt l’apprentissage : on apprend des modèles correspondant au fonctionnement normal de certains systèmes, puis on détecte les anomalies de fonctionnement.

    Si cette démarche semble naturelle, elle ne fonctionne pas parfaitement. Les résultats obtenus rivalisent certes avec l’état de l’art des systèmes sans IA, mais il n’y a pas de révolution comparable à celle que l’on a pu connaître dans le domaine de la traduction ou de la reconnaissance d’images. L’intérêt des méthodes basées sur l’intelligence artificielle réside peut-être davantage dans le moindre effort qu’elles demandent pour leur mise en œuvre. Cependant, leur principal problème est celui de la « non-transférabilité » des résultats. Cela constitue un défi majeur : le bon fonctionnement en laboratoire ne garantit pas une application immédiate à d’autres cas d’étude, même légèrement différents. Cette difficulté provient du problème récurrent du manque de données de qualité pour l’apprentissage notamment, on dispose souvent de données mal étiquetées ou imparfaites. La communauté scientifique n’a pas encore trouvé de solution convaincante à ce problème, qui est l’objet d’un champ de recherche actif.

    Malgré les annonces commerciales, il est en fait assez difficile de connaître précisément les mécanismes d’IA concrètement mis en œuvre dans les outils industriels de détection d’intrusions. Une migration vers l’apprentissage est certainement en cours, mais il est peu probable selon moi qu’elle améliore significativement la qualité de la détection par rapport aux méthodes actuelles, au moins dans un premier temps.

    Deuxièmement, la production d’alertes nécessite comme mentionné précédemment un tri ultérieur de ces alertes, en particulier en raison du grand nombre de fausses alertes généralement produites. Dans le secteur industriel, ce tri est effectué dans des centres d’opérations de sécurité (SOC). Les techniques traditionnelles employées incluent le regroupement des alertes correspondant à un même phénomène et la détection des données aberrantes. Ici, l’apprentissage automatique peut bien sûr apporter des solutions pertinentes.

    Plus généralement, en dehors du domaine de la détection, des chercheurs ont récemment configuré des routeurs réseau avec des grands modèles de langage (LLM) [routeurs], contournant ainsi la complexité de la configuration manuelle. Cette piste pourrait être explorée pour la configuration de la sécurité réseau ou des mécanismes de contrôle d’accès aux données contenues par les systèmes informatiques. On peut même envisager de dépasser l’héritage des années 70, avec une configuration par IA de droits d’accès afin d’implémenter des politiques de sécurité complexes et difficiles à mettre en œuvre aujourd’hui. Je ne développerai pas plus ici, mais l’IA pourrait ainsi contribuer à relancer des travaux sur la sécurité des systèmes d’information, sujet fondamental de la cybersécurité qui donne malheureusement lieu à très peu de recherche, en tous cas en France.

    Tout ce qui précède traite de l’impact de l’IA au service de la cybersécurité. Mais l’IA va aussi avoir un impact contre la cybersécurité. En effet, les mécanismes de l’IA, et en particulier les LLM (Large Language Models), sont en capacité de générer du code et donc potentiellement du code malveillant (virus, exploitation de vulnérabilités, etc.). Ils sont aussi en mesure de rendre beaucoup plus réalistes les mails d’hameçonnage, ce qui pourrait conduire à piéger davantage d’utilisateurs. Ces effets délétères de l’IA sont encore peu observés (ou en tous cas on manque de chiffres), mais ils sont redoutés et il convient de s’y préparer, au cas où ils se concrétiseraient.

    Pour terminer, on voit aussi une inquiétude marquée relative à la génération par LLM de fake news. Pour ma part, je considère que ce sujet, évidemment d’une extrême importance, ne relève pas du domaine de la cybersécurité. Pour dire les choses rapidement, tout mensonge ou toute arnaque véhiculée ou utilisant l’informatique (et qu’est-ce qui n’utilise pas l’informatique aujourd’hui ?) ne relève pas nécessairement de la cybersécurité.

    À quel changement peut-on s’attendre dans le futur ? Par exemple, quelle tâche pourrait être amenée à s’automatiser, et à quels horizons ?

    Comme mentionné précédemment, la supervision de sécurité sera probablement impactée par la détection d’anomalie à base d’IA, bien que des efforts restent à fournir. Il est difficile de le prédire avec précision, mais il est probable qu’un impact notable au-delà de la simple démonstration ne se produise que dans quelques années. Nous l’avons déjà abordé, l’enjeu principal réside dans la qualité des données d’apprentissage. Sans données de qualité et partageables, aucun progrès significatif ne sera possible. Des données de qualité permettront de construire des modèles de qualité, qui devront ensuite être adaptés aux cas particuliers.

    Quelles connaissances en intelligence artificielle sont nécessaires pour les postes en cybersécurité ?

    La sécurité combine R&D et actions opérationnelles. Les équipes opérationnelles n’ont pas nécessairement besoin de connaître le type de modèle précis à choisir ni la manière dont il est entraîné. Prenons à nouveau l’exemple de la supervision de la sécurité. Les équipes opérationnelles des SOC voient arriver des alertes et doivent être en mesure de les qualifier : fausse alerte ou alerte réelle. Pour ce travail, pas vraiment besoin d’une formation en IA radicalement différente de celle déjà au programme des formations aujourd’hui.

    En revanche, en R&D, des connaissances en IA sont effectivement nécessaires. En effet, les développeurs en charge du développement des sondes de détection devront choisir des modèles, disposer d’une méthodologie solide pour l’apprentissage, ainsi que pour l’évaluation de la qualité de cet apprentissage. Une compétence solide en apprentissage automatique sera donc ici requise.

    Il est également important de rappeler que les mécanismes d’apprentissage automatique sont eux-mêmes vulnérables. Il existe donc un besoin important de formation concernant les attaques spécifiques contre l’apprentissage automatique, afin d’assurer sa protection.

    Que faudrait-il privilégier pour le domaine : des informaticiens à qui apprendre le métier ou des spécialistes du métier également compétents en IA ?

    Je pense que nous avons besoin de spécialistes de l’IA qui s’intéressent à la sécurité, tant en termes d’utilisation de l’IA au service de la sécurité, qu’en termes d’utilisation de l’IA contre la sécurité, avec des attaques générées par IA. Il ne s’agit pas seulement de contribution à des attaques simples comme l’hameçonnage, mais aussi de génération de stratégies d’attaques sophistiquées ou de découvertes dans des logiciels de nouvelles vulnérabilités pouvant être exploitées pour réaliser des attaques, c’est à dire l’utilisation du cyberespace dans le but de perturber, de désactiver, de détruire ou de contrôler de manière malveillante un environnementou une infrastructure informatique, ou de détruire l’intégrité des données ou de voler des informations non publiques.

    Les spécialistes en IA devraient être en mesure de guider les spécialistes de la sécurité, qui ne savent généralement pas quel modèle sélectionner pour quel avantage, ni à quel point telle ou telle tâche est complexe. Malheureusement, il semble que les spécialistes de l’IA, pour le moment, délaissent la sécurité de l’IA et la sécurité par l’IA, au profit de thèmes qu’ils jugent plus intéressants. J’en arrive donc à la conclusion qu’il faudra que les spécialistes en sécurité s’y attellent eux-mêmes. Comme auparavant finalement : lorsqu’ils faisaient des statistiques, ils le faisaient eux-mêmes, sans demander l’aide de mathématiciens.

     Quelles formations continues vous paraissent indispensables ?

    Dans la continuité de mon propos, il faut que les acteurs de la R&D dans certains sous-domaines de la sécurité s’intéressent à l’usage de l’IA. Il est nécessaire que ces acteurs aient une bonne compréhension des différents mécanismes de l’IA. J’insiste aussi sur la formation spécifique sur les attaques contre l’apprentissage automatique. Je pense qu’il ne suffit pas d’étudier l’apprentissage automatique en soi, il faut aussi comprendre comment il peut être contourné.

    Inversement, certains articles scientifiques (« Real Attackers Don’t Compute Gradients » [real]) expliquent clairement que les attaquants privilégient toujours les attaques les plus simples, comme l’hameçonnage. Il faut donc du discernement pour être capable d’évaluer la vraisemblance d’une attaque contre l’IA, et ces formations peuvent y contribuer.

    Quelle demande formuleriez-vous auprès des concepteurs d’intelligence artificielle ?

    L’histoire de l’informatique est jalonnée d’exemples où, lors de la conception d’un système, la cybersécurité est négligée. Cela s’est vérifié pour les systèmes d’exploitation, les réseaux et l’internet en particulier, et c’est le cas aujourd’hui pour l’intelligence artificielle. Or, cette négligence se révèle souvent problématique après un certain temps. Pourquoi ? Parce que réintégrer la sécurité a posteriori est extrêmement complexe, voire impossible.

    Par conséquent, si j’avais un conseil à donner, ce serait d’intégrer la sécurité dès la conception, même si cela peut s’avérer parfois contraignant. Sinon, il faudra peut-être faire machine arrière, voire cela s’avérera tout simplement impossible. Réfléchissons avant d’agir !

     

     Ludovic Mé.

    Références

    [routeurs] Mondal, R., Tang, A., Beckett, R., Millstein, T., & Varghese, G. (2023, November). What do LLMs need to synthesize correct router configurations?. In Proceedings of the 22nd ACM Workshop on Hot Topics in Networks (pp. 189-195).

    [real] Apruzzese, G., Anderson, H. S., Dambra, S., Freeman, D., Pierazzi, F., & Roundy, K. (2023, February). “real attackers don’t compute gradients”: bridging the gap between adversarial ml research and practice. In 2023 IEEE conference on secure and trustworthy machine learning (SaTML) (pp. 339-364). IEEE.

     

  • Faire communiquer un modèle de langage et un assistant de preuve

    On entend beaucoup dire que les LLM ne savent pas raisonner. Pourtant, des modèles de langage semblent capables de raisonner. Comment est-ce possible ? Pour résoudre ce mystère, nous avons demandé à un expert du domaine, Guillaume Baudart, d’expliquer à binaire ce « miracle ». Serge Abiteboul et Pierre Paradinas

    Les grands modèles de langage (LLMs pour Large Language Models) sont des modèles d’intelligence artificielle capables de générer du texte en langage naturel. Entraînés sur d’immenses quantités de données, ces modèles sont au cœur d’applications comme ChatGPT (openAI) ou Le Chat (Mistral). Grâce à des développements récents, ces modèles sont de plus en plus utilisés pour des tâches allant de la génération de code à la résolution de problèmes mathématiques à partir de descriptions en langage naturel. Mais que veut dire raisonner pour ces modèles ? Peut-on se fier aux résultats ?

    D’un autre côté, les assistants de preuve tels que Rocq permettent de valider une preuve mathématique avec un très haut niveau de confiance, mais l’expertise nécessaire pour utiliser ces outils les rend difficiles d’accès.

    Faire communiquer efficacement un LLM et un assistant de preuve permettrait d’atteindre deux objectifs complémentaires. D’abord, l’assistant de preuve peut valider les raisonnements générés par un LLM. Ensuite, les LLMs offrent une interface conversationnelle intuitive qui peut faciliter l’utilisation de ces assistants jusque-là réservés aux experts.

    Deux lois d’échelle pour les LLMs

    On assiste aujourd’hui à une course mondiale pour développer des modèles de plus en plus puissants. Les chiffres donnent le tournis : les modèles les plus récents contiennent des centaines de milliards de paramètres, sont entraînés sur des milliards de textes d’origines diverses, et leur coût d’entraînement est estimé à des dizaines de millions de dollars. Pour donner un exemple récent, le modèle DeepSeek-V3 contient 671 milliards de paramètres et son entraînement a demandé près de 3 millions d’heures GPU (les processeurs graphiques utilisés pour les calculs intensifs). Si ce modèle a fait les gros titres parce que son entraînement a été incroyablement efficace pour sa taille, il aura quand même coûté environ 6 millions de dollars.

    La course aux grands modèles s’explique par une observation simple : les performances augmentent avec la taille des modèles. Plus précisément, lors de l’entraînement, les paramètres (des milliards de nombres qui contrôlent le comportement du modèle) sont ajustés pour optimiser un objectif qu’on appelle la perte. Dans le cas des modèles de langage comme les LLMs, on demande au modèle de compléter un texte connu (partiellement masqué) et la perte mesure la distance entre le texte généré et le texte original. Par exemple, « Le petit chat est mort. » est très proche de « Le petit chat est fort. » mais assez loin de « Le ciel est bleu aujourd’hui. ».

    Or, on a observé dès 2020 une loi d’échelle pour l’entraînement des LLMs : la perte évolue selon une loi de puissance avec la quantité de calcul (nombre de paramètres, tailles de corpus d’entraînement, et temps d’entraînement). Et plus la perte est faible, plus les modèles deviennent performants pour diverses tâches : résumer, extraire de l’information, faire des raisonnements mathématiques, générer du code informatique, etc. Il est par ailleurs possible de spécialiser les LLMs sur une tâche spécifique en complétant leur entraînement sur des données ciblées.

    Beaucoup plus récemment, on a également observé une nouvelle loi d’échelle pour l’inférence : les performances d’un modèle augmentent aussi avec la taille du texte généré lors de son utilisation. Confronté à une question, les modèles récents commencent par générer un long texte appelé chaîne de pensées qui imite un comportement humain. En utilisant le contenu de la chaîne, le modèle peut ensuite synthétiser un résumé.

    Généré par Théo Stoskopf à l’aide de ChatGPT

     

    Voici par exemple un exercice issu d’un jeu de données d’exercices de lycée utilisé pour évaluer les LLMs (traduit en français ici).

    Des tubes de peinture contiennent 8 centilitres d’un mélange de jaune et de bleu. Il y a du bleu et du jaune dans chaque tube. Mon premier tube contient un quart de la quantité totale de jaune et un sixième de la quantité totale de bleu. Combien y a-t-il de tubes ?

    Si certaines applications (comme ChatGPT) masquent les chaînes de pensées, on peut parfois demander au modèle de nous montrer tout le texte généré. Voici par exemple la chaîne de pensées générée par DeepSeek-R1 pour ce problème (attention spoiler, le raisonnement original en anglais a été traduit).

    Ok, essayons de déterminer combien il y a de tubes. Le problème indique que chaque tube contient 8 centilitres d’un mélange de jaune et de bleu. Chaque tube contient les deux couleurs. Le premier tube contient un quart du total de jaune et un sixième du total de bleu. Nous devons trouver le nombre de tubes.

    Hmm, décomposons le problème. Je vais noter la quantité totale de peinture jaune Y et la quantité totale de peinture bleue B. Chaque tube contient une certaine quantité de jaune et de bleu, pour un total de 8 cl. Le premier tube contient 1/4 du total de jaune et 1/6 du total de bleu. Donc, la quantité de jaune dans le premier tube est Y/4, et la quantité de bleu est B/6. Puisque chaque tube contient 8 cl au total, alors Y/4 + B/6 = 8. C’est une équation.

    Maintenant, pensons aux autres tubes. Il y a n tubes au total. Chacun des (n – 1) tubes restants doit également contenir du jaune et du bleu, mais combien ? Comme le problème ne spécifie pas de distribution particulière pour les autres tubes, sauf qu’ils contiennent tous les deux couleurs, peut-être pouvons-nous supposer que le reste de jaune et de bleu est réparti équitablement entre eux ? Attendez, mais le problème ne dit pas cela. Hmm, peut-être avons-nous besoin d’une autre approche.

    Alternativement, puisque le premier tube contient Y/4 de jaune et B/6 de bleu, alors la quantité restante de peinture jaune est Y – Y/4 = (3/4)Y, et la quantité restante de peinture bleue est B – B/6 = (5/6)B.

    […]

    Est-ce possible ? Voyons voir. Par exemple, si nous répartissons le reste de jaune à raison de 3 cl par tube (12/4=3) et le reste de bleu à raison de 5 cl par tube (20/4=5), chaque tube contiendrait 3+5=8 cl, ce qui fonctionne. Donc oui, c’est possible. Toutes les conditions sont satisfaites si n=5. Donc, la réponse est 5 tubes.

    Mais laissez-moi vérifier à nouveau. Si n=5, le volume total est de 40 cl, Y=16, B=24. Premier tube : 4 jaune, 4 bleu. Reste 12 jaune et 20 bleu. 12/4=3, 20/4=5. Chaque tube restant contient 3 jaune et 5 bleu. Cela fait 8 cl chacun, et tous contiennent les deux couleurs. Donc cela fonctionne. Par conséquent, le nombre de tubes est 5.

    On peut voir le modèle essayer plusieurs approches, se corriger, vérifier ses résultats, presque comme un étudiant en train de passer un examen devant un tableau noir. Le texte est ponctué d’expressions comme : « Ok, essayons de déterminer », « peut-être pouvons-nous supposer », « Attendez », « Hmm », « Est-ce possible », « laissez-moi vérifier » qui incitent le modèle à continuer la génération de texte pour progresser dans le raisonnement. Le modèle peut ensuite synthétiser une réponse courte et structurée en résumant cette chaîne de pensées. Les LLMs les plus récents, dits modèles de raisonnement, sont spécialisés lors de l’entraînement pour générer ces chaînes de pensées.

    Cette nouvelle loi d’échelle ne s’arrête pas aux chaînes de pensées. Plutôt que d’investir toute la puissance de calcul au moment de l’entraînement, on utilise maintenant les ressources de calcul pour exploiter au mieux les textes générés. Une technique simple consiste à générer plusieurs chaînes de pensées en parallèle avant de choisir celles qui ont donné les meilleurs résultats. On peut également utiliser des algorithmes de recherche arborescente : à chaque étape de raisonnement, on génère plusieurs solutions, mais on ne fait progresser que les plus prometteuses.

    En combinant toutes ces approches, il est aujourd’hui possible de spécialiser de relativement petits modèles qui atteignent des performances comparables à celles des énormes LLMs les plus connus (GPT-4o, Claude Sonnet, Gemini) pour un budget beaucoup plus modeste.

    Ces nouveaux développements posent une question fondamentale : comment vérifier les raisonnements produits par les LLMs ? Cette question, qui était déjà préoccupante pour les premiers LLMs, devient cruciale pour les modèles de raisonnement pour lesquels une hallucination (une information fausse et inventée) peut complètement fausser la chaîne de pensées.

    On construit donc des agents : des applications capables de coupler les LLMs avec des outils externes pour valider le texte généré (par exemple pour faire des recherches sur le web, ou pour exécuter du code généré par le LLM), et des algorithmes de recherche.

    Généré par Théo Stoskopf à l’aide de ChatGPT. L’oiseau est inspiré du logo de l’assistant Rocq.

     

    Valider les chaînes de pensées avec un assistant de preuve

    Fruit d’un travail à l’intersection de la logique mathématique et la théorie des langages de programmation, les assistants de preuve sont des outils qui permettent à un ordinateur de vérifier un raisonnement mathématique. Une preuve est décomposée en étapes logiques et l’ordinateur vérifie que chaque étape respecte les règles de la logique mathématique. Si une preuve repose sur l’utilisation d’un théorème, l’ordinateur vérifie que toutes les hypothèses sont bien vérifiées et que la conclusion suffit à prouver le résultat attendu

    Les assistants de preuve comme Rocq (anciennement Coq), Lean ou Isabelle sont des outils interactifs. L’utilisateur propose une étape de raisonnement que l’ordinateur vérifie avant d’indiquer à l’utilisateur ce qu’il reste à démontrer. Prenons un exemple très classique :

    Tous les hommes sont mortels. Socrate est un homme. Donc, Socrate est mortel.

    Le but initial est de prouver Socrate est mortel. Pour prouver ce théorème, on peut commencer par spécialiser la première prémisse Tous les hommes sont mortels à l’individu Socrate. L’assistant ajoute alors une nouvelle hypothèse : Si Socrate est un homme alors Socrate est mortel. On applique alors la seconde prémisse Socrate est un homme à cette hypothèse et l’assistant vérifie qu’on obtient bien Socrate est mortel.

    Buste d’origine romaine en marbre de Socrate, Le Louvres

     

    En théorie, ce fonctionnement interactif est parfaitement adapté pour développer un agent capable de vérifier un raisonnement mathématique. Chaque étape de raisonnement est validée par l’assistant de preuve, et les réponses (ou les messages d’erreur) de l’assistant de preuve nourrissent le LLM pour générer les prochaines étapes de raisonnement. Malheureusement, cet exercice de formalisation reste particulièrement difficile pour les humains comme pour les LLMs. Des LLMs récents sont aujourd’hui très performants pour la génération de code, mais l’exercice de preuve formelle ajoute une contrainte fondamentale qui rend l’exercice beaucoup plus compliqué : la preuve n’est terminée que si le code est parfaitement correct. Il n’y a aucune approximation possible. Par ailleurs, le code doit être écrit dans un langage spécialisé dont il existe relativement peu d’exemples au milieu des immenses quantités de données utilisées lors de l’entraînement.

    Pour utiliser au mieux les capacités des LLMs, on peut réutiliser l’idée des chaînes de pensées. Plutôt que d’essayer de générer directement du code, on demande au modèle de décrire le théorème et ses hypothèses en langage naturel (par exemple en anglais ou français) et de suggérer un schéma de preuve, avant de générer le code en résumant la chaîne de pensées.

    Couplé avec des algorithmes de recherche, cette approche commence à donner des résultats impressionnants sur des exercices de niveau lycée ou licence [1-2-3]. En utilisant une technique d’apprentissage « par renforcement » AlphaProof, un modèle entraîné par Google Deepmind sur des millions de théorèmes générés automatiquement, a même réussi à prouver avec l’assistant de preuve Lean des problèmes d’olympiades de mathématiques, atteignant le niveau d’une médaille d’argent.

    Un assistant d’assistant de preuve

    Les assistants de preuve sont donc des outils précieux pour valider les raisonnements générés par les LLMs. En changeant de perspectives, les LLMs peuvent également modifier en profondeur la manière dont nous utilisons des assistants de preuves qui restent aujourd’hui des outils réservés aux experts.

    Si le code final doit être écrit dans un langage de programmation spécialisé, les chaînes de pensées générées lors du raisonnement sont écrites en langage naturel. Un humain peut donc facilement inspecter le raisonnement pour comprendre le code suggéré par l’assistant, voire directement intervenir pour le corriger. Les LLMs permettent ainsi de développer des interfaces conversationnelles :  il devient de plus en plus possible de « discuter » (en français ou en anglais) avec l’assistant de preuve pour formaliser un théorème sans être un expert du langage de programmation spécialisé.

    Les logiciels d’édition de code intègrent déjà ce genre de technologies pour les langages les plus populaires comme Python ou JavaScript. Ces assistants rendent de nombreux services qui vont de l’autocomplétion (compléter un bout de code à partir du contexte et des commentaires) à l’analyse de documentation (par exemple pour retrouver une fonction ou un théorème à partir d’une description floue en langage naturel).

    L’utilisation des LLMs pour les assistants de preuve est un domaine de recherche aujourd’hui très actif. On cherche à développer des agents capables de faciliter de nombreuses tâches qui restent difficiles ou ingrates pour les humains. Par exemple, en utilisant les impressionnantes capacités de traduction des LLMs, on aimerait traduire directement un livre de mathématiques (théorèmes et preuves) dans le langage de l’assistant de preuve. Cette tâche suppose d’être capable de comprendre le contexte, les hypothèses implicites propres à chaque domaine, et la nature des objets mathématiques manipulés. Les LLMs récents entraînés sur de très nombreux textes mathématiques (avec différents niveaux de rigueur) peuvent faire des associations d’idées pour combler les « trous » entre le langage naturel du livre et sa formalisation dans un assistant de preuve. Ce problème reste très difficile, mais une solution partielle générée par un LLM peut être un point de départ précieux pour un humain.

    Enfin, le comportement d’un programme peut aussi être formalisé dans un assistant de preuve. Il est donc possible de prouver qu’un programme est correct. Par exemple, on peut prouver qu’une fonction de tri en Python ou JavaScript renvoie toujours un tableau trié. À plus long terme, on aimerait avoir des assistants capables de traduire une spécification en langage naturel vers un code exécutable, une formalisation de la spécification, et une preuve de correction qui montre que le code correspond bien à sa spécification. Les assistants de preuve aidés par des LLMs permettraient ainsi de garantir que le code généré par un LLM est bien correct ! C’est un enjeu crucial dans un monde où le code informatique des applications que nous utilisons tous les jours devient de plus en plus généré automatiquement par ces modèles.

    Conclusion

    Faire communiquer LLMs et assistants de preuve ouvre des perspectives prometteuses pour l’avenir de l’intelligence artificielle et de la vérification formelle. En combinant la capacité des LLMs à générer des raisonnements complexes en langage naturel avec la rigueur des assistants de preuve, il devient possible de développer des agents capables de vérifier des preuves mathématiques. Ces agents pourraient non seulement améliorer la fiabilité des résultats produits par les LLMs et les capacités de raisonnement des futures générations de modèles, mais aussi rendre les outils de preuve formelle aujourd’hui réservés à des experts plus accessibles.

    Guillaume Baudart, Inria

    • [1] https://arxiv.org/abs/2310.04353
    • [2] https://hal.science/hal-04886208v1 
    • [3] https://arxiv.org/abs/2408.08152

     

    Note : Merci à Vincent Baudart, Paul-André Melliès, Marc Lelarge, Théo Stoskopf, Jules Viennot, et Sarah Winter pour leurs relectures et leurs suggestions.

     

  • Prendre des décisions optimales sans avoir toutes les cartes en main, 2/2 : la science des révélations

    L’article « Revelations: A Decidable Class of POMDP with Omega-Regular Objectives » a été primé par le « Outstanding Paper Award » à la conférence AAAI 2025, la plus prestigieuse conférence internationale en intelligence artificielle (https://aaai.org/). Cette récompense couronne le fruit d’un travail de recherche initié à Bordeaux, au sein de l’équipe Synthèse (https://synth.labri.fr/) du Laboratoire Bordelais de Recherche en Informatique (LaBRI), où travaillent quatre des auteurs: Marius Belly, Nathanaël Fijalkow, Hugo Gimbert et Pierre Vandenhove, en coopération avec des chercheurs à Paris (Florian Horn) et Anvers (Guillermo Pérez). Après nous avoir raconté la genèse de ce papier dans un précédent article, ce billet en esquisse les idées principales, tandis que l’article complet est consultable librement à l’adresse https://arxiv.org/abs/2412.12063 . Chloé Mercier et Serge Abiteboul.

    L’équipe Synthèse du LaBRI s’attaque au problème ardu de la synthèse de programme. Il s’agit de développer des algorithmes qui eux-mêmes génèrent d’autres algorithmes, à partir de quelques exemples ou d’une spécification de ce qui est attendu. Concrètement, ces algorithmes très puissants sont utilisés dans une variété de contextes. Par exemple, la plupart des tableurs proposent aujourd’hui des fonctions de remplissage automatique : vous remplissez quelques cellules et, à partir de ces quelques exemples, un petit algorithme est synthétisé à la volée et se charge de finir le travail (https://deepsynth.labri.fr/). Un autre exemple est le contrôle robotique : un opérateur transmet à un robot une tâche à exécuter, par exemple reprendre le contrôle de la balle dans un match de  Robocup, et charge au robot et à ses algorithmes de programmer la bonne suite de mouvements et d’actions à effectuer pour arriver au but escompté. 

    Quand les ingénieurs et chercheurs en Intelligence Artificielle (IA) ont besoin de résoudre des problèmes de synthèse, ils utilisent couramment un formalisme mathématique appelé processus de décision Markoviens, ou pour faire plus court, les MDP. La question centrale est la suivante : dans une situation où il faut prendre une suite de décisions, décrite par un MDP, comment faire pour prendre de bonnes décisions ? Ou, encore mieux, comment faire pour calculer automatiquement la meilleure suite de décisions possibles, ce qui s’appelle également une stratégie optimale ?

    Les MDP pour décider

    Mais qu’est-ce qu’un MDP exactement ? Dans le contexte de cette recherche, c’est un système à états finis dont l’évolution est déterminée à la fois par les décisions (choix d’action), mais également par le hasard. Voilà à quoi ressemble un tel animal :

    Un exemple de MDP
    Ce MDP illustre un exemple issu de l’article. C’est un jeu classique : il y a deux portes, et un tigre se cache derrière l’une des deux. On doit choisir quelle porte ouvrir, mais on ne sait pas où est le tigre. Grâce à l’action “écouter” (“listen” dans l’illustration) on peut révéler où se cache le tigre avec une probabilité positive.
    Crédits: les auteurs.

     

    Dans la vie courante, on peut se servir des MDP à de multiples occasions (nous les avions déjà rencontré dans le cas du Cluedo dans un autre article binaire), par exemple pour jouer au « Solitaire », également appelé « Patience » ou encore « Spider Solitaire » dans sa célèbre variante. La situation ci-dessous illustre le dilemme de la prise de décision dans un MDP : faut-il placer un des deux rois noirs sur la pile vide à gauche ? Si oui, lequel des deux ? Le choix est épineux car certaines cartes sont masquées et ne seront révélées qu’ultérieurement.

    Jeu de Solitaire
    Le jeu de Solitaire. Même quand toutes les cartes sont révélées, le problème est difficile : cf https://web.stanford.edu/~bvr/pubs/solitaire.pdf.
    Crédits: les auteurs.

    Stratégies de résolution des MDP

    Il y a deux grandes catégories d’algorithmes IA pour résoudre un MDP, qui peuvent paraître similaires à première vue mais qui pour les chercheurs en informatique sont bien distinctes. D’une part, il y a les algorithmes qui fonctionnent bien en pratique mais sans garantie de fournir la meilleure solution, ce qui est le cas de la plupart des méthodes d’apprentissage, notamment celles utilisant les réseaux de neurones (DeepRL). D’autre part, il y a les algorithmes qui fournissent à coup sûr une réponse exacte, qui relèvent de l’IA de confiance, basée sur la notion de calculabilité et de problème décidable développé par le génie Alan Turing, pionnier de l’informatique théorique. L’article des chercheurs bordelais appartient à la seconde catégorie : quand l’algorithme proposé produit une stratégie gagnante, on peut utiliser cette stratégie en toute confiance — elle garantit de gagner avec probabilité 1.

    Soyons modestes et réalistes : les techniques d’apprentissage permettent de calculer des stratégies dans des problèmes très complexes alors que les techniques exactes au sens de la théorie de la calculabilité sont pour l’instant circonscrites à des problèmes plus simples, car elles sont en général beaucoup plus gourmandes en ressources de calcul. Par exemple, Google DeepMind a exploité les techniques de DeepRL afin de synthétiser d’excellentes stratégies à StarCraft, un jeu vidéo populaire dans lequel il faut prendre des dizaines de décisions par seconde en fonction de millions de paramètres. L’IA de DeepMind a initialement battu les meilleurs joueurs mondiaux, mais sa stratégie n’était pas parfaite : des contre-stratégies difficilement prévisibles ont ensuite été découvertes.  Les méthodes exactes sont aujourd’hui inexploitables pour résoudre un problème aussi complexe que StarCraft, mais cela ne les empêche pas d’être efficaces en pratique. Par exemple, autre succès bordelais, l’équipe Rhoban du LaBRI a remporté une médaille d’or à la Robocup 2023 en exploitant des méthodes exactes pour résoudre de petits MDP en se basant sur le partage d’informations entre plusieurs robots coopératifs (https://github.com/Rhoban/TeamPlay).

    La difficulté de la résolution exacte de problèmes de décision est très variable en fonction de l’information disponible au moment de la décision. Le cas idéal est celui de l’information parfaite, c’est le cas où toute l’information est disponible. Un exemple classique est celui d’un robot qui doit sortir d’un labyrinthe dont on connaît le plan ainsi que la propre position et orientation exacte du robot. Dans ce cas, le calcul est relativement facile à effectuer : il faut calculer un chemin vers la sortie (par exemple avec l’algorithme de Dijkstra) puis suivre ce chemin avec la suite de commandes de déplacement adéquates. Mais dans les problèmes rencontrés en pratique, il est rare d’avoir toutes les cartes en main. C’est le cas au solitaire, où une partie des cartes est masquée, ce qui nécessite de faire des hypothèses. Dans ce cas, en toute généralité le problème ne peut être résolu de manière exacte, la réponse n’est pas calculable au sens de Turing : aucun algorithme, aussi puissant que soit l’ordinateur sur lequel il est programmé, ne peut résoudre avec exactitude tous les problèmes de contrôle de MDP. C’est assez démoralisant à première vue pour un informaticien mais cela n’arrête pas certains chercheurs en informatique qui s’attellent à trouver des classes de MDP pour lesquelles le problème est moins complexe. En informatique théorique, on appelle cela une classe décidable. 

    Le travail de recherche primé à AAAI fournit justement une classe décidable de MDP : c’est le cas des problèmes avec « révélation forte », pour lesquels à chaque instant il y a une probabilité non-nulle que l’état exact du monde soit révélé. L’article donne aussi des résultats de décidabilité pour le cas des « révélations faibles », qui garantit que l’état exact du monde ne peut rester inconnu infiniment longtemps.

    Un article de recherche se doit d’être tourné vers le futur, d’ouvrir des pistes. Notre algorithme permet d’analyser les jeux avec des révélations (fortes). Une perspective intéressante est de retourner le problème : on peut se demander plus généralement ce que fait l’algorithme lorsqu’il est utilisé pour n’importe quel jeu, avec ou sans révélations. Cela permet d’envisager d’analyser tous les jeux, même les plus compliqués, mais en restreignant plutôt le type de stratégie que les joueurs utilisent, ou la quantité d’informations qu’ils sont capables de traiter.

    Marius Belly, Nathanaël Fijalkow, Hugo Gimbert, Florian Horn, Guillermo A. Pérez et Pierre Vandenhove

  • Prendre des décisions optimales sans avoir toutes les cartes en main, 1/2 : la genèse d’un papier scientifique

    Les chercheurs ont toujours du mal à expliquer comment la recherche progresse dans un cadre international, pluridisciplinaire et collaboratif. Nous allons illustrer cela avec la genèse d’un article scientifique « Revelations: A Decidable Class of POMDP with Omega-Regular Objectives ». Cet article a été primé par le « Outstanding Paper Award » à la conférence AAAI 2025, la plus prestigieuse conférence internationale en intelligence artificielle (https://aaai.org/). Quatre des auteurs, Marius Belly, Nathanaël Fijalkow, Hugo Gimbert et Pierre Vandenhove, sont au laboratoire bordelais de recherche en informatique (LaBRI). Ils ont collaboré avec des chercheurs à Paris (Florian Horn) et Anvers (Guillermo Pérez). L’article est consultable librement à l’adresse https://arxiv.org/abs/2412.12063. Les auteurs racontent ici pour binaire l’histoire de ce travail. L’intérêt de l’article est d’observer la recherche en train de se faire. Il n’est pas nécessaire de comprendre même leurs résultats. Dans un second article, ils donneront plus de détails sur les contributions scientifiques. Serge Abiteboul et Chloé Mercier.

    La question originale a été posée pendant le workshop « Gamenet » sur la théorie des jeux mêlant informaticiens, mathématiciens et économistes à Maastricht (Pays-Bas) en 2022.  Les résultats mathématiques présentés par Guillaume Vigeral et Bruno Ziliotto sur les phénomènes de “révélations” dans les modèles de jeux à information imparfaite ont suscité la curiosité de Hugo et Florian au sujet des propriétés algorithmiques de ces jeux.

    Le poker est un exemple classique de jeu à information imparfaite : chaque joueur possède à tout moment une information partielle de la partie, à savoir il connaît sa main et ce que les autres joueurs ont annoncé, mais pas la main des autres joueurs. Les jeux à information imparfaite sont extrêmement durs à comprendre d’un point de vue algorithmique, et l’on peut même prouver que, dans des modèles très simples, ils sont “indécidables”, ce qui signifie qu’il n’existe pas d’algorithme permettant de construire une stratégie optimale. Analyser algorithmiquement les jeux à information imparfaite est un vaste programme de recherche, très actif dans le monde académique mais également dans l’industrie : Google DeepMind s’est par exemple attaqué à StarCraft. Son succès a été mitigé puisque, si l’IA a initialement battu les meilleurs joueurs mondiaux, des stratégies imprévisibles contrant l’IA ont ensuite été découvertes.

    Informellement, une “révélation” dans un jeu à information imparfaite correspond à un instant où les joueurs possèdent une connaissance complète de l’état du jeu. Par exemple au poker, lorsque tous les joueurs révèlent leurs cartes. Mais le mécanisme du jeu peut introduire après ce moment à nouveau des incertitudes, par exemple si un joueur pioche une nouvelle carte et ne la révèle pas. A son retour à Bordeaux, Hugo a posé à Nathanaël cette question fascinante : les jeux qui impliquent “régulièrement” des révélations sont-ils plus faciles à analyser d’un point de vue algorithmique ? Intuitivement, la difficulté d’analyser les jeux à information imparfaite est due à la multiplication des possibilités. Mais s’il y a “souvent” des révélations, ce nombre de possibilités devrait être réduit. Nous avons commencé à plancher sur ce sujet à trois : Nathanaël, Hugo, et Florian.

    Hugo et Florian ont rendu visite à Nathanaël pendant son année sabbatique à l’Université de Varsovie (en 2023), et l’hiver polonais leur a permis de faire une première découverte : ils ont prouvé que ces jeux n’étaient pas plus faciles à analyser que le cas général. Au lieu d’abandonner, ils ont décidé de se focaliser sur les processus de décisions Markoviens (MDP), cas particulier des jeux où il n’y a qu’un seul joueur. Dans ce nouveau cadre, ils ont formulé des conjectures et conçu un algorithme pour résoudre ces MDP, mais ils n’avaient pas encore de preuve complète.

    Encouragé par ces résultats, Hugo a proposé à Marius, alors étudiant en Master, d’effectuer son stage de recherche sur cette question au printemps 2023. Après de longs mois à manipuler des outils probabilistes et topologiques et après deux visites à Paris pour travailler avec Florian, les premières preuves ont été couchées sur papier. Le stage a en particulier permis de formaliser une distinction importante : il a distingué entre deux notions différentes de “révélations”, dites “faible” et “forte”. Malgré les progrès, de nombreuses questions restaient ouvertes.

    Pierre a alors commencé un post-doctorat dans l’équipe bordelaise en septembre 2023, peu après la fin du stage de Marius. Il a dévoré son rapport de stage, relançant encore une fois la machine : l’espoir fait vivre et nourrit la recherche. Nous avons alors fait de grands pas en avant, et obtenu des résultats positifs dans le cas de révélations fortes ainsi que des résultats négatifs pour les révélations faibles. Plus précisément, nous avons construit un algorithme permettant d’analyser les jeux avec des révélations fortes, et montré que cela était impossible (indécidable) en cas de révélations faibles. C’est aussi une expérience classique en recherche : lorsque l’on se lance dans un nouveau problème, on commence par faire de tout petits pas. Plus on avance dans la compréhension des objets, et plus on fait de grands pas, jusqu’à résoudre le problème (ou pas). Faire de la recherche, c’est ré-apprendre à marcher à chaque nouveau problème !

    Pour valider nos résultats empiriquement, nous avons collaboré avec Guillermo, expert des méthodes statistiques et exactes pour les jeux stochastiques. L’intérêt de l’algorithme que nous avions construit était d’être conceptuellement très simple et facile à implémenter. Il s’est avéré qu’il permet également en pratique de construire des stratégies plus performantes !

    Un article de recherche se doit d’être tourné vers le futur, d’ouvrir des pistes. Notre algorithme permet d’analyser les jeux avec des révélations (fortes). Une perspective intéressante est de retourner le problème : on peut se demander plus généralement ce que fait l’algorithme lorsqu’il est utilisé pour n’importe quel jeu, avec ou sans révélations. Cela permet d’envisager d’analyser tous les jeux, même les plus compliqués, mais en restreignant plutôt le type de stratégie que les joueurs utilisent, ou la quantité d’informations qu’ils sont capables de traiter.

    Marius Belly, Nathanaël Fijalkow, Hugo Gimbert, Florian Horn, Guillermo A. Pérez et Pierre Vandenhove