☞ Remarques générales
Ceci est encore un billet que j'écris à reculons, l'IA
étant devenue un de ces sujets sur lesquels il est impossible d'ouvrir
la bouche sans attirer une horde de pénibles qui ne sont pas
intéressés par votre point de vue mais vous expliquer le leur,
typiquement soit que ça va amener l'humanité à un paradis
post-singularité
(immanentizer
l'eschaton
), soit qu'il faut immoler dans le feu tous les
ordinateurs qui font tourner une IA voire tous les gens
qui s'en servent. Et si on ne tient pas une de ces deux positions
mais quelque chose qu'on pourrait qualifier de plus
nuancé[#1], on aura affaire aux
deux sortes de pénibles à la fois, ce qui est deux fois plus pénible,
et ça décourage pas mal d'en parler, surtout si on ne sait pas bien
soi-même ce qu'on doit en penser (ce qui résume assez bien mon état
d'esprit).
[#] J'ai quelque part dans mon fichier TOBLOG de parler du sophisme du centrisme (qui consiste à croire ou à faire croire que si on est à mi-chemin entre deux opinions extrêmes on a forcément raison), et du méta-sophisme du centrisme (dont on parle moins, et qui consiste à accuser n'importe quelle opinion nuancée de sophisme du centrisme pour la discréditer), et de comment ces deux sophismes entretiennent la pauvreté du discours et la polarisation de toutes sortes d'opinions vaguement politiques.
Déjà, pour la terminologie, il faut rappeler (comme le fait Natacha
dans un billet que je lie juste en-dessous), parler
d'IA
souvent un mauvais point de départ, parce que
c'est surtout un buzzword et qu'il y a très peu de rapport
entre les choses qu'on met sous ce terme, à part faire le buzz et/ou
cristalliser le mécontentement : si on parle des IA
génératrices de texte il vaut mieux utiliser le terme
de LLM (Large Language Model), un
peu moins fourre-tout, pour la technologie actuelle. (Je vais donc
essayer de dire IA
quand je parle du domaine en
général, par exemple des compagnies d'IA,
et LLM
quand je parle des modèles textuels. Mais
je ne promets pas d'arriver à maintenir cette distinction de façon
complètement cohérente.)
Pour le contexte général, j'ai déjà écrit des
choses ici avec lesquelles je
continue à être d'accord[#2] ;
et je suis aussi globalement tout à fait d'accord avec ce que Natacha
écrit
dans ce
billet et avec ce que Matoo écrit
dans celui-ci.
On peut me qualifier d'IA-critique
parce que je
pense que, globalement, ces technologies apportent et vont continuer à
apporter à l'humanité un bénéfice net fortement négatif ; j'ajoute que
c'est plutôt la faute des gens et des compagnies qui sont derrière (et
lesquels en tireront, eux, un bénéfice fortement positif au détriment
de nous tous) que des techniques elles-mêmes ; mais en même temps, je
ne pense pas que cette critique autorise n'importe quelle mauvaise
foi[#3], ni d'essayer de
culpabiliser les utilisateurs
individuels[#4], ni de
prétendre, par exemple, que comme les IA peuvent
halluciner n'importe quoi (ce qui est vrai), elles ne peuvent jamais
servir à rien (ce qui est juste faux, et tellement déconnecté de la
réalité que ça rend toute critique inaudible ensuite).
[#2] Occasion comme une autre pour rappeler que j'ai le droit de changer d'avis sur tout sujet, à tout moment, et sans prévenir qui que ce soit : donc un billet de blog écrit à l'instant T ne reflète que mon opinion à l'instant T (et même à l'instant T je ne considère pas qu'ils m'engagent à quoi que ce soit).
[#3] Comme celle consistant à confondre les IA textuelles (LLM) et les IA génératrices d'images ou vidéos (diffusion stable) et d'appliquer aux unes des arguments qui ne valent que pour l'autre. Ou d'utiliser des chiffres bidon ou des comparaisons complètement dénuées de sens sur la consommation d'énergie. Ou de se découvrir une soudaine passion pour la propriété intellectuelle et les sites fermés juste parce que ce sont des armes commodes contre les IA.
[#4] Pour être bien clair : on peut tout à fait pointer du doigt les gens qui manquent à leurs responsabilités (par exemple reproduisent une hallucination d'IA sans avoir rien vérifié, ou transmettent des informations confidentielles à un LLM et donc à la boîte qui le fait tourner), mais le problème n'est pas spécifiquement l'usage de l'IA : il faut séparer le reproche d'avoir utiliser une IA de celui d'avoir manqué à ses devoirs (comme celui de vérification). Ceci est à plus forte raison le cas pour un utilisateur institutionnel. Mais pour l'utilisateur lambda d'un LLM pour son usage personnel, je pense que culpabiliser n'a aucun sens : il faut plutôt éduquer pour faire comprendre les risques, les limites, les problèmes, etc. Le problème n'est pas d'utiliser une IA, c'est d'avoir la paresse d'essayer de comprendre ce qu'elle a répondu, de l'analyser de façon critique, de se rappeler qu'elle peut halluciner sur tout et à n'importe quel sujet (mais que ça ne la rend pas forcément inutile pour autant) ; le problème quand on copie-colle une sortie d'IA, ce n'est pas l'IA, c'est le copier-coller.
Full disclosure, donc : j'utilise moi-même
occasionnellement des IA (mais je n'ai pas payé
d'abonnement, donc essentiellement les versions gratuites) ; et je les
ai trouvé utiles pour certaines
tâches[#5][#6].
Pour l'instant, pour la réflexion mathématique, je les ai trouvées
totalement inutiles à part comme une sorte de moteur de recherche
amélioré (je sais qu'il y a un argument standard qui
dit X, est-ce que tu peux me retrouver l'argument, la
référence ou le mot-clé ?
).
[#5] Principalement
trois types de tâches : relire un texte que j'ai écrit (au
minimum pour trouver les fautes de frappe ; beaucoup de remarques sont
complètement connes, mais on peut juste les
ignorer), retrouver quelque chose à quoi je pense et que j'ai
sur le bout de la langue ou sur quoi je n'ai que de vagues indices (la
réponse sera souvent hallucinée, mais ce n'est pas grave, si le bon
truc est trouvé on peut vérifier), et expliquer comment faire
certaines choses, surtout en informatique (où on a affaire à des docs
complètement pourries que je n'ai pas envie de passer des heures à
lire, donc je demande à un LLM comment je fais
<truc> ?
, il me produit une ligne de commande, et je vérifie
ensuite en lisant juste la partie de la doc qui concerne le bout de
ligne de commande qu'il a produit), mais j'ai aussi, par exemple,
récemment demandé à ChatGPT de m'expliquer et me
décortiquer la structure d'une phrase de Thucydide que mes
connaissances limitées du grec ancien ne suffisaient pas à me
permettre de comprendre même avec la traduction.
[#6] Je précise que je ne fais ni écrire ni relire mes billets de ce blog pas des IA. Les faire écrire par des LLM serait complètement stupide parce que leur fonction même est de m'aider à structurer ma pensée, donc ça défeaterait le purpose comme on dit. Je suis éventuellement parfois tenté de les faire relire (cf. la note précédente), au moins pour m'éviter des fautes embarrassantes, mais en général quand j'ai fini de rédiger j'en ai tellement marre que je ne veux plus rien avoir à faire avec le billet, et certainement pas ajouter une étape supplémentaire de relecture et de prise en compte des suggestions de l'IA (et de décision desquelles prendre en compte). Et pour ce qui est des fautes de frappe dont mes billets sont truffés, j'ai de toute manière des petits lutins (humains, probablement) qui viennent me les signaler dans les commentaires. Bref, 100% des conneries du présent billet sont le résultat de ma stupidité naturelle, garanties sans aucune assistance d'hallucination de LLM.
Assez parlé de l'IA en général, ce n'est pas mon sujet du jour. Je veux parler spécifiquement de la situation vis-à-vis des mathématiques.
☞ Pourquoi c'est difficile à évaluer
Mais si j'ai rappelé le contexte général, et notamment la polarisation des opinions autour de l'IA en général, c'est parce qu'il faut que je souligne le phénomène suivant : notre position politique sur l'IA va forcément influencer fortement notre jugement sur les capacités des IA. C'est impossible de nier que nous soyons tous largement de mauvaise foi à ce sujet : si on pense que le développement des IA est nuisible à la société. (Cf. ce post qui montre un graphique dont les données sont tirées de cet article sur le jugement porté sur des poèmes écrits par des LLM et par des vrais poètes humains : ce qui m'intéresse ici n'est pas tant le fait que les volontaires préfèrent les poèmes écrits par des IA à ceux écrits par des humains ; c'est surtout que, quel que soit la nature de l'auteur, si on leur dit que c'est écrit par une IA ils aiment significativement moins. Ou, de façon moins significative mais amusante, ce post qui montre des réactions face à un vrai tableau de Monet de gens à qui on a dit que c'est une production d'IA, et qui expliquent toutes sortes de raisons pour lesquelles le tableau est très mauvais.)
Ce n'est pas pour rien qu'on teste les médicaments à l'aveugle, et même en double aveugle, et dans le cadre d'un protocole scientifique précis où on a décidé à l'avance ce qu'on devait tester et où on doit signaler les résultats négatifs. Et aussi, on doit signaler qui a payé pour l'étude, et ainsi de suite. C'est la base de la recherche d'impartialité dans la méthode scientifique.
Or quand on cherche à évaluer le niveau des LLM actuels en maths… on a des résultats assez différents selon la manière dont on s'y prend. Un premier problème est que nous n'avons, pour commencer, aucun moyen scientifique de mesurer la difficulté d'une question de maths. Un deuxième est que nous n'avons pas non plus vraiment de moyen de mesurer le succès. Et un troisième est que nous n'avons pas vraiment idée de quels sont les paramètres qui vont jouer.
☞ Les LLM producteurs de preuves bidon
Comme je l'ai dit plus haut, j'ai occasionnellement demandé à
des LLM ce qu'ils pensaient de telle ou telle question de
maths : pour l'instant, les seules situations que j'aie
personnellement rencontrées où ils m'ont répondu quelque chose
d'utile, c'est par une référence directe à la littérature (en
gros : oui, il y a un théorème bien connu qui dit
ceci-cela
[#7]) ; donc comme
une sorte de moteur de recherche pour toute la littérature
mathématique. Mais quand j'ai présenté un vrai problème non-évident
sur lequel chercher, j'ai toujours eu une réponse très assurée,
superficiellement plausible, et en fait complètement bidon. (Pour
donner juste un exemple avec un exercice de
calculabilité, voici
une conversation avec la version gratuite de ChatGPT en
mode réflexion, où il commence par me faire une réponse complètement
bidon utilisant un classical recursion-theoretic
fact
qui est tout simplement faux et stupide, puis je lui demande
s'il est sûr, et il a passé plein de temps à réfléchir juste pour
trouver sa faute.)
[#7] Bien sûr, je vérifie ensuite que le théorème dit bien ceci-cela, parce que le modèle peut parfaitement halluciner, mais à ce niveau-là ce n'est pas grave parce que ça se vérifie facilement.
Et visiblement je ne suis pas le seul dans cette situation, parce que MathOverflow reçoit plein de réponses générées par LLM qui semblent superficiellement plausibles quand on ne va pas vérifier très attentivement ligne à ligne, et qui contiennent, en fait, des erreurs fondamentales. (Pour l'instant, c'est l'effet le plus visible par moi de l'IA sur les maths.)
Je peux aussi lier cette étude intéressante qui a demandé à divers LLM de prouver des résultats subtilement faux, et qui a noté combien ils prétendaient y arriver : c'est assez mauvais (le meilleur modèle accepte encore de « prouver » des choses fausses dans 61% des cas).
Un souci est que ces erreurs d'IA ne sont pas
faciles à détecter parce qu'elles ne ressemblent pas trop aux
erreurs que font des humains ; enfin, si, mais pas aux humains qui ont
le niveau d'expertise et d'intuition suggéré par le ton du discours
général. Nous avons l'habitude de penser oh, cette personne sait
visiblement bien de quoi elle parle
et ne pas vérifier tout : même
en mathématiques, on a tendance à faire confiance à la bonne foi des
auteurs sur certains
points[#8].
Les LLM vont, par exemple, souvent utiliser un théorème
en omettant de vérifier ses hypothèses (peut-être parce qu'ils
reproduisent des textes d'apprentissage où on n'a pas vérifié les
hypothèses parce qu'elles sont évidentes d'après le contexte) : je ne
dis pas que ça n'arrive jamais aux humains, ça, mais un expert qui a
l'habitude, et ça se voit d'après son ton, de faire appel au théorème
schmurz ne va pas se tromper sur les hypothèses du théorème schmurz,
parce qu'il a un bon modèle mental de comment le théorème schmurz
s'applique.
[#8] L'exemple plus
évident est quand quelqu'un écrit un calcul évident montre
ou
bien un résultat standard affirme que
ou à plus forte raison
quand il cite une référence : très souvent, on ne vérifie pas, parce
qu'on suppose implicitement que la personne qui écrit
est faillible mais de bonne foi (donc que le calcul facile
marche bien comme annoncé, que le résultat standard est bien standard,
ou que la référence soutient bien le théorème cité).
Les LLM peuvent complètement bidonner tout ça, donc
l'hypothèse qui marchait bien pour les humains (les gens faillibles
mais de bonne foi ne font pas ça) casse, et la vérification devient
beaucoup plus pénible.
Heureusement, les gens qui postent sur MathOverflow ce genre de réponses générées par IA, superficiellement plausibles mais fausses (je suppose pour faire une sorte de social karma farming) ne sont pas subtils, et laissent souvent des tics de langages de LLM en faisant du copier-coller, alors qu'à l'inverse un vrai humain va souvent faire des remarques personnelles que le LLM ne fera pas. Finalement, on arrive à détecter les réponses générées par IA sur des critères de forme (ou de réputation préalable de la personne qui répond) et à les effacer ; mais ce n'est clairement pas un système robuste.
La littérature scientifique de façon générale est en train de se faire noyer par le AI slop, avec des références hallucinées, des arguments bidon, etc. C'est un grave problème, et ça menace la totalité de la science.
Mais le cas des maths, qui m'intéresse dans ce billet, est quand même un peu à part.
☞ Une solution possible : la formalisation des preuves
En principe, en maths, vérifier une démonstration est une tâche automatisable, mais pour ça il faut avoir affaire à une preuve formelle, pas juste une preuve écrite dans un langage naturel (l'anglais, le français…). Expliquons-nous un peu.
Il existe des assistants de preuve (les plus populaires
étant Coq
et Agda,
plutôt spécialisés dans le domaine de l'informatique,
et Lean
plutôt spécialisé dans le domaine des mathématiques classique), qui
sont des outils dans lesquels on peut exprimer des preuves
mathématiques comme des objets informatiques (pas très différents de
programmes, et ce n'est pas un
hasard), que je qualifie de preuve formelle
, et qui à la
fin vous disent oui, c'est bon
, et s'ils le disent alors la
preuve est correcte[#9].
Convertir une preuve informelle (écrite en langage naturel, par
exemple par des humains) en preuve formelle est faisable par un
humain, mais c'est souvent fastidieux, et surtout, pour que ça marche,
il faut que tous les ingrédients préalables de la preuve (les
théorèmes utilisés) aient eux-mêmes été formalisés. C'est une
opération de traduction, et on peut espérer la confier à
un LLM (technologie, à l'origine, développée pour ça) :
la beauté de la technique est que ce n'est pas grave si
le LLM hallucine en formalisant la preuve : soit il
produit quelque chose de correct, que l'assistant de preuve accepte,
et alors peu importe que la preuve formalisée ne soit pas exactement
celle qu'on lui a demandé de traduire, tant qu'elle est bonne, soit il
produit quelque chose de faux, et l'assistant de preuve va refuser, et
alors on engueule le LLM et on lui fait recommencer.
Bref, formaliser les preuves par des LLM est une
opération parfaitement sensée, et exactement le genre de choses
auxquelles ils sont censés servir.
[#9] Modulo,
évidemment, des bugs dans l'assistant de preuve (conduisant à la
possibilité de prouver ‘⊥’, c'est-à-dire une absurdité). Mais ce
serait difficile d'exploiter ce genre de bugs et de faire
simultanément une preuve crédible. Si l'IA (supposée non
malicieuse) produit une preuve utilisant un bug de l'assistant de
preuve, ça va se voir comme le nez au milieu de la figure (à moins
qu'elle essaie de le cacher, mais on ne voit pas pourquoi elle ferait
ça, du moins tant que le processus d'entraînement n'est pas
entièrement automatisé autour du but faire dire oui à l'assistant
de preuve
).
C'est d'ailleurs sur cet aspect-là des maths que j'avais le plus d'espoir en l'IA : non pas pour trouver des nouvelles preuves mais pour vérifier formellement les preuves existantes (parce que, je répète, faire ça à la main est possible, mais fastidieux).
Mais ce n'est pas vraiment ce qui s'est passé : on a développé des LLM capables de générer des preuves (parfois bidon) plus vite qu'on a développé des LLM capables de convertir les preuves en preuves formelles pour vérification par un assistant de preuve. Autrement dit, on a automatisé une partie intéressante des maths plus vite qu'une partie fastidieuse : c'est très con, ça. (Ça me fait penser à cette remarque selon laquelle les IA actuelles sont en train de décharger les humains de tout ce qu'il y a d'intéressant et de créatif dans la vie pour les laisser se concentrer sur le fait de faire la vaisselle et le ménage, ce qui n'était pas vraiment un super plan.)
Mais bon, maintenant ça marche quand même un peu. J'ai un collègue qui donne à un LLM[#10] divers problèmes à formaliser en Lean, et qui a par exemple formalisé les réponses (elles-mêmes trouvées[#11] par l'IA) au concours d'entrée des ENS Ulm et Lyon en 1995. Apparemment ça a pris deux jours, mais il y est arrivé. Pour les non spécialistes, soyons bien clair si je ne l'ai pas été avant : si l'IA a produit une preuve formelle en Lean et que Lean l'accepte, la preuve est correcte ; il n'y a pas de pipo ou d'hallucination possible quand l'assistant de preuve valide la preuve. (Il faut quand même que l'humain vérifie que la preuve prouve bien ce qu'elle prétend prouver, parce que parfois l'énoncé formel ne coïncide pas avec l'énoncé qu'on prétend avoir prouvé et c'est une source d'arnaques qui demeure, mais c'est nettement moins compliqué de vérifier l'énoncé final que vérifier la preuve complète.)
[#10] Je crois qu'il préfère qu'on ne dise pas lequel. Mais je vais revenir sur la question de la compétence de différents modèles.
[#11] Cette partie-là n'est pas forcément très impressionnante parce que les questions sont assez classiques dans la littérature mathématique (cf. ici), et probablement corrigées sous une forme ou une autre même si on ne semble pas trouver un corrigé intégral en ligne tel quel.
Seulement voilà, même si formaliser les mathématiques est un but louable et que j'approuve totalement (que ce soit fait par des humains, par des IA ou par une combinaison des deux), le fossé séparant le niveau de maths qu'on arrive à formaliser et le niveau de maths dans lequel on arrive à raisonner en langage naturel, ou simplement la quantité de résultats formalisés et ceux prouvés en langage naturel, est énorme. Donc : si la prolifération de preuves bidon produites par des IA incompétentes oblige à passer la totalité des maths en langage formel (y compris pour les preuves prétendument produites par des humains parce qu'on ne peut plus jamais en être sûr), ce sera un recul énorme de nos capacités.
C'est là la première menace que je vois que les IA font peser sur les maths : nous noyer sous les preuves bidon mais superficiellement plausibles, rendant le processus de vérification actuel[#12] intenable, et que le processus de formalisation reste trop peu pratique[#13].
[#12] Rappelons que quand on soumet un article à un journal de maths, il est envoyé à un relecteur (anonyme), qui doit décider si le contenu de l'article est intéressant, correct et nouveau. Évidemment, le relecteur a le droit de se faire aider par un LLM (mais l'obligation morale de ne pas se défausser de sa responsabilité dessus) ; mais comme le travail de relecture n'est pas rémunéré, on peut se demander qui paierait pour ce LLM. Et les LLM ne brillent pas forcément, tant qu'on ne leur demande pas de formaliser les preuves, pour la détection d'erreurs.
[#13] Il n'y a pas que
l'aspect pratique, d'ailleurs, il y a aussi que les maths formelles
apportent avec elles toutes les emmerdes du monde de l'informatique :
chaos des langages (on ne peut pas mélanger des preuves formelles pour
divers assistants), incompatibilités de versions, changements
d'API, commentaires désynchronisés du code, noms mal
choisis, etc. Ce n'est pas avec enthousiasme que j'envisage les
problèmes du style oh la preuve marchait avec la version
4.6.3-beta4 de la cohomologie étale, mais elle a cassé avec la version
4.6.3-final à cause d'une différence d'ordre des hypothèses dans le
théorème de changement de base propre
. D'un autre côté, la
situation actuelle avec des oui, telle qu'elle est écrite la preuve
est incorrecte, mais Gabber a expliqué à la fin d'un séminaire comment
on pouvait la réparer en éliminant l'hypothèse que S est
localement de présentation finie, donc en fait ce n'est pas grave
qui arrive même sans que les IA viennent foutre leur
propre merde.
☞ Your Mileage May Vary
La prolifération des preuves fausses et les emmerdes qui viennent avec, c'est la menace qui vient des IA médiocres. Maintenant venons-en au problème venant des IA (trop ?) compétentes.
Parce que comme je l'ai dit plus haut, moi, personnellement je n'ai jamais réussi à obtenir d'un LLM un résultat mathématique intéressant autrement qu'une sorte de recherche de la littérature (ce qui n'est pas rien). Mais manifestement, tout le monde n'est pas dans ce cas.
Le souci, comme je le disais plus haut, c'est que le niveau des IA en maths est quelque chose qui fait intervenir plein de paramètres : qui évalue, ce qu'on évalue, comment, quel modèle, avec quel protocole, etc. C'est donc très difficile d'avoir une vue d'ensemble. Qu'est-ce qui explique cette différence d'expérience ?
Quand je dis à des fans d'IA que j'obtiens, moi, des
résultats très décevants, on m'explique que j'utilise le mauvais
modèle (il faut utiliser Claude, pas ChatGPT
ou
vice versa, il faut utiliser la version 42.1729
, il faut
utiliser le modèle Truc en mode Machin
, etc.). Sans doute ne
suis-je pas en droit d'attendre des miracles d'une version gratuite
(mais même les versions gratuites, il y a des gens qui prétendent
quand même arriver à leur faire faire des choses utiles, et ce n'est
pas clair d'où vient la différence : des problèmes posés ? de leurs
attentes ? autre chose ?). Mais ce n'est certainement pas avec un
salaire de fonctionnaire en France que je vais pouvoir me payer un
abonnement permettant de faire des tests vraiment significatifs. Ah,
si, mon employeur me fournit un abonnement pro à Mistral, donc j'ai
essayé de lui poser divers problèmes de maths, avec des résultats tout
aussi décevants : je suppose que les fans d'IA vont
m'expliquer que Mistral est à la traîne. Avec eux il faut toujours
utiliser un modèle différent ou une version différente.
Bref, mener des expériences sérieuses coûte cher, trop cher.
☞ Les grandes annonces publicitaires
Alors ce qu'on a à la place, ce sont des annonces spectaculaires, qui sont des opérations de pub des compagnies derrière ces modèles. Comme je le disais plus haut, prendre ces annonces pour argent comptant, c'est l'équivalent de prendre pour argent comptant les pubs des compagnies pharmaceutiques : même quand elles ne mentent pas explicitement, beaucoup de choses ne sont pas dites et peuvent constituer autant de mensonges par omission.
Voici par exemple un compte-rendu de la participation des IA aux dernières olympiades internationales de maths : ce qui a été annoncé fièrement par les compagnies n'était pas exactement faux, mais omettait énormément de contexte important, que ce post de blog raconte. Je pense qu'on a une vision très différente des choses quand on lit ce compte-rendu extérieur que quand on lit les annonces qui ont été faites publiquement par les compagnies derrière cette opération de comm'. Il faut apprendre à exercer le même esprit critique vis-à-vis de toutes les annonces qu'elles font (ou que font les fans d'IA, terme sous lequel je regroupe globalement les gens qui acceptent ces annonces sans esprit critique).
☞ Le unit distance problem a été résolu par OpenAI
Une annonce toute récente au moment (deux jours) où j'écris ce billet de blog est la résolution par OpenAI d'un problème ouvert assez célèbre : le unit distance problem d'Erdős. Il faut que j'en parle un peu longuement.
☞ Un peu de contexte
Un peu de contexte mathématique à ce sujet (les non-mathématiciens
peuvent se contenter de survoler ce paragraphe). En gros, on veut
considérer n points dans le plan et on essaye de les
arranger pour avoir un nombre maximal de paires de points qui soient à
distance exactement 1 : combien peut-on en faire pour n
grand ? (Par exemple, vous pouvez arranger vos points selon une
grille carrée de côté 1, ce qui vous donne grosso modo deux fois plus
de paires de points à distance 1 — les arêtes des carrés — qu'il y a
de points. En gros, on se demande si on peut faire significativement
mieux.) ❧ C'est Erdős qui a formulé cette question (il considérait ça
comme un de ses problèmes ouverts préférés), et il semblait assez
fermement convaincu que la réponse était qu'on ne peut pas faire mieux
que n1+o(1), ce qui signifie qu'il conjecturait
que pour tout ε>0 il existe n₀ à partir
duquel tout ensemble de n≥n₀ points dans le plan
a moins que n1+ε paires à distance 1.
Il est trivial qu'il en a toujours moins de n2
(puisqu'il y a moins de ce nombre de paires tout court), il n'est pas
très difficile de prouver la borne O(n3/2)
(référence : Erdős, On
Sets of Distances of n
Points
, Amer. Math. Monthly 53
(1946) 248–250, théorème 2), et la meilleure borne connue est
O(n4/3) (Spencer, Szemerédi,
Trotter, Unit Distances in the Euclidean Plane
,
in: Bollobás (ed.), Graph Theory and Combinatorics
(London 1983) (Academic Press, 1984)). ❧ Ce qu'a démontré le
modèle d'OpenAI, c'est qu'il existe ε>0 tel
qu'on peut construire un ensemble de n points, pour
des n arbitrairement grands, ayant au
moins n1+ε paires à distance 1.
(Donc Erdős avait tort dans sa conjecture. C'est un point
significatif pour juger ce résultat.) Digression : je me suis dit
que, comme le résultat est explicite, ça pourrait être intéressant de
tracer comme illustration un ensemble de points ayant « beaucoup » de
paires à distance 1, puis j'ai vu que la preuve donne ε
valant quelque chose comme 6×10−38 (mais voir aussi
la note #18), donc, non, je ne
vais pas vous tracer ça, en
fait[#14].
[#14] Mais si vous voulez quand même une image de ce à quoi ce genre d'arrangement peut ressembler, le post d'annonce d'OpenAI a un exemple (lien direct). Il faut juste ajouter la précision que l'unité de distance n'est pas le pas de la grille comme on pourrait se l'imaginer : le pas de la grille vaut 1/√65 ≈ 0.124. Sur cet exemple, on a n = 16² = 256 points, et 912 paires de points à distance 1 (c'est-à-dire environ n1.229), à savoir celles sont les deux paires de point sont à (±1,±8) pas ou bien (±4,±7) pas de la grille.
Évidemment, cette annonce fait beaucoup de bruit. Et il ne faut
pas minimiser : jusqu'à avant-hier, les IA
n'avaient donné aucun résultat nouveau significatif aux mathématiques
— c'est donc une première. (Il y a évidemment une part de
jugement subjectif dans ce que significatif
veut
dire[#15], mais je pense que
c'est un résumé honnête.) On a cru les voir résoudre certains
problèmes ouverts (dont des problèmes
d'Erdős[#16], justement), mais
en fait il s'est avéré que les preuves trouvées par l'IA
étaient essentiellement des preuves déjà trouvées et publiées par des
humains (donc essentiellement régurgitées par le LLM,
bien sûr sans dire d'où elles venaient), et que les gens qui les
avaient publiées ne savaient pas qu'ils résolvaient un problème que
d'autres considéraient comme important. (Il ne faut pas s'imaginer
qu'il y a un grand répertoire centralisé de tous les problèmes ouverts
en maths et qu'on pioche dedans pour décider quoi chercher !)
[#15] À mes yeux, la construction du contre-exemple au unit distance problem qu'a donné le modèle de OpenAI est assez comparable en importance, en thématique et en direction (quoique pas dans ses techniques) au progrès réalisé en 2018 par Aubrey de Grey sur le problème de Hadwiger-Nelson en montrant l'existence d'un unit distance graph qui ne soit pas 4-coloriable (dans le même langage, le résultat d'OpenAI est que pour un certain ε>0 il existe des unit distance graph ayant un nombre n de sommets arbitrairement grands ayant au moins n1+ε arêtes). C'est surprenant, ça montre qu'on avait une mauvaise intuition sur les unit distance graph (dans le sens qu'ils peuvent être nettement plus denses qu'on l'imagine naïvement), mais en fait ça n'améliore pas vraiment notre compréhension de ces graphes. Ça reste un résultat significatif, qui aurait pu être publié dans un excellent journal. (Je crois que le résultat de de Grey n'a jamais été publié au sens formel, parce que ça ne l'intéresse pas ; et le résultat d'OpenAI ne le sera probablement pas non plus pour des raisons analogues.)
[#16] Une question qu'un regard critique doit amener à se poser est naturellement : pourquoi cette focalisation sur les problèmes d'Erdős ? Une réponse possible est qu'ils sont assez célèbres, bien catalogués et raisonnablement nombreux (Erdős était grand collectionneur de problèmes ouverts). Mais une autre est qu'ils sont thématiquement orientés, ne couvrant pas (ou couvrant au mieux de façon très inégale) le spectre des thématiques de recherche des mathématiques : au minimum, on peut dire qu'ils surreprésentent largement la combinatoire, la théorie des graphes, la théorie des nombres « élémentaire » / combinatoire / additive, éventuellement la théorie descriptive des ensembles ; au détriment de sujets tels que : la géométrie différentielle, la topologie algébrique, l'algèbre commutative, l'analyse complexe, l'analyse fonctionnelle, la logique. Tout ça n'est pas un reproche — c'est ce qui intéressait Erdős et c'est son droit le plus strict. Mais ces sujets sont aussi représentatifs d'un certain style de problèmes et de raisonnements (on pourrait dire, très sommairement, que les solutions vont avoir tendance à faire appel à des astuces plus qu'à des grands programmes de recherche, et souvent des outils peu « sophistiqués »), qui va du coup orienter l'appréciation qu'on fait de la compétence mathématique, tant des LLM que des humains, si on utilise spécifiquement cette aune de mesure. Encore une autre chose à noter est qu'Erdős fait partie de ces gens qui ont une sorte de fan-club mathématique autour d'eux (que je trouve personnellement assez agaçant et surtout, là aussi, thématiquement problématique : chacun a le droit d'admirer qui il veut, mais le fait qu'on rencontre beaucoup plus de fans d'Erdős que, au pif, de Weyl, pour prendre quelqu'un d'autre qui a été très touche-à-tout, ne me semble pas représentatif de l'importance de leurs contributions relatives aux mathématiques).
Là la situation est différente : le unit distance problem était suffisamment célèbre pour qu'on puisse être raisonnablement convaincu que ce n'est pas imaginable qu'un humain l'ait résolu sans s'en rendre compte et que le LLM aurait juste reproduit sa preuve. Donc c'est au minimum à prendre très au sérieux. Il faut aussi que je dise clairement que la preuve a été vérifiée (pas formellement en Lean, mais soigneusement par des humains, qui l'ont analysée en détails et qui comprennent très bien les choses, cf. plus bas) : on n'a pas affaire à une preuve bidon.
☞ Tout ce qu'on ne nous dit pas
Mais ça reste une opération de comm' de la part
d'OpenAI, et il faut exercer son esprit critique. Ils
nous disent un certain nombre de choses, par exemple qu'il s'agit
d'un LLM (i.e., un truc qui raisonne en langage humain
naturel), pas un modèle qui raisonne de façon formelle ; que c'est un
modèle interne
(whatever that may mean,
mais en tout cas pas le ChatGPT auquel le commun des
mortels a accès[#17]) ; et
qu'on lui a donné un prompt lui donnant pour instruction de résoudre
ce problème, sans lui donner de consigne ni d'indication qui puisse
l'aider (le prompt exact est reproduit dans l'article, ainsi que la
sortie brute du modèle ; on nous donne aussi une version reformatée du
« processus de pensée » du modèle, ce qui est indiscutablement
intéressant quand on connaît le sujet).
[#17] Il y a un type sur Twitter qui prétend avoir fait reproduire à ChatGPT 5.5 Pro la preuve en question, mais quand on regarde dans l'échange, on voit qu'il a donné plein d'indications au modèle, en gros les indications que Gowers estime (dans ses remarques sur la preuve) être suffisantes pour un humain pour pouvoir la reconstruire (à commencer par : cherche un contre-exemple, ce qui est peut-être déjà suffisant en soi). Ceci dit, si on arrive effectivement à faire produire la preuve par ChatGPT dans son incarnation publique actuelle, c'est peut-être un signe qu'en fait c'est juste ce problème précis qui était beaucoup plus facile qu'on croyait, parce que ChatGPT dans son incarnation publique actuelle on a beaucoup de signes qu'il est globalement très médiocre pour faire des maths utiles, et pas beaucoup de signes de gens qui en ont fait quoi que ce soit de vraiment utile.
Mais il a aussi un certain nombre de choses que OpenAI ne nous dit pas. Notamment : comment ont-ils choisi ce problème ? (Pour sa célébrité ? Sa facilité potentielle pour leur modèle ?) Combien d'autres problèmes ont-ils essayé de faire résoudre à ce modèle, sans succès ? Comment ce modèle a-t-il été entraîné ? Combien de temps (ou de tokens de réflexion) ça a pris et sur quel matériel ? Combien ça a coûté ? Combien ça a consommé d'énergie (juste pour la réflexion, je ne parle pas de l'entraînement) ? Et quelque chose d'autre que je trouve important : puisque apparemment ils ont lancé le modèle plusieurs fois, avec différents temps de réflexion en mesurant la probabilité de succès (il y a un graphique sur leur post d'annonce, dont l'abscisse et suspicieusement dénuée d'unités), on aimerait savoir : est-ce que les réponses correctes trouvées sont toutes la même, ou est-ce que le modèle trouve une preuve différente à chaque fois ?
Le silence sur chacune de ces questions est extrêmement suspect : on doit supposer le pire à chaque fois, parce que si c'était dans leur intérêt de donner des informations ils le feraient. (Notamment, leur silence sur le temps ou la puissance de calcul est très éloquent.)
Donc je dirais qu'il faut prendre cette annonce un peu comme quand une compagnie pharmaceutique prétend avoir guéri quelqu'un d'une maladie jusqu'à présent incurable : c'est sans doute significatif, ça mérite de l'attention, mais on demande à voir plus d'études, faites par des gens qui n'ont pas de conflit d'intérêt — une annonce comme ça, avec aussi peu de détails techniques, c'est juste une pub.
☞ Pourquoi l'IA a réussi là où les humains ont-ils échoué ?
Pour juger les choses, il faut notamment aussi examiner la difficulté de cette preuve et la raison pour laquelle les mathématiciens humains ne l'avaient pas trouvée. Je recommande vivement la lecture du document, cosigné par 9 éminents mathématiciens, Remarks on the disproof of the unit distance conjecture (lié depuis le post d'OpenAI, voici un lien arXiv direct pour les flemmards) : certaines de ces remarques sont tout à fait lisibles et intéressantes même si on ne connaît rien aux maths (ou rien à ce problème), et je recommande notamment les remarques de Melanie Wood ; le même document contient aussi une version simplifiée et améliorée de la preuve, faite par ces auteurs humains à partir de la preuve produite par le LLM (là par contre il faut s'y connaître en théorie des nombres pour le lire — mais je veux dire qu'on peut sauter le début si on n'est pas mathématicien).
Je ne sais pas si j'ai grand-chose à ajouter comme remarques personnelles par rapport à ces 9 mathématiciens, mais voici quelques informations. La preuve brute produite par le LLM fait 3 pages, la preuve détaillée produite à partir de là en fait une dizaine, la preuve détaillée simplifiée produite par les mathématiciens (je soupçonne surtout Will Sawin[#18] et Victor Wang, en fait) en fait 4. (C'est cette dernière que j'ai lue, parce que je ne voulais pas y passer la journée.) Ce n'est pas terriblement compliqué au sens où les outils utilisés sont des techniques et théorèmes habituels de théorie algébrique des nombres (corps CM, théorie du corps de classes, théorème de densité de Čebotarëv, inégalités de Minkowski ; le maximum de technicité étant sans doute ce qui tourne autour de l'inégalité de Golod-Šafarevič[#19]). L'approche générale utilisée est une approche qui a déjà été utilisée pour des problèmes analogues. La contribution du LLM réside essentiellement dans deux lemmes (lemmes 2.1 et 2.2 de la preuve simplifiée), assez peu techniques, faciles à démontrer et sans outils compliqués, mais qu'il fallait « penser » à introduire. (La partie difficile de la preuve, donc notamment tout ce qui tourne autour de Golod-Šafarevič, est une technique standard connue des experts.)
[#18] Il a déjà amélioré l'exposant, juste le lendemain de la publication de l'annonce par OpenAI. <U+1F92F SHOCKED FACE WITH EXPLODING HEAD> [Oui, oui, ceci est partiellement une blague : je sais bien qu'il a eu accès à la preuve en avant-première.]
[#19] S'il y a des collègues connaissant un peu de théorie algébrique des nombres mais pas ça et qui veulent en savoir plus : lisez par exemple Koch, Algebraic Number Theory (1997), le théorème 3.78 (p. 180) ainsi que les références de la preuve de celui-ci. (Pour la complétude de mon blog, l'énoncé est : si K est un corps de nombres quadratique imaginaire ayant au moins 6 diviseurs premiers dans son discriminant, alors sa 2-extension maximale non ramifiée est infinie. Au choix des places près, c'est un peu le type de ce qui est utilisé dans la preuve réécrite par les humains du résultat d'OpenAI. La preuve écrite par le LLM directement utilise une tour de 3-extensions, proposition 3.8, au lieu de 2-extensions, mais c'est un peu gratuitement compliqué.)
Disons aussi que la preuve ne contient aucune idée majeure, aucune
construction nouvelle, et rien qui ne paraîtrait,
disons surhumain
de quelque manière que ce soit. Ce n'est pas
juste que les outils utilisés sont assez banals (en gros contenus dans
un cours de M2 de théorie algébrique des nombres — en tout cas celui
que j'ai eu — plus Golod-Šafarevič), mais les techniques ne sont pas
nouvelles non plus. Il reste que personne n'avait pensé à ça.
Pourquoi les humains n'ont pas trouvé ce contre-exemple, donc ?
(Ce n'est pas vraiment pertinent pour le sujet des compétences
des LLM, mais ça l'est pour essayer de jauger la
difficulté du problème.) Une raison importante semble être qu'Erdős
était fermement persuadé qu'on ne pouvait pas faire mieux
que n1+o(1) (et comme signalé dans les remarques
de Bloom, il pensait que le problème serait difficile si c'était
vrai) : donc certainement moins d'efforts ont été déployés pour
trouver un contre-exemple que pour prouver la conjecture (ce qui
aurait sans doute demandé des idées radicalement nouvelles, et ce qui
aurait été beaucoup plus intéressant). Donc en quelque sorte c'est
surtout un échec de notre intuition, mais ce ne sera pas le premier ni
le dernier en maths. L'autre raison (signalée par plusieurs des
commentateurs) est que pour produire le contre-exemple il faut une
connaissance à la fois du problème et des techniques de théorie des
nombres, ce que peu de gens ont, mais le LLM si. Donc là
c'est un échec de notre compartementalisation des mathématiques
(enfin, de la difficulté à tout apprendre à la fois). Et il fallait
aussi avoir l'audace d'essayer de construire des corps de nombre dont
les degrés ne sont pas bornés (techniques utilisées ailleurs, je
répète que le LLM n'a rien inventé, mais qui peuvent
sembler condamnées sur ce problème pour les raisons que Will Sawin
explique dans ses commentaires techniques). Il reste qu'il semble
plausible que si on avait eu l'indication en fait, les
constructions de tours à la Golod-Šafarevič permettent de fabriquer un
contre-exemple au unit distance problem
d'Erdős
, ça aurait été vite plié. Évidemment, des gens ont
certainement eu cette idée, mais pour la mettre en pratique
il faut mettre les mains dans le cambouis d'un certain nombre
d'inégalités avec plein de choses qu'on peut essayer de contrôler à la
fois, et on ne va pas essayer si on n'a pas une bonne confiance dans
le succès ou du temps à perdre. Alors que le LLM peut
essayer très rapidement plein de pistes puisqu'on lui a donné cette
mission précise et cette mission seule.
Donc, pour résumer, le LLM semble avoir battu les humains sur ce problème pour trois raisons principales : il n'était pas influencée par l'intuition d'Erdős, il a une connaissance encyclopédique des mathématiques, et il a une patience inépuisable pour tester les pistes de façon exhaustive combinée à une intention totale de résoudre ce problème et ce problème spécialement. En revanche, pas de trace d'intuition fulgurante, de technique nouvelle, encore moins de génie surhumain (à ce stade).
Voilà en gros comment j'interprète la situation présente. Il ne faut ni surestimer ce résultat (les LLM actuels ne sont absolument pas surhumains[#20] en maths), ni le sous-estimer (ce ne sont pas non plus des perroquets stochastiques comme certains aiment bien dire).
[#20] Ils ont résolu un problème ouvert assez célèbre, mais, soulignons-le, les problèmes ouverts assez célèbres, il y en a plein en maths, et des humains qui en résolvent, ça arrive régulièrement. Donc manifestement, il n'est pas nécessaire d'être surhumain pour résoudre un problème qu'aucun autre humain n'avait réussi à résoudre avant !
☞ Mais à l'avenir ?
Maintenant, comment est-ce que ça va évoluer, et qu'est-ce que ça
implique pour l'avenir des maths ? C'est là que ça devient assez
effrayant. Il y a une possibilité tout à fait crédible que
les IA (qu'il s'agisse de LLM comme
ici, ou de modèles plus formels, ou de combinaisons entre les
deux) mettent tout simplement fin à l'aventure humaine des
mathématiques[#21],
pas tellement parce qu'ils rendraient les humains obsolètes
(c'est une possibilité, mais honnêtement si on me donne un gadget
magique qui produit une preuve super élégante de n'importe quel
théorème, moi je vais m'en réjouir), mais juste en détruisant
les fondements économiques de la pratique de la recherche en
mathématiques ; ou au minimum, que ça conduise à réserver la
pratique des maths aux plus riches, qui pourront se payer l'accès
aux IA deluxe top moumoute.
[#21] Qu'on me
permette l'abus de langage de parler de tuer les mathématiques
(comme dans le titre). Bien sûr que le monde éternel, inchangeant et
parfait des formes mathématiques (si on croit à la philosophie
platonicienne sur ce plan, ce qui est plus ou moins mon cas) ne va pas
être affecté ; et de toute façon, IA ou
pas IA, exactement 0% du paradis platonique des
mathématiques reste accessible à nous depuis cet univers-ci. Mais ce
n'est pas de ça qu'on parle : quand je dis tuer les
mathématiques
, je parle de mettre fin à l'activité humaine qu'est
l'exploration des mathématiques et la découverte de résultats
nouveaux.
Rien n'est certain, bien sûr. On ne peut franchement pas dire si les LLM vont continuer à s'améliorer ou pas. Il est possible, par exemple, qu'ils soient qualitativement limités dans leur pratique des mathématiques par le langage humain qui sert encore fondamentalement à les entraîner (et à communiquer l'intuition, si bien que les modèles formels n'iraient pas bien loin non plus). Il est possible qu'ils soient limités par la disponibilité de textes, par le temps, par l'énergie, ou par le coût économique, de leur processus d'entraînement, ou par le nombre de poids qu'on peut réalistement utiliser dans un modèle. Il est possible qu'ils soient limités par la nature même de leur mode de fonctionnement (et que comme c'est quand même assez proche de celui des humains, ils tombent sur les mêmes limitations que les humains). Il est possible que la difficulté des maths soit tellement binaire[#22] que très peu de problèmes tombent quelque part entre « facilement résolubles » et « essentiellement impossibles » et que toute l'ingéniosité des maths humaines ne soit pas de résoudre les problèmes qui peuvent l'être mais de trouver ceux qui peuvent l'être. Rappelons quand même qu'aucun programme informatique (ou même, en fait, aucun processus physique si on fait des hypothèses modérées sur les lois de la physique) ne peut résoudre n'importe quel problème de maths : ça c'est un théorème[#23] ; ceci étant, rien n'empêche a priori qu'un programme puisse être monstrueusement plus fort que les humains. Il est possible qu'on découvre que les humains sont vachement meilleurs que les IA pour certains problèmes de maths et vachement moins bons pour d'autres (pour d'autres types de tâches, ça semble continuer à être le cas, donc pourquoi pas). Je n'en sais rien. Tout ça est vraiment impossible à prévoir à ce stade : les croyances qu'on peut avoir sur ce que feront les IA de dans 1, 2, 5, 10, 20 ou 50 ans reflètent surtout vos propres désirs ou craintes sur les IA et pas une moindre prédiction sérieuse sur ce que sera la réalité. Mais nous vivons certainement une époque intéressante pour les mathématiques.
[#22] Une analogie serait avec l'usage des calculs dans les résultats mathématiques : il y a plein de problèmes (par exemple en géométrie algébrique, par des bases de Gröbner) qui se résolvent en théorie par un « simple » calcul algorithmique, mais tels qu'en pratique, ce calcul est très souvent « soit très facile soit infaisable dans tout l'âge de l'univers ». Donc avoir un ordinateur plus puissant n'apporte pas grand-chose. À vue de nez, les calculs de géométrie faits par bases de Gröbner ont sans doute progressé dans les années 1990, mais je pense qu'on ne peut pas faire grand-chose de plus maintenant qu'il y a 25 ans. Donc les gens qui auraient prédit que les calculs par ordinateur allaient détruire tout un pan des maths se seraient trompés.
[#23] Ce théorème est d'ailleurs constructif : on peut fabriquer explicitement un énoncé vrai et qu'aucun modèle d'IA actuel n'est capable de prouver. L'ennui, c'est que cette construction explicite incorporerait tous les poids de tous les modèles (puisqu'ils font, en principe, partie de la fonction calculable). Donc en fait ce n'est pas super intéressant : ce serait juste un truc trop gros.
☞ Le scénario des IA surpuissantes pour tous
Disons quand même que je crois très peu au scénario (pas logiquement exclu, certes) où on arrive à des modèles ouverts, relativement petits, capables de tourner sur un téléphone ou un ordinateur portable[#24], et qui résolvent n'importe quel problème de maths beaucoup mieux que n'importe quel humain. Ce monde-là serait certes assez désespérant pour notre ego de mathématiciens humains, mais au moins désespérant de façon satisfaisante[#25] : je ne sais pas ce que je ferais comme métier dans ce monde si on me met au chômage, mais je passerais sans doute plein de temps sur mon smartphone à apprendre des maths de la part de ces IA surpuissantes — parce que fondamentalement, je fais des maths parce que ça m'intéresse, pas parce que c'est mon métier, et ce qui m'intéresse dans les maths, ce n'est pas de les trouver moi-même, c'est de savoir la réponse à plein de questions (dit autrement : ce que j'aime fabriquer, ce ne sont pas des théorèmes, ce sont des définitions). Donc je gagnerais quand même quelque chose au changement. Mais ne rêvons pas : ce n'est très probablement pas ce monde-là qui va se produire.
[#24] Si on croit que les IA vont inévitablement devenir meilleures que les humains sur une tâche donnée (disons, faire des maths), la question se pose : quelle taille de modèle faut-il pour ça ? Si on pense que c'est possible sur un modèle qui tourne sur les serveurs de OpenAI, il n'y a pas de raison fondamentale de croire que ce n'est pas possible sur un smartphone. (Je ne sais pas ce qu'il faut comme ordinateur de 2026 pour être capable de battre les meilleurs grands maître aux échecs, mais ce n'est pas un supercalculateur comme c'était le cas autrefois.) Mais bizarrement, même les fans d'IA ont rarement l'air de croire que ça arrivera à ce point : leur vision mentale de l'IA surpuissante semble être toujours celle où le truc tourne sur un ordinateur d'une grosse compagnie. Je trouve assez bizarres de croire que le seuil est atteignable avec notre technologie actuelle, mais aussi qu'il se situe dans un intervalle logarithmique assez étroit (entre un smartphone et les serveurs de calculs d'OpenAI) : c'est très audacieux de faire des paris sur la complexité de Kolmogorov.
[#25] La principale
raison pour laquelle je l'évoque, c'est pour contrer préventivement
l'accusation oh, les mathématiciens sont jaloux de leur cerveau et
sont blessés dans leur orgueil de ne plus être les plus forts
.
D'abord, quand on fait des maths, on acquiert forcément une certaine
humilité par rapport aux mathématiques : il y a toujours quelqu'un de
plus fort que soi (au moins dans un domaine donné), et il y a toujours
des problèmes qu'on doit accepter qu'on ne saura jamais résoudre (n'en
déplaise
à Monsieur
Hilbert) et, comme je le dis plus haut, ce sera le cas même avec
toutes les IA surhumaines que vous puissez imaginer. (On
ne connaîtra jamais plus que 0% du paradis platonique.) Les maths ont
même un sujet d'étude de ce qu'on pourrait faire avec des gadgets
magiques qui résolvent magiquement toutes sortes de problèmes
mathématiques (et le fait que ces gadgets aient eux-mêmes forcément
des limitations, etc.), j'en ai déjà
parlé. J'ai même
déjà posé
une question sur MathOverflow qui discute essentiellement de ce
que feraient les mathématiciens dans un monde de science-fiction où
ils auraient accès à un gadget magique qui leur dit instantanément si
un énoncé arithmétique est démontrable ou non. Donc ce n'est pas
comme si l'idée théorique d'avoir instantanément la réponse à plein de
questions de maths était quelque chose de détestable à l'esprit des
mathématiciens ! Ce n'est pas un problème d'ego.
☞ Le problème économique
Ce qui va arriver beaucoup plus probablement, c'est que certaines personnes, les happy few, auront accès à des IA deluxe coûtant ¤¤¤[#26] et capables de faire des choses très fortes (quoi exactement, ça reste à savoir) et que le reste de nous, le commun des mortels des mathématiciens, sera profondément dans la merde, et/ou mis au chômage. (Et donc, sans possibilité d'interroger ces merveilleuses IA sur les questions de maths que j'aurais toujours voulu poser.) Le moindre problème auquel on peut s'attendre, c'est que ça va conduire ceux qui ont déjà les meilleurs résultats à réussir à se faire payer l'accès aux meilleures IA qui leur donneront les meilleurs résultats, et ainsi de suite : c'est déjà comme ça que ça fonctionne dans plein d'autres domaines[#27], mais ça ne risque pas de s'améliorer avec les IA très chères. Mais à plus long terme, si en payant dix ou cent fois moins de mathématiciens pour faire la recherche qu'ils font actuellement, avec des IA coûtant très cher mais moins cher que le salaire de tous les mathématiciens actuels, le politique aura vite fait son calcul[#28].
[#26] Le prix actuel
(déjà fort cher) est certainement artificiellement comprimé par
rapport à ce dont ces compagnies ont besoin pour être rentables, dans
l'espoir de créer une dépendance. Il ne faut pas s'imaginer que ça
restera comme ça (je pense que la bulle de l'IA éclatera,
mais il restera des IA, comme il reste des
domaines .com après l'explosion de la bulle dot-com).
Évidemment, on peut espérer que l'accès aux bons LLM
devienne si cher que le salaire d'un mathématicien soit
finalement quand même plus rentable que l'IA censée le
remplacer (et que, du coup, le problème ne se pose pas), mais je ne
compterais quand même pas trop là-dessus. La loi de Murphy prédit que
ça tombera pile au pire milieu possible.
[#27] Les maths ont (ou avaient) ceci de singulier qu'on peut faire des maths avec un papier et des stylos et aucun autre matériel. (C'est sans doute aussi cette frugalité qui explique que le politique tolère une certaine recherche mathématique apparemment peu féconde en retombées économiques : les mathématiciens ne demandent pas un accélérateur de particules de 27km.) Bon, il y a bien quelques problèmes où on a besoin d'un ordinateur pour les calculs, mais finalement pas des masses. Donc si les IA arrivent à rendre les maths coûteuses, ce sera déjà un effet nuisible spectaculaire.
[#28] Les artistes menacés par les IA génératrices d'images peuvent espérer que le public est preneur d'images authentiquement produites par des humains (comme je le disais dans mon billet précédent, toute œuvre d'art est une conversation entre l'artiste et le spectateur, et nous avons encore envie de communiquer avec d'autres humains, comme le suggère l'expérience liée plus haut concernant le jugement sur les poèmes en fonction de si nous les pensons écrits par des IA ou des humains). Ce serait se fourrer le doigt dans l'œil de s'imaginer que qui que ce soit en à quoi que ce soit à faire qu'un théorème soit démontré par un humain (éventuellement on peut avoir envie que la preuve soit peaufinée par un humain, ou exposée par un humain, mais ça ne fera pas un métier en soi).
Et comme, en plus, ce qui compte n'est pas tellement ce que les IA peuvent faire (comme je l'ai dit, mesurer la compétence en maths est assez délicat) mais ce que les décideurs pensent qu'elles peuvent faire, et pensent qu'ils peuvent économiser de l'argent de telle ou telle manière, je pense que je n'ai pas besoin de faire un dessin.
En outre, la grande majorité de la recherche en maths actuelle ne sert à rien directement. Je l'ai déjà dit, mais je me répète : la raison pour laquelle elle existe quand même est qu'on ne peut pas, dans un monde où les maths sont faites par des humains, amputer les maths de tout ce qui ne sert à rien : les mathématiciens communiquent entre eux, échangent leurs idées entre eux, et ont besoin les uns des autres ; très sommairement : les maths pures ne servent à rien directement, mais elles inspirent les maths appliquées, qui servent à quelque chose. Il y a donc une sorte de contrat, pas vraiment explicité et pas vraiment clair, mais néanmoins une sorte de contrat, entre la société et la communauté mathématique, qu'il faut financer un minimum l'ensemble, y compris les maths pures, pour que les maths appliquées puissent exister (et pour que les maths pures soient enseignées, ce qui sert au minimum à donner des cadres mentaux aux étudiants). Les IA ont le potentiel de changer complètement ce contrat : même si on suppose qu'elles arrivent à faire plein de choses, elles ne vont probablement pas réclamer d'elles-mêmes qu'on les fasse tourner sur des problèmes de maths pures pour enrichir leur base de réflexion. Donc même si la disparition des mathématiciens n'entraînera pas forcément la disparition des maths dans la mesure où il y aurait des IA auxquelles on pose des questions de maths, elle peut entraîner celle des maths pures.
Pour dire les choses de façon peut-être plus percutante : s'il y a des IA surpuissantes en maths, et que le politique décide de ne plus payer pour les humains qui ne servent apparemment plus à rien, alors il n'y a plus de mathématiciens humains ; et s'il n'y a plus de mathématiciens humains, il n'y a plus personne pour poser certaines questions de maths à ces IA surpuissantes, à plus forte raison pour les publier et augmenter la base de connaissances de ces IA surpuissantes.
Bref, si les IA qui font des maths s'améliorent significativement (ce qui, je répète, n'est pas du tout une certitude, mais c'est tout à fait possible), je ne vois vraiment pas trop de raison d'être optimiste quant à l'avenir de la discipline.
Et même dans le scénario optimiste où les IA ne rendent pas les humains obsolètes (aux yeux des décideurs) dans la recherche mathématique, la question de savoir comment on les recruterait est aussi très embêtante, parce que la notion de thèse de doctorat devient difficile à maintenir dans un monde où une IA payée à un prix pas totalement inabordable pour certains permet de réaliser des travaux comparables à ce qu'on demande actuellement pour soutenir une thèse. (Même si on suppose qu'on donne accès aux doctorants aux meilleures IA — ce qui soulève la question de qui paye ça et comment — il faut encore trouver moyen comment tester le travail humain isolément. Des séances de questions-réponses lors des soutenances de thèse qui soient vraiment longues et difficiles et discriminantes ? Un travail de contrôle beaucoup plus poussé par les encadrants de thèse de ce que font les doctorants à titre personnel ?)
☞ Conclusion
Pour résumer, je vois deux principales raisons pour lesquelles les IA menacent les mathématiques : d'une part le problème des IA médiocres qui risquent de noyer le système de vérification et de confiance sous les preuves bidon (et que si la formalisation des maths peut servir à les écarter, elle vient avec un coût énorme) ; et d'autre part le problème des IA trop compétentes et accessibles seulement aux happy few, qui attaque l'organisation même de la communauté mathématique (comment maintenir l'équité des moyens ? comment tester les compétences mathématiques ? comment justifier l'existence des maths pures ? comment maintenir les financements d'une communauté humaine des mathématiques ?). Les fans des IA se gardent bien d'aborder ce genre de questions.
Et bien sûr, ces deux principales raisons de craindre les IA, à savoir les IA merdiques et les IA surpuissantes, ne sont pas exclusives : on peut très bien avoir la double peine[#29].
[#29] ChatGPT, trouve-moi
s'il te plaît un équivalent de l'expression le beurre et l'argent
du beurre
, mais en négatif. La drogue et la peine de la
drogue ?
Peut-être que pour finir je devrais citer le dernier paragraphe du billet d'OpenAI annonçant leur résultat, sur la place des humains dans les mathématiques du futur, parce qu'il est très révélateur :
That future still depends on human judgment. Expertise becomes
more valuable, not less. AI can help search, suggest,
and verify. People choose the problems that matter, interpret the
results, and decide what questions to pursue next.
Ça peut sembler partir d'un bon sentiment, mais c'est un bon sentiment exactement aussi faux que quand une grande compagnie écrit, disons, un message en faveur de la diversité pour le mois des fiertés : le passage ci-dessus pue à la fois la langue de bois corporate et d'avoir été lui-même manifestement généré par IA. Ils sont tellement hypocrites dans leur place de l'humain dans la société qu'ils contribuent à mettre en place que même sur une annonce importante de ce style, ils n'ont pas pu trouver cinq minutes de temps d'un humain pour formuler cette partie de leur message. Ça en dit long.