Il y a cinq ans, en avril 2019, une équipe de DeepMind (la société qui a développé AlphaGo, la première intelligence artificielle capable de battre un être humain au jeu de Go) soumettait un réseau de neurones, spécialement entraîné pour résoudre des examens, à des mathématiques, un examen du secondaire. Le résultat? Un F décevant, l’équivalent italien d’un trois. Début 2024, à une époque où l’on ne parle que d’intelligence artificielle, un résultat diamétralement opposé a été obtenu : une IA développée par DeepMind en collaboration avec l’Université de New York a résolu correctement 75 % des problèmes de géométrie de l’Internationale. Olympiade mathématique (OMI), le concours international de mathématiques le plus prestigieux destiné aux lycéens, atteignant le niveau de la médaille d’or. Que nous dit ce dernier triomphe de l’intelligence artificielle ? Est-ce une nouvelle confirmation de l’obsolescence de la pensée humaine, ou un succès globalement prévisible ?
Pour comprendre cela, il faut aller au-delà des gros titres sensationnalistes et découvrir de quoi est faite AlphaGeometry, l’IA qui a brillamment résolu les problèmes de l’OMI.
Anatomie d’une IA
Le nom « intelligence artificielle » est évocateur, mais en même temps très générique : de même qu’un vélo, une voiture et un bateau à moteur sont tous trois des véhicules, mais avec des usages très différents, il existe des types d’intelligence artificielle radicalement différents et avec des fonctions également domaines d’application variés. Depuis le lancement de ChatGPT, nous connaissons tous le terme « chatbot » (ou, pour ceux qui aiment les aspects techniques, Large Language Models, LLM). Il s’agit d’IA qui, en première approximation, génèrent des textes à partir de l’analyse des fréquences d’énormes quantités de phrases (une estimation indique que ChatGPT 3 a été entraîné sur pas moins de 500 Go de données, ce qui correspond approximativement à 100 millions d’écrits). pages).
Cependant, toutes les IA ne peuvent pas être attribuées aux LLM. AlphaGeometry, par exemple, utilise un principe différent. En première approximation, il s’agit d’un système composé de deux parties : un logiciel traditionnel de preuve automatique de théorèmes, supporté par un LLM formé exclusivement aux preuves de géométrie. Les problèmes de géométrie de l’OMI doivent être résolus par des preuves. Autrement dit, nous devons partir des hypothèses fournies par chaque problème et, sur cette base, construire un raisonnement qui montre pourquoi elles impliquent la véracité des conclusions requises. Ce type de raisonnement déductif est, dans une plus ou moins grande mesure pour diverses branches des mathématiques, déjà partiellement traduisible en termes algorithmiques : les logiciels capables de prouver automatiquement des théorèmes existent depuis les années 1960 (mais les bases théoriques précèdent même la naissance des premiers des ordinateurs).
De temps en temps, ces logiciels traditionnels non basés sur l’IA nécessitent une aide extérieure. Jusqu’à il y a quelques années, cette aide était exclusivement assurée par des utilisateurs humains. La nouveauté d’AlphaGeometry est qu’il a remplacé les utilisateurs humains par un LLM formé spécifiquement aux textes de géométrie, avec pour tâche de fournir de nouvelles données d’entrée au logiciel pour prouver des théorèmes en cas de panne. Par exemple, cela pourrait suggérer de réaliser des constructions auxiliaires que le prouveur du théorème n’est pas en mesure de réaliser de manière autonome. Le succès d’AlphaGeometry à l’OMI peut donc être paraphrasé ainsi : l’équipe DeepMind a réussi à former un LLM capable de supporter parfaitement un prouveur automatique de théorème de géométrie traditionnel.
Il ne s’agit pas d’un résultat isolé : au contraire, déjà en 2019, une équipe de scientifiques de Google avait développé HOList, une IA de preuve automatique de théorèmes capable d’obtenir plus de 1 200 nouveaux résultats corrects sans aucune aide. La structure était similaire à celle d’AlphaGeometry : les logiciels traditionnels pour réaliser des démonstrations étaient combinés avec l’IA, dans ce cas basée sur l’apprentissage profond.
IA spécialisée et IA généraliste
AlphaGeometry et HOList sont des IA spécialisées. Le terme fait référence à une IA entraînée pour effectuer quelques tâches spécifiques, en l’occurrence prouver des théorèmes. Le terme « spécialisé » s’oppose au terme « généraliste », qui désigne plutôt une IA qui n’est pas optimisée pour des tâches particulières. ChatGPT est un exemple d’IA généraliste, et il est peu probable qu’elle remporte des médailles d’or à l’Olympiade internationale de mathématiques. Il faut cependant reconnaître que les performances de l’IA généraliste, même dans le domaine mathématique, s’améliorent à chaque nouvelle version publiée.
Il ne faut cependant pas oublier les limites d’applicabilité : ce sont des systèmes qui génèrent des résultats souvent génériques et qui, après une analyse minutieuse, se révèlent incomplets. De plus, je ne recommanderais à personne d’effectuer des calculs avec des LLM : les chiffres des résultats sont choisis de manière probabiliste et il y a toujours un pourcentage d’erreur, qui augmente beaucoup plus vite que la complexité des opérations. Les logiciels de calcul traditionnels, basés sur des algorithmes, restent le meilleur choix pour ce type de tâches : ils ne commettent pas d’erreurs et ont des temps d’exécution optimisés (et, par conséquent, également un coût énergétique moindre).
Quel avenir pour l’IA en mathématiques ?
Même si l’IA, tant spécialisée que généraliste, présente encore diverses limites, on ne peut éluder la question : comment l’IA va-t-elle changer notre quotidien ? Beaucoup se posent la question, y compris des mathématiciens de très haut niveau. Par exemple, les numéros d’avril et juillet 2024 de Bulletin de la Société Mathématique Américaine, l’un des magazines les plus prestigieux dans le domaine, est entièrement dédié à la manière dont l’IA va changer la pratique mathématique. C’est une occasion unique de s’arrêter et de réfléchir sur ce que sont les mathématiques, quel est le rôle des personnes qui les pratiquent au quotidien et quelle valeur attribuer aux démonstrations (peu importe qui les a obtenues : humains ou logiciels).
En réalité, les mathématiciens ne sont pas étrangers aux réflexions sur le rôle des preuves : un bref aperçu de quelques points de vue faisant autorité est présenté ici. Mais aujourd’hui, cette question doit être abordée à la lumière de la capacité de l’IA à produire de nouvelles démonstrations du plus haut niveau à une vitesse vertigineuse. Il ne s’agit pas uniquement de questions philosophiques : Terence Tao, médaillé Fields 2006 et plus jeune médaillé d’or à l’OMI, a été chargé par la Maison Blanche de mener des expériences pour comprendre quel peut être l’impact de l’IA sur la science ; ces recherches donneront lieu à des recommandations qui influenceront les choix politiques en matière d’IA.
IA : prédire l’avenir ou vivre le présent ?
Même en tenant compte de son histoire, qui a débuté dans la première moitié du XXe siècle, l’IA en est encore à ses balbutiements : toute prédiction sur ses évolutions futures risque de s’avérer fausse. Quoi qu’il en soit, la période de maturation de ces outils ne peut être évitée et doit être saluée, malgré toute la complexité et les dilemmes qu’elle soulève. Si nous ne relevons pas le défi, d’autres sujets, à commencer par les développeurs d’IA eux-mêmes, dicteront l’ordre du jour et traceront la voie à laquelle nous devrons tous nous adapter (une voie davantage inspirée par les intérêts économiques et la devise avancer vite et casser des choses plutôt que des idéaux philanthropiques).
Une alternative plus intéressante nous vient d’une des contributions au numéro d’avril de Bulletin de la Société Mathématique Américaine: faisant écho à Thoreau, le défi que nous pose l’IA est de « vivre délibérément, en face uniquement des faits essentiels de la vie », en déléguant aux machines tout ce qui ne relève pas de l’intelligence humaine.
Un merci spécial à Chiara Roglieri pour les discussions intéressantes sur l’IA et pour le partage de l’article de Américain scientifique sur AlphaGemoetry.
