Comments on Sur la destruction des maths par les boîtes d'IA

@Sty, @Ruxor: combien de mois avant que les emplois manuels ne soient eux aussi menacés, par des robots ?

@Ruxor Le point est justement que ce n'est *pas* un argument faible. Ce n'est certes pas le seul argument non plus mais c'est l'un des problèmes centraux, au moins symboliquement.

Si tu veux éviter de provoquer ce genre de discussions pénibles, il y a une solution simple : arrête de policer la façon dont les gens défendent des causes avec lesquelles tu es plutôt d'accord sous prétexte que tu trouves leurs arguments pas assez forts (surtout quand ça résulte d'une incompréhension de ta part).

(Je dois quand même préciser que je suis entièrement d'accord avec le reste de ce que tu dis dans le billet.)

@Ruxor

Tout dépend ce que tu appelles « bienfaits pour l'humanité ». Si l'IA permet de travailler 10 fois moins pour produire la même chose (que ce soit des théorèmes de maths ou des pièces de moteurs électriques), tout le monde (peut-être pas pour les maths, si j'ai bien suivi) va dire que c'est positif. Sauf qu'on va très certainement faire le choix de travailler autant et produire 10 fois plus (ne serait-ce que parce que nos sociétés ne sont pas conçues pour fonctionner sans le travail). Ça n'est pas soutenable sur le plan environnemental.

Il faut aussi s'attendre à ce que l'IA apporte des progrès spectaculaires contre les maladies, infectieuses ou non. C'est objectivement un « bienfait pour l'humanité ». Mais idem, ça s'accompagnera d'une augmentation majeure de notre impact sur l'environnement.

Donc du point de vue environnemental ça n'est pas tellement la consommation énergétique primaire des ordinateurs de l'IA qu'il faut questionner, mais l'impact du développement incroyablement rapide, presque exponentiel, que l'IA est en train de fournir à nos sociétés qui ne savent pas fonctionner de manière soutenable.

>>>Kévin Buzzard avait lancé un vaste projet de recherche récemment sur cette formalisation

Il faut noter que le projet de Buzzard a été lancé essentiellement pour enrichier la bibliothèque de Laan avec des définitions bien propres et mitonnées aux petits oignons. Après tout Mathlib est le socle sur lequel tout repose donc il est important de formaliser ça avec le plus grand soin.
Comme Buzzard le dit, son projet c'est "formalize in a gold-standard way (i.e. suitable for mathlib)".

Le travail qu'à produit Anthropic n'a pas du tout ce but. Il s'agit juste d'autoformaliser la preuve et de profiter de la mousse marketo-médiatique à ce sujet.

Buzzard ne semble pas amer parce qu'il explique bien que son projet à lui n'est pas celui d'Anthropic : "I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway)."

Il y a une chose que l’IA ne sait pas faire : c’est sortir du cadre. De même qu’une calculatrice super puissante ne fera pas de calculs en nombres complexes si elle n’est pas programmée pour, de même qu’un logiciel de géométrie dynamique ne sortira pas du cadre euclidien s’il n’est pas programmé pour, de même une IA ne sortira pas du cadre conceptuel à l’intérieur duquel elle a été entraînée.

La solution est donc de hisser l’ensemble de la communauté mathématique au niveau de Grothendieck, où elle sera totalement à l’abri des assauts de l’IA. 😃

Ne peut-on pas penser que dans 1 ou 2 ans ces entreprises seront passées à autre chose. Et qu'on pourra toujours faire de la recherche nouvelle. On digèrera ce qu'ils ont fait de façon intelligible, puis posera des questions, les IA académiques repondront en partie, etc. C'est la période de transition qui est compliquée.

Merci d'avoir exprimé aussi limpidement ce que je pensais intérieurement de façon plus confuse. Chacun de tes billets est un petit joyau de réflexion, d'originalité, d'humour, de littérature, de philosophie, d'érudition… La lecture de ce blog me procure une joie que jamais une discussion avec un chatbot ne remplacera. Encore bravo pour ton talent et le temps que tu consacres à nous éclairer, et bonne chance pour ces temps à venir qui s'annoncent troubles.

+1 a3nm : voir l'argument écologique sous un angle comptable/utilitariste c'est rater la forêt pour les arbres.

Je me permets de signaler l'Association for Human Mathematics <URL: https://www.ahmath.org/ > et l'essai adjacent "The crisis of AI-generated mathematics" de Max Weinreich.

Mes condoléances aux chercheurs en mathématiques, qui vivaient dans une niche métastable où ils pouvaient vivre de leur passion, dans des circonstances financières il est vrai assez variables. Il demeure vrai que c'est (c'était) un domaine privilégié où des gens essentiellement issus de milieux favorisés pouvaient continuer de s'intéresser exclusivement aux choses abstraites, voire prendre fierté dans la futilité de leur travail, et pourtant gagner de quoi subsister. Cela s'opposait notamment à la situation de la plupart des artistes. Mais j'avoue que mon envie caustique de jouer à comparer les souffrances de chacun se heurte à la réalité d'une IA bientôt superintelligente, déjà terrifiante, qui risque peut-être de provoquer des désastres très directs avant même de mettre tous les travailleurs intellectuels de l'humanité au chômage. Le sort des mathématiciens doit s'ajouter à celui des programmeurs et graphistes pour alerter le reste du monde, pas "on risque de perdre nos emplois à long terme" mais "c'est en train d'arriver là maintenant tout de suite, et dieu sait si on aura le temps de nous réorganiser autour de l'IA avant qu'elle ne mène à notre perte".

Les choses vont tellement vite… Tu as raison de souligner que l'argument anti-slop qui consiste à dire que la formalisation (en Lean notamment) empêcheles dérives (= une avalanche de papiers faux) et qui était sans doute valable il y a quelques mois est complètement mort.

On a complètement sous-estimé la capacité des IA à formaliser, ce qui a l'air d'être devenu une tâche relativement trivial pour elles. L'exemple le plus frappant est Anthropic qui a réussi à formaliser la preuve du théorème de Fermat-Wiles (13,4 millions de lignes de code…) alors qu'en parallèle Kévin Buzzard avait lancé un vaste projet de recherche récemment sur cette formalisation (avec financement !) en pensant que ça allait prendre des années.

Merci pour ce billet de blog qui résume si bien la triste situation dans laquelle nous sommes.

En ce qui concerne le programme de Hilbert, je me disais déjà depuis quelques années (avant que les progrès des LLM en mathématiques ne deviennent aussi spectaculaires) qu’au-delà de la calculabilité, la théorie de la complexité avait elle-aussi une portée assez limitée pour prédire la difficulté *pratique* des problèmes réels, en particulier depuis que les solveurs SAT sont capables de résoudre des instances concrètes avec un nombre de variables qui devrait pourtant les rendre trop complexe *dans le pire des cas*. Clairement, nous ne comprenons pas suffisamment la complexité *moyenne* des problèmes intéressants. Il y a bien une théorie de la complexité-en-moyenne, mais mais une grande partie de ses résultats repose sur des hypothèses ou des choix de distributions qui ne semblent pas nous dire grand-chose à propos de la complexité empirique des problèmes rencontrés à l’état sauvage, pour ainsi dire. (Et les méthodes opaques des boîtes d’IA ne nous en apprennent malheureusement pas davantage ! Il serait intéressant de savoir quels problèmes elles ont essayé de résoudre sans succès, par exemple---ce qu’elles feraient si elles avaient vraiment à cœur de faire progresser les mathématiques et de collaborer avec la communauté scientifique).

Un autre point : ton billet (et nombre d’autres réactions de personnes sensées) explique bien les dommages de l’IA en maths *d’un point de vue interne*, mais on parle assez peu de ce que les maths apportent *d’un point de vue externe*, c’est-à-dire aux autres sciences et à la société de manière générale, et de ce que l’usage des LLM comme ersatz risque de nous faire perdre. Il me semble clair -- pour tout un tas d’arguments que tu résumes bien -- que les LLM et leurs maîtres capitalistes sont un danger pour la discipline. En revanche, dans un contexte où un grand nombre de scientifiques, d’ingénieurs, etc. (sans parler du grand public) ne voient déjà les mathématiques que comme une grosse boîte à outils dans laquelle il faut piocher le bon marteau pour attaquer son problème du moment et en tirer la solution toute faite, les LLM donnent l'illusion d'être un outil généraliste qui permettrait de ne plus s’embarrasser de mathématiques. J’imagine que bon nombre de personnes s’en réjouissent ! Bien sûr, ce n’est pas mon cas---il suffit de constater le grand nombre de résultats bidons (je pense par exemple aux crises de la reproductibilité en biologie, en médecine, en sciences sociales, etc.) dus à la mécompréhension des méthodes statistiques pour se convaincre que le choix du bon outil et son application correcte requièrent une compréhension à laquelle les LLM ne peuvent pas se substituer pour l’instant.

On me répondra que les LLM seront bientôt capables de s’assurer de la bonne application des outils mathématiques à toute question scientifique (!), et qu’il suffira de leur fournir suffisamment de contexte pour qu’ils choisissent et appliquent la bonne méthode. Peut-être… Mais cela me semble être un problème autrement plus compliqué que de produire des démonstrations mathématiques. S’assurer qu’un nombre (ou toute autre abstraction mathématique) ait un sens n’est pas une affaire dont la cohérence peut être vérifiée en Lean ! Il s’agit d’une activité que l’on pourrait qualifier de « méta-rationnelle » ou du moins de synthétique (comme le choix de questions intéressantes en maths d'ailleurs), dont les ressorts restent relativement mystérieux et dont je doute qu’ils soient totalement automatisables ("famous last words" de nos jours, je sais).

Je trouve le billet super intéressant mais il y a juste une distinction qui m'a manqué : quand on dit que sortir une preuve formelle opaque d'un résultat tue la recherche autour de ce résultat, je trouve que ça mélange à la fois (1.) une observation sur ce qui motive intrinsèquement des gens à réfléchir à un problème, et (2.) une observation sur comment la communauté mathématique est structurée actuellement et comment la reconnaissance est distribuée.

Je suis d'accord que (1.) existe : personnellement en tout cas si je réfléchis à un problème et qu'une solution formelle opaque du problème sort alors je ne vais pas être très motivé à continuer à y réfléchir ou à essayer de la décortiquer. (Mais c'est vrai aussi d'une preuve humaine -- à part que vu qu'elle est parfois moins opaque il y a davantage de motivation à comprendre ce que j'avais raté.)

Et je suis d'accord que (2.) ne justifie pas complètement le comportement des boites d'IA : si on prétend faire des maths c'est quand même bien de s'intéresser aux règles de la communauté des matheuxses et à l'impact de ce qu'on fait sur celle-ci.

Mais : je trouve quand même que c'est important de soigneusement distinguer (1.) et (2.). Parce que (2.) c'est quand même quelque chose qu'on peut espérer changer, et qu'on devrait de toute façon changer pour tout un tas de raisons. Et (1.) je trouve que ça mérite d'être examiné : certes l'existence d'une preuve opaque va décourager certaines personnes, mais elle va peut-être aussi en motiver d'autres à déslopifier le slop comme tu dis, ce qui peut avoir un impact positif à terme. Il y a aussi le fait que publier des preuves formelles opaques c'est quand même un peu un victimless crime si on ne regarde pas (2.) : c'est difficile de qualifier en quoi l'existence d'une preuve formelle est quelque chose qui cause du tort à des gens qui réfléchissaient au problème et ne sont aucunement empêchés de continuer à y réfléchir.

Sinon : sur l'empreinte environnementale des LLM, je suis sensible à l'argument mais pas tant pour l'impact marginal (je suis d'accord qu'il est faible) que pour la symbolique de la situation. En gros : sachant qu'on est depuis longtemps sur une trajectoire non soutenable environnementalement, je trouve ça vraiment intolérable de voir l'humanité (en termes d'attention collective, de perception du progrès, et surtout de capitaux) se ruer en courant dans une direction complètement haute qui (en dehors des rêves douteux des AI-optimists) n'aide pas à régler la crise climatique et même l'aggrave sévèrement en terme d'impact global…