La intel·ligència artificial també sacseja les matemàtiques

A la col·lecció del Museu Getty de Los Angeles hi ha un retrat fet al segle XVIII del matemàtic Euclides, de la Grècia antiga, on apareix amb aspecte descurat i les mans brutes, sostenint diversos fulls d'Elements, el seu tractat de geometria. El text d’Euclides ha estat el paradigma d’argumentació i raonament matemàtics durant més de dos mil·lennis.

“Euclides és famós perquè comença amb unes definicions que són gairebé poètiques”, comenta el lògic de la Universitat Carnegie Mellon Jeremy Avigad en un correu electrònic. “Sobre aquest fonament, va bastir la matemàtica del seu temps i va demostrar les coses de tal manera que cada pas es deriva clarament dels anteriors, a partir dels conceptes bàsics, les definicions i els teoremes exposats prèviament”. Si bé hi havia qui denunciava que alguns dels passos “evidents” d’Euclides no ho eren tant, assenyala Avigad, el sistema funcionava.

Al segle XX, però, els matemàtics van deixar de veure amb bons ulls que la matemàtica es basés en aquests fonaments geomètrics intuïtius. Per aquest motiu, van desenvolupar sistemes formals: representacions simbòliques precises i normes mecàniques. Finalment, aquesta formalització va permetre traslladar la matemàtica al llenguatge informàtic. El 1976, el teorema dels quatre colors (segons el qual n’hi ha prou amb quatre colors per omplir un mapa de tal manera que no hi hagi regions adjacents del mateix color) va ser el primer gran teorema a quedar demostrat amb l’ajut de la força bruta informàtica.

La revolució de la IA

Avui dia, els matemàtics s’enfronten a l’última força transformadora: la intel·ligència artificial. El 2019, Christian Szegedy, un informàtic que ha treballat a Google i actualment treballa en una start-up de la badia de San Francisco, va predir que un sistema informàtic igualaria o superaria la capacitat de resolució de problemes dels millors matemàtics humans en qüestió d’una dècada. L’any passat va corregir la predicció per situar la data en el 2026.

Al febrer, Avigad va acudir a un seminari sobre “demostracions assistides per ordinador” a l’Institut de Matemàtica Pura i Aplicada, al campus de Los Angeles de la Universitat de Califòrnia, i l’últim dia de les jornades va aprofitar per visitar el retrat d’Euclides. L’acte va atreure un còctel atípic de matemàtics i informàtics. “Sembla conseqüent”, comenta Terence Tao, un dels matemàtics de la universitat, guanyador de la medalla Fields el 2006 i principal organitzador del seminari.

Tao assenyala que els matemàtics no s’han començat a amoïnar per les possibles amenaces derivades de la intel·ligència artificial, tant per a l’estètica matemàtica com per a ells mateixos, fins fa pocs anys. El fet que hi hagi matemàtics destacats que aborden aquestes qüestions i n’exploren les potencialitats “d’alguna manera trenca el tabú”, diu.

Intel·ligència que demostra

Avui dia, no falten aparells per optimitzar-nos la vida: l’alimentació, el son, l’activitat física. “Ens agrada portar a sobre aparells que ens facilitin una mica encertar en les coses”, diu el matemàtic de la Universitat de Wisconsin-Madison Jordan Ellenberg durant una de les pauses del seminari. Els dispositius que fan servir la intel·ligència artificial podrien fer el mateix amb les matemàtiques, afegeix: “Està molt clar que la qüestió és què poden fer les màquines per nosaltres i no pas què ens faran les màquines a nosaltres”.

Un d’aquests aparells matemàtics s’anomena assistent de demostració o demostrador interactiu de teoremes. L’Automath n’era una versió primitiva dels anys 60. Pas a pas, un matemàtic tradueix una demostració en llenguatge informàtic i, tot seguit, un programa informàtic comprova si el raonament és correcte. Les comprovacions s’acumulen en una biblioteca, una referència canònica dinàmica que poden consultar altres usuaris.

Aquesta mena de formalització serveix de fonament per a la matemàtica actual, comenta Avigad, que dirigeix el Centre Hoskinson de Matemàtica Formal (fundat per l’emprenedor del món de la criptografia Charles Hoskinson), “exactament de la mateixa manera que Euclides mirava de codificar i dotar d’uns fonaments la matemàtica del seu temps”.

Per altra banda, el sistema d’assistent de demostració de codi obert Lean està atraient molta atenció darrerament. Desenvolupat a Microsoft per Leonardo de Moura, un informàtic que actualment treballa a Amazon, Lean es basa en el raonament automàtic a través del que es coneix com a GOFAI o intel·ligència artificial simbòlica, la qual està inspirada en la lògica. De moment, la comunitat de Lean ha verificat un teorema intrigant sobre el capgirament d’una esfera com un mitjó, així com un teorema clau en un sistema per unificar reialmes matemàtics, entre altres projectes.

Des que va assistir al seminari, Emily Riehl, matemàtica de la Universitat Johns Hopkins, ha fet servir un programa assistent de demostració experimental per formalitzar demostracions que havia publicat anteriorment amb un coautor. Al final d’una verificació, comenta: “Tinc una comprensió molt i molt aprofundida de la demostració, molt més que mai. Penso amb una tal claredat que l’hi puc explicar a un ordinador dels més ximplets”.

