Attento a ciò che desideri: l'oracolo dell'IA e il futuro della matematica

“Risolvi la matematica, risolvi ogni cosa” è lo slogan che sembra fare da eco a ogni problema risolto da un modello linguistico. La matematica astratta, che nella tradizione platonica appartiene al regno delle verità intellegibili, diventa lo strumento di soft power con cui i capitalisti dell’IA rassicurano gli investitori.

A maggio, OpenAI ha annunciato un importante risultato sulla congettura di Erdős sulle distanze unitarie, problema aperto da ottant’anni. A settembre Anthropic ha comunicato che alcuni agenti basati su Claude hanno tradotto in Lean la dimostrazione, già nota, dell’ultimo teorema di Fermat. Pochi giorni dopo, OpenAI ha scritto di aver trovato un controesempio alle equazioni di Navier-Stokes, uno dei sette problemi del millennio; il 6 ottobre ha poi pubblicato su GitHub più di settecento preprint scritti da un modello interno, con progressi dichiarati su centinaia di problemi aperti.

Peccato che, mentre risolvono problemi, i nuovi modelli ne creino altri, di natura diversa.

La comunità matematica aveva già reagito a giugno con la dichiarazione di Leiden, firmata da migliaia di ricercatrici e ricercatori, che chiedeva a chi sviluppa i modelli maggiore trasparenza su dati e metodi. L’11 settembre, tre giorni dopo l’annuncio su Navier-Stokes, venticinque medaglie Fields hanno firmato una lettera aperta intitolata “Un grave disallineamento dell’IA in matematica”.

Come ricorda su Scienza in rete il logico Hykel Hosni, l’automatizzazione del calcolo è stata cercata dai matematici ben prima che nascessero i calcolatori elettronici. Da Leibniz a Hilbert fino a Turing, matematici e logici hanno cercato di sottrarre le dimostrazioni all’intuizione per affidarle al rigore dei passaggi formali.

“Attento a ciò che desideri, potresti rischiare di ottenerlo”, recita un vecchio detto. I matematici stanno scontando il prezzo di un loro secolare desiderio?

Giorgio Venturi, docente di Filosofia della matematica all’Università di Pisa, individua una fonte dell’equivoco: «Queste nuove intelligenze artificiali sono basate su analisi statistiche del linguaggio che hanno poco a che fare con la deduzione logica come i logici l’hanno formalizzata». Da un certo punto di vista, ammette, si può leggere quanto accade come la vittoria tardiva di una matematica ridotta a linguaggio, una manipolazione di simboli capace di risolvere problemi difficili. Ma se questa è una vittoria, non ne ha il sapore. Le reti neurali non operano come i sistemi formali del sogno di Hilbert, forte del motto positivista «noi dobbiamo sapere, noi sapremo».

E invece, dice Venturi, «Non sappiamo esattamente come funzionano queste macchine, perché i modelli linguistici hanno sviluppato capacità deduttive ad altissima dimensione non prevedibili a partire dal modo in cui sono stati costruiti».

Eppure, questi modelli, per strade a noi estranee, alla soluzione dicono di arrivarci. Prendiamo Navier-Stokes. Secondo OpenAI, un modello interno ha coordinato circa diecimila agenti in parallelo che, scambiandosi oltre due milioni di messaggi, hanno generato migliaia di righe di codice. Ci sono volute 88 ore e diversi milioni di dollari. L’output è un testo di 166 pagine in linguaggio umano, sottoposto poi a Lean, un software di verifica formale che controlla la validità logica riga per riga. 

Il risultato annunciato da OpenAI dimostrerebbe che, in presenza di una forza esterna sufficientemente regolare, il moto di un fluido può sviluppare una singolarità in tempo finito. Questa soluzione risponderebbe a due delle quattro varianti che il Clay Institute ha formulato per il problema. Tocca ora agli umani stabilire se l’enunciato formalizzato coincide con quello richiesto per il premio da un milione di dollari, a cui OpenAI ha dichiarato di rinunciare. 

