David Madore's WebLog: Nouvelles réflexions sur les LLM et les maths

(Plan :)

• Les preuves erronées
• La difficulté de vérifier
• Le positif et le négatif
• La difficulté n'est pas une grandeur unique
• Le problème de l'arrêt des exponentielles
• Les maths comme benchmark
• Preuves humaines, trop humaines ?
• Inventivité ?
• Paternité des idées
• Préoccupations pour l'avenir
• Le but des maths n'est pas de résoudre des problèmes
• Le rêve de « résoudre » les maths
• La déclaration de Leiden

☞ Les preuves erronées

D'abord, ça me semble important de souligner que les LLM actuels continuent à l'heure actuelle à produire énormément de démonstrations fausses (théorèmes hallucinés, appliqués avec les mauvaises hypothèses, confusions quand un terme a plusieurs sens, etc.). Même les « bons » modèles. (Oui, les bons en font moins, mais on leur demande des choses plus compliquées, et là ils en font encore beaucoup.) On peut parfois détecter ces erreurs, certainement les réduire, en demandant au LLM de vérifier sa propre preuve, mais même ainsi, la confiance n'est pas terrible. Du coup, si on veut quelque certitude, soit il faut formaliser la preuve en Lean[#2], ce qui n'est possible qu'avec un tout petit bout de la recherche en maths (dont beaucoup de problèmes d'Erdős[#3], qui ont la spécificité d'être très élémentaires), soit la faire vérifier par un expert humain, et là on a un bottleneck, parce que les experts ont autre chose à foutre que vérifier N preuves générées par IA dont beaucoup sont du bullshit.

[#2] Comme je l'explique dans un bout de mon précédent billet sur le sujet, Lean est un outil informatique dans lequel on peut exprimer des preuves mathématiques de façon formelle, et qui vont alors la vérifier (de façon complètement automatisée, et fiable). On peut demander à un LLM d'écrire ou de convertir la preuve en Lean. Mais pour que la preuve soit effectivement formalisable en Lean, il faut que tous les outils qu'elle utilise aient été eux-mêmes préalablement formalisés en Lean, ce qui, à l'heure actuelle, est loin de couvrir la totalité du spectre des mathématiques connues.

[#3] Paul Erdős était grand collectionneur de problèmes mathématiques, et ses problèmes sont devenus une sorte de défi pour les boîtes d'IA (je me demande ce qu'Erdős lui-même aurait pensé de cette situation, d'ailleurs). Mais il faut souligner que les problèmes d'Erdős représentent les intérêts du collectionneur, et qu'ils ont notamment un biais très important en faveur des énoncés élémentaires, souvent sans grande théorie derrière, et de certains domaines particuliers des maths (grosso modo : la combinatoire, la théorie des graphes, la théorie des nombres « élémentaire » / combinatoire / additive, éventuellement la théorie descriptive des ensembles).

En fait, c'est complètement con : on a automatisé une partie intéressante de la résolution de problèmes mathématiques (trouver une preuve), mais pas vraiment la partie chiante (vérifier les preuves), qui est pourtant, du point de vue théorique, parfaitement automatisable. (Un peu comme on préférerait que les IA nous débarrassent des choses chiantes de la vie, comme le ménage, et pas des choses créatives et intéressantes.)

☞ La difficulté de vérifier

Et en pratique, ce qui est en train de se passer en ce moment en maths, ce n'est pas tant que les problèmes ouverts tombent les uns après les autres (à part les problèmes d'Erdős), c'est que tout le monde est noyé par les preuves bidon produites par IA : avant, pour reconnaître un crackpot en maths c'était très facile (juste au style), maintenant, comme les preuves bidon produites par IA sont superficiellement hyper plausibles, c'est devenu extrêmement difficile de savoir sauf à tout lire en détails. Là on a un vrai problème.

(Et à moins de tout formaliser, ce n'est pas clair que le progrès des LLM nous tire d'affaire, parce que ce qui compte est le rapport entre leur capacité à générer du bullshit avancé et leur capacité à en détecter, et c'est pas évident comment il évolue.)

☞ Le positif et le négatif

C'est pour ça que je souligne que, à l'heure actuelle, il n'est pas du tout clair que la contribution des IA aux maths soit positive (même en ignorant totalement leurs coûts !). Il y a des termes >0 et des termes <0, et j'ai personnellement tendance à penser que la somme est <0.

Je peux aussi mentionner l'impact négatif qu'ont les LLM sur le site MathOverflow (une sorte de réseau social des mathématiciens, sous forme de questions-réponses); on peut toujours rêver qu'elles vont remplacer ça en mieux, mais pour l'instant ce n'est pas clair (ni gratuit !).

Donc je trouve assez fallacieux de ne parler que des progrès que les LLM ont apportés pour certains problèmes et de taire complètement tous les aspects négatifs sur la discipline. Peut-être que les contributions >0 vont augmenter à l'avenir, mais les <0 risquent d'empirer aussi ! Bref, bien malin qui saura dire à quoi ressemblera la somme.

L'enthousiasme (d'ailleurs assez relatif) de gens comme Terry Tao[#4] n'engage qu'eux : ce n'est pas parce qu'il est très fort que son avis est plus important que n'importe quel autre mathématicien. Et je trouve d'ailleurs significatif que la vidéo ne retienne, des commentaires de 9 mathématiciens sur la preuve d'OpenAI du unit distance problem, que les plus positifs : j'encourage beaucoup à lire ceux de Melanie Matchett Wood, avec lesquels je me sens très en phase.

[#4] Terence Tao est professeur à UCLA, médaillé Fields, et considéré par beaucoup comme un des plus brillants mathématiciens vivant actuellement (voire le plus brillant, parce qu'il a un fan-club franchement pénible ; mais indiscutablement il est très fort pour résoudre des problèmes, et aussi capable de comprendre un nombre impressionnant de domaines différents des mathématiques). Il fait preuve d'un certain enthousiasme pour le rôle que les IA vont jouer dans l'avenir des mathématiques, ce qui agace parfois certains collègues, surtout que ses propos sont pas mal utilisés par les zélotes de l'IA. (Mais bon, il est aussi signataire de la déclaration de Leiden, donc ce n'est certainement pas un enthousiasme sans réserves.)

☞ La difficulté n'est pas une grandeur unique

Beaucoup de spéculations (notamment dans la vidéo de Monsieur Phi) se fondent sur l'idée implicite que la difficulté d'un problème mathématique est une sorte de valeur objective, et notamment qu'elle serait la même pour les LLM et pour les humains. Vu qu'elle est déjà hyper différente d'un humain à l'autre, ça me semble particulièrement audacieux, comme hypothèse. Mais en tout cas, l'idée que les LLM deviennent très bons pour certains problèmes très durs pour les humains donc ils vont dépasser les humains en tout (je ne dis pas que la conclusion est fausse), elle repose sur une hypothèse très douteuse sur la nature linéaire de la difficulté mathématique.

Évidemment, c'est difficile de tester l'hypothèse il y a des problèmes de maths faciles pour les humains et difficiles pour les LLM parce que tout ce qui a jamais été écrit par un humain est connu des LLM (donc par définition elles savent faire), et qu'on ne sait même pas dans quelle direction chercher. Mais le fait est que certains collègues trouvent les LLM vraiment mauvais et d'autres spectaculairement bons, et on ne comprend pas bien la raison de ces différences (nature des problèmes ? qualité des modèles ? capacité à prompter efficacement ? effet placebo/nocebo dû aux préjugés sur les IA ?), mais pour l'instant on n'a vraiment aucune mesure scientifique sérieuse, juste plein d'anecdotes. En tout cas il est probable que les problèmes d'Erdős ne soient pas hyper représentatifs.

Je résumerais un peu la situation actuelle à celle où une boîte pharmaceutique aurait un produit à vendre et on mettrait en avant plein de témoignages de gens qui ont été guéris par ce médicament : je ne dis pas que ça ne dit rien, mais ça ne remplace pas une étude scientifique.

☞ Le problème de l'arrêt des exponentielles

La spéculation puisque les progrès sont très rapides, ils vont forcément aller extrêmement loin me semble particulièrement infondée : je ne sais pas quel mur les LLM peuvent risquer de heurter (économique ? énergétique ? technologique ? du processus d'entraînement ? de la nature même du modèle ?) mais je ne vois aucune raison particulière de penser que la position de telle ou telle barrière (si elle existe) est corrélée à la vitesse à laquelle on fonce dessus. Comme je le dis tout le temps (et comme j'ai passé toute la pandémie de covid à expliquer) : observer une exponentielle ne dit rien sur la manière dont elle s'arrêtera.

☞ Les maths comme benchmark

En tout état de cause, les développements ultra-rapides de ces derniers mois me semblent largement dus à une décision stratégique : OpenAI et les autres boîtes d'IA ont décidé d'utiliser les maths comme « benchmark »[#5] censément objectif pour montrer leur supériorité les unes sur les autres (notamment dans le contexte de l'introduction en bourse d'OpenAI). Évidemment, ce qui les intéresse n'est pas de faire des maths ni d'aider la science ou les mathématiciens, mais de vendre leurs produits. OpenAI a clairement décidé d'investir massivement pour une annonce spectaculaire, en ciblant les problèmes d'Erdős spécifiquement. Je ne dis pas que les LLM ne peuvent pas progresser plus généralement, mais il faut une certaine naïveté pour s'imaginer que ce développement est représentatif de quelque chose qui pourra être soutenu, ou qu'il est représentatif des maths en général, pire, de l'intelligence en général.

[#5] Comprendre : comme moyen d'évaluation, comme test pour se comparer les unes aux autres.

(Et là je me dois de citer la loi de Goodhart comme je le fais souvent : utiliser les maths / problèmes d'Erdős comme benchmark pour les IA avait peut-être un sens, mais dès que les boîtes s'en sont aperçu, ça a cessé d'être un bon benchmark.)

C'est donc notamment à cause de ça que beaucoup de mathématiciens sont exaspérés de la manière dont les boîtes d'IA font leur pub sur leur dos et leur donnent un rôle quasiment de prospectus publicitaire, au détriment de la discipline.

J'avoue que je me serais attendu à ce qu'un philosophe prenne un peu plus de recul et de nuance sur ces questions, justement, et se dire qu'il y a peut-être une part de trompe-l'œil dans les annonces spectaculaires – ce qui ne veut pas dire que tout est bidon non plus ! (Ceci dit, je reconnais tout à fait que la vidéo ne prend pas la comm d'OpenAI comme argent comptant, et elle souligne à juste titre un énorme manque de transparence, notamment sur le temps qu'il leur a fallu pour résoudre le unit distance problem[#6], le nombre de problèmes envisagés, etc.)

[#6] Voir un bout de mon précédent billet sur le sujet pour ce qu'est le unit distance problem d'Erdős, ou bien voir la vidéo que je commente, qui me semble s'en sortir pas mal sur la vulgarisation (mais ce n'est pas vraiment moi qui peux juger la qualité des explications). Ce qui importe est que la résolution par OpenAI (juste avant leur introduction en bourse) de ce problème ouvert passablement célèbre est une annonce assez spectaculaire et qui attire énormément l'attention du monde mathématique et au-delà (et explique ce billet de blog, et le précédent, et la vidéo commentée, etc.).

☞ Preuves humaines, trop humaines ?

La vidéo dit très bien que les preuves trouvées par les LLM ne sont pas du tout « surhumaines ». On peut ajouter : elles sont étonnamment élémentaires[#7] (dans le cas du unit distance problem, tout le travail technique « sophistiqué » était dans des articles d'Ellenberg-Venkatesh, Golod-Shafarevich et surtout Hajir-Maire-Ramakrishna, cités dans les remarques sur la preuve).

[#7] La preuve trouvée par OpenAI du unit distance problem nécessite pour être comprise l'équivalent en gros d'un M2 de théorie des nombres (plus la théorie de Golod-Šafarevič, sur laquelle il est facile de trouver des références). Peut-être que pour le grand public, il faut juste un M2 de la spécialité pour comprendre la preuve peut paraître signaler un grand niveau d'ésotérisme, mais la grande majorité des preuves produites par la recherche mathématique actuelle sont bien plus techniques (disons que j'ai fait mon doctorat sur la géométrie algébrique et que je suis parfaitement incapable de comprendre les détails de la grande majorité des articles de maths en géométrie algébrique). Et quelque part, ce peu de spécialisation est remarquable, parce que les LLM, évidemment, ont appris la totalité des champs de la recherche mathématique actuelle : donc sur le principe elles auraient parfaitement pu produire une preuve mélangeant douze outils de douze domaines des maths de manière complètement inimaginable pour un humain — mais non. Je ne sais pas bien ce qu'il faut en conclure.

La question à 1000 milliards de zorkmids c'est si c'est une limitation qualitative des LLM ou si c'est le résultat du benchmark choisi (les problèmes d'Erdős).

Mais en tout cas, Gowers passe une bonne partie de ses remarques[#8] à analyser ce qui manquait aux humains pour résoudre le problème (pourquoi on l'a raté), c'est vraiment intéressant, et les commentateurs sont largement passés à côté de ces remarques (peut-être trop techniques). Et la morale c'est peut-être que la découverte de cette preuve nous en apprend beaucoup plus sur la manière (forcément faillibles) dont nous humains pensons les mathématiques que sur la manière dont les LLM le font.

[#8] Ici et à d'autres endroits, je fais référence aux commentaires de 9 mathématiciens sur la preuve d'OpenAI du unit distance problem, publiés en même temps que la preuve elle-même (qu'ils ont pu voir en avant-première et sous embargo). J'invite tout le monde à les lire, même les non-mathématiciens (on peut sauter les passages techniques), elles sont très intéressantes, dans des directions assez différentes. Tim Gowers (médaillé fields et professeur au Collège de France) est un de ceux qui a écrit des commentaires.

☞ Inventivité ?

On ne sait donc pas, à ce stade, si les LLM sont capables d'imaginer de nouvelles maths (notamment, des définitions fécondes, des conjectures intéressantes, ou même des outils techniques nouveaux). Il n'est pas exclu que leur processus d'entraînement (trouver des preuves), ne leur confère pas la perception du monde mathématique qu'a l'intuition humaine (notamment parce que celle-ci est en bonne partie non-verbale, ou simplement parce qu'« intéressant » est une mesure subjective humaine par définition adaptée au cerveau humain).

☞ Paternité des idées

Un problème lié est que les LLM sont particulièrement mauvais pour signaler la paternité de leurs idées. Quand un mathématicien humain honnête écrit une preuve, s'il utilise les idées d'autres gens, il signale ces idées et cite ces gens. Les LLM, quand on leur demande de résoudre un problème, ne font pas ça. Ce n'est pas clair si elles s'en sortent mieux quand on leur demande explicitement de citer les idées proches, mais en tout cas elles ne le font pas par défaut. (D'où le fait que plein de preuves qu'on a crues « nouvelles » n'étaient en fait pas nouvelles.) Donc là aussi on a un impact négatif important sur les maths : des preuves pondues par LLM effacent les contributions des mathématiciens humains dont elles reprennent les idées, ne respectant pas la déontologique du domaine.

☞ Préoccupations pour l'avenir

Bref, ce qui préoccupe les matheux actuels, ce n'est pas d'être « dépassés » par les IA, c'est plutôt des questions comme :

• est-ce qu'on ne va pas être noyés sous les fausses preuves ? voire, sous les preuves justes mais impossibles à vérifier ou à comprendre ?
• comment va-t-on convaincre les politiques de continuer à financer les postes de mathématiciens humains ?
• comment va-t-on les recruter, d'ailleurs ?
• et qui contrôle l'accès à ces IA ? comment ne pas laisser le pouvoir sur les maths aux boîtes qui les développent ?

(Sur ce dernier point, je pense par exemple que s'il s'avère que les LLM peuvent être meilleurs que les humains en démonstrations de théorèmes, il est vital de développer des LLM totalement ouverts et que chaque chercheur puisse utiliser sur les serveurs de son labo, pas sur ceux contrôlés par OpenAI / Anthropic. Je vais d'ailleurs pinger Pierre-Carl Langlais à ce sujet, parce que c'est le seul, parmi les gens que je vois parler d'IA, qui arrive à articuler la distinction entre les LLM en général et les LLM particuliers que 3–4 grosses boîtes veulent nous vendre.)

☞ Le but des maths n'est pas de résoudre des problèmes

Maintenant, il y a aussi une question qu'on ne peut pas manquer de se poser, c'est : pourquoi fait-on des maths, au juste ? Dans quel but et à quoi ça sert ? Ce fil/post n'est évidemment pas la place pour y répondre, mais juste une petite réflexion.

Beaucoup de gens comparent les maths aux échecs, et le progrès des IA actuelles à Deep Blue versus Kasparov ou je ne sais quoi. C'est vraiment une comparaison stupide, parce que les échecs sont un jeu adversarial, les maths n'en sont pas. On n'est pas dans une match « l'humain contre la machine », ça n'aurait vraiment aucun sens. Les maths sont l'exploration d'un univers (mental, ou dicté par une logique préexistante selon votre orientation philosophique).

Et le problème avec cette conception adversariale des maths comme une sorte de match où il faut résoudre les problèmes plus vite qu'un autre ou mieux qu'une machine, c'est que ça conduit à une approche totalement absurde de la discipline.

Alors là je dois reconnaître que les matheux eux-mêmes en sommes largement responsables : on a tellement intériorisé cette idée que les maths consistent à résoudre des problèmes et trouver des démonstrations, on s'en est tellement servis pour se juger les uns les autres, y compris dans un système absurde de course à la récompense (dont la médaille Fields et d'autres prix font partie) où ce qui est valorisé est d'avoir produit des théorèmes durs, qu'on a pas mal perdu le sens de notre mission, qui n'est pas de résoudre des problèmes, de trouver des démonstrations ou de pondre des théorèmes, mais d'éclairer notre compréhension du monde mathématique.

Et là les IA nous ramènent brutalement à la réalité : si une IA demain sort une démonstration gigantesque de l'hypothèse de Riemann[#9], formalisée en Lean mais illisible pour un humain, on se rendra compte que ça n'avait en fait aucun intérêt, parce que le but des maths n'est pas d'accumuler les théorèmes ou de résoudre des problèmes, et qu'en nous imaginant que c'était ça notre but nous avons transformé les maths en un jeu où les IA peuvent nous « battre ». Ça c'était notre faute.

[#9] S'il y a quelque chose qui ressemble le plus au graal des mathématiques, c'est probablement l'hypothèse de Riemann. Elle fait partie des sept problèmes du millénaires sur lesquels l'institut Clay a annoncé en l'an 2000 mettre une récompense de 1 000 000 $ pour une solution (un seul a été résolu pour l'instant). Et même parmi les 7, je pense qu'on peut dire que l'hypothèse de Riemann est le plus prestigieux. Mais ce que j'essaie de dire, c'est qu'une preuve de l'hypothèse de Riemann n'est intéressante que si elle nous apporte une vraie compréhension (humaine) de l'hypothèse de Riemann. La preuve n'est pas le but : la preuve est le moyen. Si on a une preuve vérifiable mais incompréhensible, ça n'a aucun intérêt. (Ceci est une expérience de pensée : pour l'instant, les preuves générées par les LLM sont tout à fait compréhensibles, probablement justement parce qu'elles imitent les preuves que nous écrivons nous-mêmes en langage naturel.)

Pour un développement très bien écrit des idées de ces ~3 derniers paragraphes, je renvoie au texte de mon ancien collègue[#10] David Bessis intitulé The fall of the theorem economy — avec lequel je suis globalement d'accord.

[#10] Nous étions tous les deux au département de maths de l'ENS en 2004–2007.

☞ Le rêve de « résoudre » les maths

De toute façon, nous autres mathématiciens humains sommes habitués au fait que l'immense majorité des mathématiques nous restera à jamais inaccessible. On a même des théorèmes précis dans ce sens (Gödel, Turing) : aucune machine ne pourra jamais « résoudre » les mathématiques. D'ailleurs c'est peut-être ironique que c'était en quelque sorte un rêve de Hilbert[#11] d'imaginer une telle machine (cf. le Entscheidungsproblem), on peut dire en simplifiant beaucoup que Gödel et/ou Turing ont anéanti ce rêve en prouvant que c'était impossible, mais en tout cas on ne fera pas croire que les mathématiciens ont peur du sciemus (nous saurons) après avoir eu peur du ignorabimus (nous ne saurons pas). Nous n'avons pas peur d'être dépassés. Nous avons évidemment envie de savoir des choses. Le problème est ailleurs.

[#11] David Hilbert, certainement un des plus grands mathématiciens de tous les temps, et qui partage avec Henri Poincaré de pouvoir prétendre être le dernier « grand universaliste », c'est-à-dire capable de comprendre la totalité des mathématiques de son époque. Hilbert est notamment connu comme le chef de file du courant formaliste, un programme visant à fonder les mathématiques sur une base axiomatique permettant de réduire au moins la vérification des démonstrations et possiblement leur découverte (sur le premier point on peut dire qu'il a eu raison, sur le second il a eu tort) à un procédé purement mécanique. Gödel et Turing ont montré que ce programme souffrait de toutes sortes de limitations (pour simplifier, disons que Gödel a montré que tout ce qui est vrai n'est pas forcément démontrable, et Turing a montré que même savoir si quelque chose est démontrable, et a fortiori si quelque chose est vrai, ne peut pas se mener par un procédé mécanique).

Le problème est que les IA menacent les mathématiques et les mathématiciens de toutes sortes d'autres manières qu'en « résolvant » les maths : j'en ai évoqué certaines, mais la plus évidente est que les décideurs pourraient croire que les IA ont « résolu » les maths, donc pourquoi recruter ?

☞ La déclaration de Leiden

Et pour finir :

Il n'y a évidemment pas de porte-parole officiel de tous les mathématiciens, mais ce qui ressemble le plus à une position commune du monde mathématique sur l'IA est la déclaration de Leiden — que j'invite vivement à lire.