L’IA s’améliore dans la gestion de la recherche mathématique
images lucadp / getty
Une révolution de l’intelligence artificielle est-elle sur le point de transformer les mathématiques? Certains mathématiciens éminents le pensent, grâce à des outils automatisés qui peuvent aider à rédiger des preuves montrant soudainement des sauts impressionnants en capacité, avec le potentiel de changer la façon dont la recherche mathématique est effectuée.
Environ 100 des principaux mathématiciens du monde se sont réunis à l’Université de Cambridge en juin pour une conférence dont le thème était basé sur la question de savoir si les ordinateurs pourraient aider les mathématiciens à résoudre certains problèmes de longue date sur la façon de vérifier que leurs preuves étaient correctes. Ce processus, connu sous le nom de formalisation, n’a pas nécessairement à impliquer l’intelligence artificielle, et en fait une réunion similaire tenue à Cambridge en 2017 n’a fait aucune mention de l’IA.
Mais huit ans plus tard, l’IA est survenue à pas de géant, notamment avec le succès de grands modèles de langue alimentant des outils comme Chatgpt. Cela a suscité un nouvel intérêt sur la question de savoir comment l’IA pourrait affecter les mathématiques, de la traduction automatique des preuves écrites par l’homme dans un langage formel et comprimé, à la construction de preuves elles-mêmes.
«C’est un peu écrasant», explique Jeremy Avigad à l’Université Carnegie Mellon en Pennsylvanie, qui a aidé à organiser la réunion. «C’est sympa; je fais ça depuis longtemps et c’était une sorte de truc de frange, de niche. Tout d’un coup, je me retrouve populaire.»
Deux des pourparlers ont été organisés par Google Deepmind, qui a fait la une des journaux lorsque son système d’IA, Alphaproof, a obtenu un score de médaille d’argent à l’Olympiade mathématique internationale (IMO), une concurrence prestigieuse pour les jeunes mathématiciens et une cible de longue date pour les systèmes d’IA. «Si vous parlez aux mathématiciens et que vous leur interrogez sur le [AlphaProof] Résultats de l’OMI, vous auriez eu des réactions différentes. Je pense que la plupart diraient que ce sont des problèmes de lycée assez difficiles, mais peut-être que certains autres mathématiciens les appelleraient triviaux », explique Thomas Hubert, ingénieur de recherche chez DeepMind.
Hubert et son équipe ont montré que Alphaproof pouvait aller au-delà de la compétition de l’OMI, pour aider à formaliser une petite partie du théorème de nombre premier, un résultat important dans la théorie des nombres. Les mathématiques avaient déjà été converties en Lean, un langage de programmation, mais Alphaproof a pu prouver le théorème, puis vérifier qu’il était correct. «Je voulais faire une démo de la façon dont Alphaproof pourrait être utilisé dans la vraie vie», explique Hubert.
Morph Labs, une startup AI basée aux États-Unis, a également démontré un outil d’IA appelé Trinity, qui est conçu pour traduire les preuves complètement automatiquement, à partir de la notation mathématique manuscrite et générant une preuve entièrement formalisée et vérifiée dans Lean. Bhavik Mehta à l’Imperial College de Londres, qui a consulté Morph Labs, a montré un exemple de Trinity prouvant un théorème relatif à la conjecture ABC, qui reste infâme le sujet d’un débat intense sur le fait qu’il est vrai ou non – quelque chose que la formalisation pourrait aborder.
Bien que cette preuve ne soit qu’un petit élément constitutif de toute la preuve nécessaire pour la conjecture ABC, et Trinity nécessitait une version légèrement plus détaillée de la preuve manuscrite que le document d’origine, de nombreuses personnes ont été surpris de la quantité de code mathématique correct généré par l’outil.
«La différence entre ce que Morph a fait et ce qui s’était passé auparavant, c’est qu’ils ont pris un journal entièrement en mathématiques, bien que de 1962 qui ne manquait que quatre pages, un humain [then] a cassé l’argument en petits morceaux, puis une machine vient de traduire le tout en maigre “, explique Kevin Buzzard à l’Imperial College de Londres.” Je ne suis pas sûr que nous ayons déjà vu quelque chose de tel auparavant. “
Cependant, il n’est toujours pas clair comment cela fonctionnera pour d’autres domaines de mathématiques, explique Mehta. “C’était essentiellement la première tentative, et la première tentative a fonctionné, peut-être qu’elle a eu de la chance.”
Christian Szegedy à Morph Labs affirme qu’une fois que l’outil est entièrement opérationnel, il progresse rapidement. «Une fois qu’une boucle de rétroaction est établie et que nous n’avons pas besoin de la quantité de maintien de la main dont ce théorème avait besoin… alors il devient essentiellement une réaction en chaîne et nous pouvons faire toutes les mathématiques à la fois», dit-il.
Des outils comme ceux-ci sont déjà au moment où ils pourraient être incroyablement utiles aux mathématiciens, explique Timothy Gowers à l’Université de Cambridge. «Il faudra juste un peu de travail pour les créer, et il semble y avoir beaucoup de gens qui souhaitent faire précisément cela, donc je pense qu’au cours des prochains, et je veux vraiment dire quelques-uns, de un à cinq ans, il y aura des changements dans la façon dont nous ferons des mathématiques qui rivaliseront en importance les changements dans la pratique mathématique provoqués par le courrier électronique, Latex. [the standardised maths notation]Arxiv [an online paper repository] et Google. “
Mais tous les mathématiciens ne conviennent pas que le journal Morph Labs était si impressionnant. Rodrigo Ochigame à l’Université de Leiden aux Pays-Bas prévoit que nous ne connaissons pas tous les détails de l’œuvre. «Ils n’ont publié qu’une seule sortie, éventuellement sélectionnée par cerise, de leur système sans rédiger un document ou partager des informations de base sur leurs méthodes. Ils n’ont même pas dit s’ils ont testé leur système sur d’autres théorèmes», dit-il. “Lorsqu’on lui a demandé au public de la quantité de calcul utilisée par le modèle, ils ont refusé à plusieurs reprises de répondre, ce qui rend difficile l’évaluation de la signification de leur résultat.”
Et le scepticisme reste à peu près à quel point les outils d’IA peuvent être utiles. La plupart des mathématiciens travaillent toujours sans utiliser d’outils automatisés, et il n’est pas clair s’ils changeront d’avis à mesure que les outils s’améliorent, explique Minhyong Kim au Centre international des sciences mathématiques au Royaume-Uni. «Les mathématiques et les mathématiciens sont incroyablement diversifiés dans leurs inclinations. J’imagine que certaines personnes finiront par utiliser des outils d’IA très efficacement et de manière créative, tandis que certains essaieront de maintenir une distance.»
«Les gens sous-estiment la complexité, la créativité et la subtilité de la recherche mathématique», explique Ochigame, c’est pourquoi tant de recherches sont encore effectuées en utilisant un stylo, un papier et une pensée profonde. «Il y a un énorme écart entre les compétitions de mathématiques du secondaire, comme l’OMI et la recherche de pointe», dit-il.
Sujets:
Sur le même sujet