La verifica presenta non pochi ostacoli. Il 6 ottobre Alexander Bastounis, Fabian Circelli e Anders Hansen hanno pubblicato su arXiv un preprint intitolato “Navier-Stokes lost in translation”, in cui mostrano che la versione formalizzata in Lean non corrisponde alla dimostrazione scritta in linguaggio naturale. Secondo gli autori, la formalizzazione ha cioè modificato alcuni elementi matematici rilevanti per far tornare i conti. 

OpenAI ha riconosciuto lo scarto tra le due versioni, precisando che questo non dimostra che una delle due sia necessariamente errata. Individuare la discrepanza, secondo le ricostruzioni, ha richiesto a un gruppo di matematici circa due settimane di lavoro, contro le 88 ore degli agenti e le 17 della formalizzazione.

Il Clay Mathematics Institute, dal canto suo, non ha fretta. Il regolamento prevede che una soluzione sia pubblicata su una rivista con revisione tra pari e che passino due anni dall’accettazione da parte della comunità prima che si riunisca un comitato. Il presidente Martin Bridson ha definito la valutazione «deliberatamente non frettolosa».

Non sono soltanto la lunghezza dei testi o le strategie necessarie per far tornare i conti a rendere tutto ambiguo. Secondo Venturi, c’è un altro motivo: «Esiste tutto un lavoro concettuale, dietro una dimostrazione, che nelle macchine non appare.» E non appare perché non c’è. «La matematica non è soltanto produrre dimostrazioni, o dare la soluzione a un problema,» continua il filosofo, «è costruire le strutture concettuali che permettono di capire non solo che un risultato è vero ma anche perché lo è». Senza queste strutture concettuali, la macchina assume le veci di un oracolo.

Detentore di verità inaccessibili, l’oracolo produce risultati senza padrone, in cui l’autore è uno ed è la macchina stessa. Se la genesi non è rintracciabile, non lo è nemmeno il mittente. Venturi parla di «risposte senza indirizzo»: proposizioni che possono essere corrette ma risultano incomprensibili alla mente umana, che ragiona per cause e giustificazioni, per bellezza e analogie. Senza un legame interno che stringa premesse e conseguenze, non si può accedere alla comprensione.

Per questo, si consola Venturi, i risultati su Navier-Stokes e su Erdős non fanno una teoria: «un conto è trovare un controesempio a un quantificatore universale, l’altro è dare una soluzione che comprende tutti i casi e spiega davvero un ambito.» Costruire una teoria resta, per ora, dominio dei matematici. Chissà per quanto tempo sarà vero.

Un ulteriore problema epistemologico è nella profonda asimmetria tra la capacità di calcolo dei modelli e quella del cervello umano di leggere e comprendere ciò che producono. Mehtaab Sawhney, matematico di OpenAI, osserva che il collo di bottiglia si sta spostando dal generare dimostrazioni all’assorbirle e contestualizzarle. Il rischio, per i matematici, non è tanto l’estinzione quanto il ridursi a digeritori degli output della macchina.

Se la macchina dà la soluzione ma non può produrne il senso, questo resta alla comunità matematica. Ma la comunità poggia su un terreno fragile, e i grandi modelli linguistici rischiano di allargarne le crepe.

Per Venturi la matematica è «una tradizione orale» in cui le dimostrazioni e la loro comprensione sono l’esito di un lungo processo informale fatto di discorsi tra colleghi. «Ed è per quello che i matematici continuano a lavorare alla lavagna, e il relatore di tesi di dottorato è fondamentale.»

Se chi dirige la ricerca resta indispensabile, la fascia intermedia è a rischio: chi contribuisce al lavoro seguendo le direttive può essere sostituito da una macchina. Ma saltando quel percorso, come si formeranno i matematici che dovranno valutare i risultati?

