« Une explosion exponentielle », m'a dit par téléphone le mathématicien Thomas Bloom, décrivant le flot de nouveaux résultats dans son domaine. Il ne savait pas que quelques heures plus tard, OpenAI allait publier 722 manuscrits mathématiques produits par un modèle d'IA inédit.
L’ampleur des nouveaux travaux confère une nouvelle urgence à la question : comment l’IA change-t-elle la découverte mathématique ? Dans leur course aux percées qui font la une des journaux, les sociétés d’IA ne divulguent généralement pas leurs méthodes et leurs données. Cette concurrence entre les sociétés d’IA menace de submerger la collaboration et la compréhension humaines.
Cette tension s'est manifestée en miniature sur un site Web géré par Bloom qui suit les progrès réalisés sur plus de 1 000 problèmes initialement posés et rassemblés par Paul Erdős, l'un des mathématiciens les plus prolifiques du XXe siècle. Ici, les gens collaboraient pour discuter de problèmes ouverts, ou de problèmes pour lesquels la meilleure solution n'avait pas été trouvée ou n'était pas connue de la grande communauté mathématique. Mais de plus en plus de visiteurs rivalisaient pour résoudre des problèmes ouverts avec des preuves d'IA qu'ils ne comprenaient souvent pas. Bloom, mathématicien à l'Université de Manchester en Angleterre, ne veut pas passer ses journées à arbitrer les travaux générés par l'IA. Ainsi, peu de temps après notre conversation, et avant de savoir qu'OpenAI allait annoncer ses derniers résultats, Bloom a annoncé qu'il ne marquerait plus les problèmes comme étant ouverts ou résolus, et il a également fermé les commentaires.
C'est vraiment passionnant que l'IA puisse résoudre autant de problèmes ouverts si rapidement. Mais peut-il aider les mathématiciens à comprendre les réponses et à s’en inspirer ?
Deux jours seulement après le déluge de résultats d'OpenAI, l'édition évaluée par des pairs d'une étude Google DeepMind est devenue publique. Rapporté pour la première fois dans une prépublication plus tôt cette année, il offre un aperçu de la manière dont un système d'IA s'attaque aux problèmes mathématiques ouverts. Le système appelé AlphaProof Nexus a résolu 9 problèmes d'Erdős et réalisé un certain nombre d'autres avancées mathématiques intéressantes, rapportent des chercheurs le 8 octobre dans Science.
Le rapport comprend une description détaillée de la manière dont les résultats ont été obtenus. De plus, les mathématiciens humains ont examiné de nombreuses preuves. C'est « assez différent » de la façon dont OpenAI et Anthropic gèrent leurs résultats mathématiques, dit Bloom.
« L'objectif ultime de toute IA pour la recherche en mathématiques », déclare Swarat Chaudhuri, chercheur et co-auteur de l'étude de Google DeepMind à Londres, devrait être « de faire progresser les mathématiques comme le font les mathématiciens humains ».
Un aperçu de l'intérieur d'une machine mathématique IA
Dans l'étude récemment publiée, Chaudhuri et ses collègues ont testé différentes configurations de leur système. Pour résoudre un ensemble de 353 problèmes Erdős ouverts, ils ont utilisé plusieurs agents alimentés par le modèle de langage Gemini. Ceux-ci pourraient faire appel à AlphaProof, un modèle d’IA spécialement entraîné pour faire des mathématiques, et source d’inspiration pour le nom du système global, pour les étapes difficiles. Les agents se sont également appuyés sur Lean, un logiciel mathématique qui identifie les étapes qui restent à prouver, pour vérifier leur logique. Les agents partageaient leur travail, faisant circuler des tentatives de preuves prometteuses et écartant celles qui ne fonctionnaient pas.
L’équipe a également testé une configuration plus simple sur les neuf problèmes résolus par le système complet. Les agents Gemini indépendants ont travaillé sur des épreuves en utilisant les commentaires de Lean, sans partager de tentatives ni consulter AlphaProof. Cette configuration a également résolu les neuf problèmes. Il était moins cher (utilisant moins de ressources informatiques) que le système complet pour les problèmes faciles et plus cher pour les deux plus difficiles. L’équipe n’a pas établi si une configuration plus simple résoudrait l’un des problèmes manqués par le système complet.
Le fait qu'une configuration plus simple puisse résoudre les neuf mêmes problèmes que le système complet a surpris Chaudhuri. Cela suggère que des modèles linguistiques de plus en plus performants peuvent aborder les mathématiques de recherche avec des outils de vérification relativement simples.
Mais la vérification informatique comporte une mise en garde. Lean vérifie uniquement la déclaration donnée, telle qu'elle est écrite dans son code. Et une déclaration mathématique peut être incorrectement traduite vers ou depuis le code Lean. Une prépublication du 6 octobre montre pourquoi cette traduction est importante. Dans cet article, les chercheurs identifient les inadéquations entre certaines parties de la preuve écrite Navier-Stokes d'OpenAI et son homologue Lean. Les disparités ne signifient pas que la preuve écrite est fausse, écrit l’équipe, mais elles notent qu’une preuve Lean valide ne valide pas automatiquement un article de mathématiques généré par l’IA.
C’est pourquoi l’examen effectué par les mathématiciens humains pour la publication DeepMind est si important. « Le mathématicien humain doit vraiment réfléchir au problème et fixer des objectifs pour le système », explique Chaudhuri. Et même si le système ne parvenait pas à terminer une preuve, ses étapes vérifiées aidaient les mathématiciens à se concentrer sur les lacunes restantes. « Les mathématiques sont en fin de compte un art humain », déclare Chaudhuri. « Le système améliore les connaissances de l'utilisateur humain, et celui-ci est capable de guider le système avec de nouvelles idées. »
La capacité en mathématiques implique des responsabilités
Les résultats mathématiques obtenus par le système AlphaProof Nexus « ne sont pas vraiment d'une importance capitale », explique Bloom, qui n'a pas participé aux travaux. Mais cela souligne l’approche plus mesurée de l’équipe. Google DeepMind, dit-il, « essaie d'être plus responsable en matière scientifique », tandis que des entreprises comme OpenAI utilisent les mathématiques pour présenter leurs logiciels. Les articles d'OpenAI et les preuves Lean qui les accompagnent ont été entièrement générés par l'IA, laissant à la communauté mathématique le soin de déterminer ce qui est utile ou inutile.
OpenAI affirme avoir travaillé avec un groupe consultatif indépendant pour développer les meilleures pratiques sur la façon de partager leurs résultats mathématiques en matière d'IA. Mais ce groupe a déclaré que son conseil était de ne pas tester de modèles d’IA inédits sur des mathématiques avancées, conseils que l’entreprise a clairement ignorés.
L'approche rapide et compétitive de l'entreprise continue d'aliéner des mathématiciens tels que Bryna Kra de l'Université Northwestern à Evanston, dans l'Illinois. Elle affirme que l'entreprise a amélioré ses efforts pour citer la littérature antérieure. Et elle est enthousiasmée par le potentiel de l’IA à résoudre d’importants problèmes de mathématiques. Mais l'inquiétude est largement répandue, dit-elle, que les modèles d'IA aient accédé aux travaux non publiés de certaines personnes. « Nous avions une culture saine, collaborative et de partage qui est en train d’être détruite », dit-elle. « Maintenant, les gens hésitent à partager leurs idées. »
Tous les mathématiciens ne pensent pas ainsi à propos de l’IA. La technologie « rend les mathématiques plus accessibles », explique Andrew Turner, qui se demande pourquoi un petit groupe de mathématiciens devrait décider de la manière dont nous résolvons les problèmes. Turner, qui a étudié les mathématiques et la physique et est aujourd'hui directeur technique de la société Plasma AI, basée à New York, pense que « les mathématiques deviennent de l'ingénierie ». Et faire des mathématiques avec des machines permettra aux gens de « répondre à des questions auparavant insondables ».
Quelques jours après que Bloom ait mis fin au concours sur son site Web, Plasma AI a annoncé la création d'un nouveau site Web pour suivre les progrès réalisés sur les problèmes d'Erdő. Ils apprécieront les résultats de l’IA.
Bloom ne voit pas les mathématiques comme une compétition à la Silicon Valley où l'on bouge vite et casse les choses. Je suis d’accord et j’espère que les gens curieux continueront à explorer les problèmes qui les intéressent, avec l’aide de l’IA plutôt que de prendre le relais. À la fin de son message annonçant les modifications apportées à son site Web, Bloom a écrit quelque chose qui me fait pleurer à chaque fois que je le lis. J'espère que tout le monde, même les utilisateurs d'IA les plus enthousiastes, trouvera le temps de faire ce type de travail : « Soyez confus, soyez coincé, inspirez-vous. Trouvez une preuve désordonnée, puis trouvez-en une meilleure », a-t-il écrit. « Soyez fatigué, ayez faim, entrez dans un état de flow. Discutez, riez, abandonnez, buvez du café et attaquez-le à nouveau. Soyez humain. Laissez votre cerveau être ouvert. »