Converses matemàtiques

Un altre grup d’eines es basa en l’aprenentatge automàtic, que sintetitza quantitats ingents de dades i hi detecta patrons. Tanmateix, no obté bons resultats quan ha d’exercitar el raonament lògic pas a pas. DeepMind de Google dissenya algoritmes d’aprenentatge automàtic per abordar problemes com ara el plegament de les proteïnes (AlphaFold) o guanyar partides d’escacs (AlphaZero). En un article publicat a Nature el 2021, un equip va dir dels seus resultats que “impulsen el progrés en matemàtica guiant la intuïció humana amb intel·ligència artificial”.

Yuhuai Tony Wu, un informàtic que va treballar a Google i ara treballa en una start-up de la badia de San Francisco, planteja un objectiu de l’aprenentatge automàtic més grandiloqüent: “resoldre les matemàtiques”. A Google, Wu va investigar els usos possibles en matemàtiques dels grans models de llenguatge que fan anar els bots de conversa.

L’equip n’utilitzava un model entrenat amb dades d’internet i després perfeccionat mitjançant un gran conjunt de dades amb un alt contingut matemàtic basat, per exemple, en un arxiu en línia d’articles sobre matemàtica i ciència. Quan se li demanava en anglès planer que resolgués problemes matemàtics, el bot de conversa especialitzat, anomenat Minerva, “era molt bo a l’hora d’imitar els humans”, va assegurar Wu al seminari. El model va obtenir millors notes que les d'un estudiant de 16 anys mitjà en exàmens de matemàtiques de secundària.

Wu afirma que, eventualment, s’imagina un “matemàtic automàtic” que tingui “la capacitat de resoldre un teorema matemàtic tot sol”.

La prova decisiva

Davant d’aquestes novetats trencadores, els matemàtics expressen graus de preocupació diversos.

Michael Harris, de la Universitat de Colúmbia, manifesta els seus dubtes al seu Substack titulat Silicon Reckoner. L’amoïna el possible xoc entre els interessos i valors de la matemàtica de recerca i els sectors tecnològic i de defensa. En un butlletí recent, assenyalava que un dels ponents d’un seminari titulat A.I. to Assist Mathematical Reasoning (intel·ligència artificial per assistir en el raonament matemàtic), organitzat per l’Acadèmia Nacional de Ciències dels Estats Units, era un representant de Booz Allen Hamilton, contractista de les agències d’intel·ligència i les forces armades nord-americanes.

Harris lamenta que no es debatin les conseqüències a gran escala de l’ús de la intel·ligència artificial en la recerca matemàtica, especialment “si es compara amb l’animadíssim debat que es manté actualment” sobre aquest tema en “pràcticament qualsevol àmbit, excepte les matemàtiques”.

Geordie Williamson, de la Universitat de Sydney i col·laborador de DeepMind, va intervenir al congrés de l’Acadèmia Nacional de Ciències i va animar els matemàtics i els informàtics a participar més en aquests debats. Al seminari de Los Angeles, va encetar el seu discurs amb una frase inspirada en l’assaig de George Orwell de 1945 La bomba atòmica i vostè. “Atesa la probabilitat que tots en resultem profundament afectats en els pròxims cinc anys —va dir Williamson—, l’aprenentatge automàtic no ha suscitat tant debat com es podria esperar”.

Williamson és del parer que la matemàtica és la prova decisiva per determinar de què és capaç i de què no l’aprenentatge automàtic. El raonament és la quintaessència del procés matemàtic i és el problema crucial i irresolt de l’aprenentatge automàtic.

Al principi de la col·laboració de Williamson amb DeepMind, l’equip va trobar una xarxa neuronal que va predir “una quantitat en matemàtiques que importava molt”, afirma en una entrevista, i ho va fer “amb una precisió increïble”. Williamson es va escarrassar a entendre per què —això serien els elements d’un teorema—, però no en va poder treure l’entrellat. Tampoc se’n va sortir cap treballador de DeepMind. Com Euclides, el geòmetra de l’Antiguitat, d’alguna manera, la xarxa neuronal havia aconseguit discernir intuïtivament una veritat matemàtica, però el perquè lògic resultava indesxifrable.

Al seminari de Los Angeles, un dels temes destacats va ser com combinar la intuïció i la lògica. Si la intel·ligència artificial fos capaç d’aplicar les dues alhora, trencaria totes les previsions.

Tanmateix, observa Williamson, la motivació per entendre la caixa negra que representa l’aprenentatge automàtic és escassa. “És la cultura de l’amateurisme en la tecnologia: si funciona quasi sempre, ja va bé”, comenta. Aquesta opció, però, deixa els matemàtics insatisfets.

Williamson afegeix que mirar d’entendre el que succeeix a l’interior d’una xarxa neuronal suscita “interrogants matemàtics fascinants” i que trobar-hi respostes dona als matemàtics l’oportunitat de “fer una aportació important al món”.