Si aggiunge poi l’interrogativo sulle capacità cognitive del domani. L’IA è diventata un’infrastruttura sociale e i futuri studenti di matematica l’avranno usata per gran parte della loro vita. Avranno le capacità per capire i problemi che la macchina risolve? Quando la calcolatrice fu introdotta negli anni Settanta, si temette una regressione nel calcolo aritmetico. Probabilmente una regressione c’è stata, ma l’impalcatura ha retto, perché alle elementari le operazioni si imparano ancora senza calcolatrice. 

Con i modelli linguistici la situazione si complica. Essi agiscono su problemi complessi, che si affrontano dal dottorato in poi e richiedono anni di allenamento. «Come si fa a tenere lontano uno studente di università o di dottorato da macchine come i dimostratori automatici?» si chiede Venturi. «Se noi distruggiamo una generazione di nuovi matematici, non saranno più in grado di controllare davvero che quello che fa la macchina sia vera matematica».

E poi c’è la questione dei finanziamenti, che determinano la ricerca. L’hype su ciò che le aziende sanno fare potrebbe far credere ai governi che finanziare i dipartimenti sia inutile. Gli stessi matematici potrebbero aver paura a cominciare una ricerca. La matematica è collaborativa e insieme competitiva: c’è chi dedica la vita ad arrivare per primo alla soluzione di un problema, a volte per un premio, spesso per la gloria.

Tristan Buckmaster, della New York University, e Levent Alpöge, matematico di Anthropic, lavorano da mesi sulle equazioni di Eulero, strettamente legate a quelle di Navier-Stokes, servendosi ogni giorno di modelli come Claude e Codex di OpenAI. Il 3 settembre, Buckmaster scopre che alcune informazioni sui loro progressi sono arrivate a OpenAI. Il 7 settembre i due matematici pubblicano i risultati della loro ricerca; appena dodici ore dopo, OpenAI annuncia la propria dimostrazione sulle equazioni di Navier-Stokes.

Anche se la sequenza degli eventi non basta a dimostrare che il risultato di OpenAI derivi dal lavoro dei due matematici, la vicenda ha contribuito a far crescere la preoccupazione.

Nel romanzo di Liu Cixin La foresta oscura, in un universo pieno di civiltà armate chi parla per primo si espone al pericolo, e allora si tace. In matematica, la paura della foresta oscura diventa il timore che le proprie idee vengano usate per alimentare un modello di linguaggio.

Nel contesto della dichiarazione di Leiden, Peter Scholze scrive teneramente che le idee matematiche, come i bambini, vanno nutrite e fatte crescere con calma negli anni. E come non vuole che i suoi figli siano educati da un’IA, così medita le proprie idee senza usarla.

L’IA è tuttavia uno strumento ormai indispensabile per un numero crescente di matematici, soprattutto all’interno di un meccanismo competitivo come il publish or perish che regola le carriere. A vincere nella corsa ai problemi sono i modelli più potenti e più blindati.

C’è chi sceglie di lasciare l’accademia per l’azienda. Il 23 luglio, a Filadelfia, subito dopo aver ricevuto la medaglia Fields, il teorico dei numeri Jacob Tsimerman ha annunciato che sarebbe passato a OpenAI per occuparsi di sicurezza dell’IA. Solo un anno prima aveva firmato un articolo sugli scenari in cui l’IA potrebbe portare all’estinzione umana.

Quello tra industria privata e accademia è il bivio che attende anche i dottorandi e i post-doc, che vedono le università fragili e le multinazionali sempre più forti. 

In passato i minatori portavano nelle gallerie un canarino in gabbia. Il suo sistema respiratorio, molto sensibile, lo faceva soccombere per primo ai gas tossici; al cessare del suo canto, i minatori fuggivano prima che fosse troppo tardi.

Bryna Kra, matematica della Northwestern University e una delle autrici della dichiarazione di Leiden, scrive che la matematica è il canarino nella miniera di tutta la vita intellettuale. La matematica è stata la prima disciplina a essere stravolta dai nuovi modelli di linguaggio. Cosa succederà, si chiede, quando l’IA entrerà con la stessa potenza nel diritto, nelle politiche pubbliche, nell’arte? Il canarino, per ora, canta ancora. La domanda è cosa si può fare per preservare questo canto.