L’IA arrive aussi pour les mathématiques

Dans la collection du musée Getty de Los Angeles se trouve un portrait du XVIIe siècle du mathématicien grec ancien Euclide : échevelé, tenant des feuilles d’Éléments, son traité de géométrie, aux mains crasseuses.

Pendant plus de 2 000 ans, le texte d’Euclide a été le paradigme de l’argumentation et du raisonnement mathématiques. Euclide commence par des définitions presque poétiques, a déclaré Jeremy Avigad, un logicien à l’Université Carnegie Mellon, dans un e-mail. Il a ensuite construit les mathématiques de l’époque par-dessus cela, prouvant les choses de telle sorte que chaque étape successive découle clairement des précédentes, en utilisant les notions de base, les définitions et les théorèmes antérieurs. Il y a eu des plaintes selon lesquelles certaines des étapes évidentes d’Euclide étaient moins qu’évidentes, a déclaré le Dr Avigad, mais le système a fonctionné.

Mais au 20ème siècle, les mathématiciens n’étaient plus disposés à fonder les mathématiques sur cette base géométrique intuitive. Au lieu de cela, ils ont développé des systèmes formels, des représentations symboliques précises, des règles mécaniques. Finalement, cette formalisation a permis de traduire les mathématiques en code informatique. En 1976, le théorème des quatre couleurs qui stipule que quatre couleurs sont suffisantes pour remplir une carte afin que deux régions adjacentes ne soient pas de la même couleur est devenu le premier théorème majeur prouvé à l’aide de la force brute informatique.

Aujourd’hui, les mathématiciens sont aux prises avec la dernière force de transformation : l’intelligence artificielle.

En 2019, Christian Szegedy, un informaticien anciennement chez Google et maintenant dans une start-up de la Bay Area, a prédit qu’un système informatique égalerait ou dépasserait la capacité de résolution de problèmes des meilleurs mathématiciens humains d’ici une décennie. L’année dernière, il a révisé la date cible à 2026.

Akshay Venkatesh, mathématicien à l’Institute for Advanced Study de Princeton et lauréat de la médaille Fields en 2018, n’est pas actuellement intéressé par l’utilisation de l’IA, mais il tient à en parler. Je veux que mes étudiants réalisent que le domaine dans lequel ils évoluent va beaucoup changer, a-t-il déclaré lors d’une interview l’année dernière. Il a récemment ajouté par e-mail : Je ne suis pas opposé à l’utilisation réfléchie et délibérée de la technologie pour soutenir notre compréhension humaine. Mais je crois fermement que la pleine conscience de la façon dont nous l’utilisons est essentielle.

En février, le Dr Avigad a assisté à un atelier sur les preuves assistées par machine à l’Institute for Pure and Applied Mathematics, sur le campus de l’Université de Californie à Los Angeles. (Il a visité le portrait d’Euclide le dernier jour de l’atelier.) Le rassemblement a attiré un mélange atypique de mathématiciens et d’informaticiens. Cela semble conséquent, a déclaré Terence Tao, mathématicien à l’université, lauréat d’une médaille Fields en 2006 et organisateur principal des ateliers.

Le Dr Tao a noté que ce n’est qu’au cours des deux dernières années que les mathématiciens ont commencé à s’inquiéter des menaces potentielles des IA, que ce soit pour l’esthétique mathématique ou pour eux-mêmes. Que des membres éminents de la communauté abordent maintenant les problèmes et explorent le type potentiel de rupture du tabou, a-t-il déclaré.

Un participant remarquable à l’atelier était assis au premier rang : une boîte trapézoïdale nommée robot à main levée qui émettait un murmure mécanique et levait la main chaque fois qu’un participant en ligne avait une question. Cela aide si les robots sont mignons et non menaçants, a déclaré le Dr Tao.

Apportez les geignards de preuve

De nos jours, les gadgets ne manquent pas pour optimiser notre alimentation, notre sommeil, notre exercice physique. Nous aimons attacher des choses à nous-mêmes pour qu’il soit un peu plus facile de bien faire les choses, a déclaré Jordan Ellenberg, mathématicien à l’Université du Wisconsin-Madison, lors d’une pause de l’atelier. Les gadgets d’IA pourraient faire la même chose pour les mathématiques, a-t-il ajouté : Il est très clair que la question est : que peuvent faire les machines pour nous, et non ce que les machines vont nous faire ?

Un gadget mathématique est appelé assistant de preuve ou démonstrateur de théorème interactif. (Automath était une première incarnation dans les années 1960.) Pas à pas, un mathématicien traduit une preuve en code ; puis un logiciel vérifie si le raisonnement est correct. Les vérifications s’accumulent dans une bibliothèque, une référence canonique dynamique que d’autres peuvent consulter. Ce type de formalisation fournit une base pour les mathématiques aujourd’hui, a déclaré le Dr Avigad, qui est le directeur du Hoskinson Center for Formal Mathematics (financé par l’entrepreneur crypto Charles Hoskinson), de la même manière qu’Euclid essayait de codifier et de fournir une base pour les mathématiques de son temps.

Dernièrement, le système d’assistant de preuve open-source Lean attire l’attention. Développé chez Microsoft par Leonardo de Moura, un informaticien maintenant chez Amazon, Lean utilise un raisonnement automatisé, qui est alimenté par ce que l’on appelle la bonne intelligence artificielle à l’ancienne, ou IA symbolique GOFAI, inspirée par la logique. Jusqu’à présent, la communauté Lean a vérifié un théorème intrigant sur le retournement d’une sphère ainsi qu’un théorème pivot dans un schéma d’unification des domaines mathématiques, entre autres gambits.

Mais un assistant de preuve a aussi des inconvénients : il se plaint souvent de ne pas comprendre les définitions, les axiomes ou les étapes de raisonnement entrés par le mathématicien, et pour cela on l’a appelé un pleurnicheur de preuve. Tous ces gémissements peuvent rendre la recherche fastidieuse. Mais Heather Macbeth, mathématicienne à l’Université Fordham, a déclaré que cette même fonctionnalité fournissant une rétroaction ligne par ligne rend également les systèmes utiles pour l’enseignement.

Au printemps, la Dre Macbeth a conçu un cours bilingue : elle a traduit chaque problème présenté au tableau noir en code Lean dans les notes de cours, et les étudiants ont soumis des solutions aux problèmes de devoirs en Lean et en prose. Cela leur a donné confiance, a déclaré le Dr Macbeth, car ils ont reçu un retour instantané sur le moment où la preuve était terminée et si chaque étape en cours de route était bonne ou mauvaise.

Depuis sa participation à l’atelier, Emily Riehl, mathématicienne à l’Université Johns Hopkins, a utilisé un programme expérimental d’assistant de preuve pour formaliser les preuves qu’elle avait précédemment publiées avec un co-auteur. À la fin d’une vérification, elle a dit, je suis vraiment, vraiment profondément dans la compréhension de la preuve, bien plus profondément que je n’ai jamais compris auparavant. Je pense si clairement que je peux l’expliquer à un ordinateur vraiment stupide.

Raison brute mais est-ce mathématique ?

Un autre outil de raisonnement automatisé, utilisé par Marijn Heule, informaticien à l’Université Carnegie Mellon et chercheur sur Amazon, est ce qu’il appelle familièrement le raisonnement brut (ou, plus techniquement, un solveur de satisfaction ou SAT). En indiquant simplement, avec un codage soigneusement conçu, quel objet exotique vous voulez trouver, a-t-il dit, un réseau de superordinateurs parcourt un espace de recherche et détermine si cette entité existe ou non.

Juste avant l’atelier, le Dr Heule et l’un de ses doctorants. étudiants, Bernardo Subercaseaux, ont finalisé leur solution à un problème de longue date avec un fichier de 50 téraoctets. Pourtant, ce fichier est à peine comparable à un résultat que le Dr Heule et ses collaborateurs ont produit en 2016 : la preuve mathématique de deux cents téraoctets est la plus grande jamais réalisée, a annoncé un titre dans Nature. L’article se demandait ensuite si la résolution de problèmes avec de tels outils comptait vraiment comme des mathématiques. Selon le Dr Heules, cette approche est nécessaire pour résoudre des problèmes qui dépassent ce que les humains peuvent faire.

Un autre ensemble d’outils utilise l’apprentissage automatique, qui synthétise des tonnes de données et détecte des modèles, mais n’est pas doué pour le raisonnement logique, étape par étape. Googles DeepMind conçoit des algorithmes d’apprentissage automatique pour s’attaquer à des problèmes tels que le repliement des protéines (AlphaFold) et la victoire aux échecs (AlphaZero). Dans un article de Nature de 2021, une équipe a décrit ses résultats comme faisant progresser les mathématiques en guidant l’intuition humaine avec l’IA

Yuhuai Tony Wu, un informaticien anciennement chez Google et maintenant avec une start-up dans la Bay Area, a défini un objectif plus vaste d’apprentissage automatique : résoudre les mathématiques. Chez Google, le Dr Wu a exploré comment les grands modèles de langage qui autonomisent les chatbots pourraient aider avec les mathématiques. L’équipe a utilisé un modèle qui a été formé sur des données Internet, puis affiné sur un grand ensemble de données riches en mathématiques, en utilisant, par exemple, une archive en ligne d’articles de mathématiques et de sciences. Lorsqu’on lui a demandé en anglais courant de résoudre des problèmes mathématiques, ce chatbot spécialisé, nommé Minerva, était assez doué pour imiter les humains, a déclaré le Dr Wu lors de l’atelier. Le modèle a obtenu des scores supérieurs à ceux d’un élève moyen de 16 ans aux examens de mathématiques du secondaire.

En fin de compte, a déclaré le Dr Wu, il a imaginé un mathématicien automatisé qui a la capacité de résoudre un théorème mathématique tout seul.

Les mathématiques comme test décisif

Les mathématiciens ont réagi à ces perturbations avec des niveaux de préoccupation variables.

Michael Harris, de l’Université de Columbia, exprime des scrupules dans son Silicon Reckoner Substack. Il est troublé par les objectifs et les valeurs potentiellement contradictoires des mathématiques de recherche et des industries de la technologie et de la défense. Dans un récent bulletin, il a noté qu’un intervenant lors d’un atelier, AI pour aider le raisonnement mathématique, organisé par les Académies nationales des sciences, était un représentant de Booz Allen Hamilton, un entrepreneur gouvernemental pour les agences de renseignement et l’armée.

Le Dr Harris a déploré le manque de discussion sur les implications plus larges de l’IA sur la recherche mathématique, en particulier par rapport à la conversation très animée sur la technologie à peu près partout sauf les mathématiques.

Geordie Williamson, de l’Université de Sydney et collaborateur de DeepMind, a pris la parole lors du rassemblement du NAS et a encouragé les mathématiciens et les informaticiens à s’impliquer davantage dans de telles conversations. À l’atelier de Los Angeles, il a ouvert son discours avec une ligne adaptée de You and the Atom Bomb, un essai de 1945 de George Orwell. Étant donné la probabilité que nous soyons tous profondément touchés au cours des cinq prochaines années, a déclaré le Dr Williamson, l’apprentissage en profondeur n’a pas suscité autant de discussions qu’on aurait pu s’y attendre.

Le Dr Williamson considère les mathématiques comme un test décisif de ce que l’apprentissage automatique peut ou ne peut pas faire. Le raisonnement est la quintessence du processus mathématique, et c’est le problème crucial non résolu de l’apprentissage automatique.

Au début de la collaboration avec le Dr Williamsons DeepMind, l’équipe a trouvé un simple réseau de neurones qui prédisait une quantité en mathématiques qui m’intéressait profondément, a-t-il déclaré dans une interview, et il l’a fait avec une précision ridicule. Le Dr Williamson s’est efforcé de comprendre pourquoi ce serait l’étoffe d’un théorème, mais n’a pas pu. Personne chez DeepMind non plus. Comme l’ancien géomètre Euclide, le réseau de neurones avait en quelque sorte intuitivement discerné une vérité mathématique, mais le pourquoi logique de celle-ci était loin d’être évident.

Lors de l’atelier de Los Angeles, un thème important était de savoir comment combiner l’intuitif et le logique. Si l’IA pouvait faire les deux en même temps, tous les paris seraient annulés.

Mais, a observé le Dr Williamson, il y a peu de motivation pour comprendre la boîte noire que présente l’apprentissage automatique. C’est la culture du piratage dans la technologie, où si cela fonctionne la plupart du temps, c’est formidable, a-t-il dit, mais ce scénario laisse les mathématiciens insatisfaits.

Il a ajouté qu’essayer de comprendre ce qui se passe à l’intérieur d’un réseau de neurones soulève des questions mathématiques fascinantes, et que trouver des réponses offre aux mathématiciens une opportunité de contribuer de manière significative au monde.