OpenAI ritira tre dimostrazioni dopo un giorno e mette in discussione il patto della matematica

Martedì 6 ottobre è comparso su GitHub un repository di OpenAI, chiamato semplicemente math, che raccoglie 722 manoscritti di matematica ordinati in 372 famiglie di risultati, dalla geometria algebrica fino all'informatica teorica, tutti prodotti da un modello interno che l'azienda non ha rilasciato e di cui non ha voluto rivelare neppure il nome. Meno di ventiquattr'ore dopo tre di quei lavori erano già stati ritirati per un errore, con un'inversione dei ruoli assai rara nella storia delle ritrattazioni scientifiche, dove a fare un passo indietro è di solito un singolo ricercatore finito sotto accusa e quasi mai una delle principali aziende di intelligenza artificiale del mondo. Stando ai dati che la stessa OpenAI ha messo a disposizione, al modello sono stati sottoposti circa quattromila problemi aperti, con una media di tre ore di calcolo di ChatGPT Pro per ciascun risultato, nell'ambito di una campagna avviata, come spiega il repository, quando i test matematici abitualmente usati dall'azienda avevano smesso di offrire una misura utile perché il modello li risolveva tutti. Fra le affermazioni contenute nei manoscritti figurano una dimostrazione della Unique Games Conjecture, che da oltre vent'anni occupa un posto centrale nell'informatica teorica, e una regione libera da zeri valida per ogni funzione L di Dirichlet, mentre nessuno dei lavori tocca i cinque Problemi del Millennio ancora aperti; secondo un portavoce, quasi tutti i risultati sarebbero nati da un unico prompt affidato a un unico agente, e molti di essi non sarebbero ancora stati compresi neppure dai matematici dell'azienda.

Poiché il modello non è accessibile, nessuno al di fuori di OpenAI è in grado di verificare queste affermazioni, ed è per questo che il 29 settembre il gruppo consultivo sulla matematica e l'intelligenza artificiale ospitato dall'Institute for Advanced Study di Princeton aveva chiesto ai laboratori di accompagnare ogni risultato con i prompt da cui era nato e con il relativo costo di calcolo, richiesta alla quale OpenAI ha risposto indicando soltanto una media del calcolo impiegato e diffondendo dieci riassunti abbreviati del ragionamento del modello, senza pubblicare alcun prompt. L'errore, annunciato il 7 ottobre nel registro delle modifiche del repository, consiste in un segno sbagliato all'interno di un manoscritto sull'algebricità delle classi di Weil per certe varietà abeliane di dimensione otto, che invalida un argomento di cancellazione e trascina con sé la costruzione su cui poggiavano altri due lavori, fra i quali quello che affermava la congettura di Hodge razionale per i prodotti di superfici K3. I tre manoscritti appartenevano alla famiglia di risultati legata alla congettura di Hodge, la più osservata dell'intero catalogo, e quello difettoso, datato 18 settembre, era tra i più vecchi della raccolta.

Nello stesso giorno OpenAI ha corretto altri quattordici manoscritti, riparando dimostrazioni e precisando enunciati e ipotesi, e ha aggiornato i riferimenti bibliografici di altri tredici, sicché il catalogo è sceso da 722 a 719 titoli, mentre le versioni ritirate restano consultabili insieme a una nota che descrive la lacuna. Un portavoce ha attribuito la scoperta a un audit interno, senza precisare chi abbia individuato l'errore, e ha assicurato che il processo di revisione, come accade per qualunque manoscritto di ricerca, proseguirà fino al ritiro dei lavori per i quali non si troverà una correzione. A chi solleva dubbi OpenAI risponde di solito richiamandosi a Lean, un linguaggio open source nel quale una dimostrazione viene riscritta in forma rigorosa perché un programma ne controlli ogni passaggio; al momento della pubblicazione, tuttavia, soltanto 162 dei 722 manoscritti avevano il risultato principale formalizzato, e con le aggiunte del 7 ottobre si è arrivati a 300 risultati principali su 719, poco più del 42 per cento, una quota rimasta da allora immutata, dato che il registro delle modifiche contiene ancora quella sola voce e il README ripete la stessa percentuale. L'azienda ammette che alcuni dei risultati non formalizzati potrebbero contenere errori e spiega di aver pubblicato senza attendere la formalizzazione completa su raccomandazione dello stesso gruppo consultivo, benché dal confronto con l'indice del repository risulti che quasi tutto ciò che è stato ritirato o rivisto in modo sostanziale si trovava fuori dalla parte verificata in Lean.

Che anche la parte verificata richieda cautela lo mostra il precedente dell'8 settembre, quando OpenAI aveva annunciato una dimostrazione di 166 pagine sulla formazione di singolarità in tempo finito nelle equazioni dei fluidi, ottenuta da circa diecimila agenti in 88 ore e formalizzata in Lean in altre 17, che riguarda però le equazioni sottoposte a una forza esterna, mentre il Problema del Millennio chiede di trattare il caso senza forzante, motivo per cui il Clay Institute non lo considera risolto. Il 6 ottobre, lo stesso giorno in cui sono comparsi i 722 manoscritti, Alexander Bastounis, Fabian Circelli e Anders C. Hansen hanno pubblicato su arXiv un preprint intitolato "Navier-Stokes lost in translation", nel quale sostengono che la prova formalizzata in Lean non corrisponde alla dimostrazione scritta in linguaggio naturale, la quale affermerebbe più di quanto il codice verifichi, e affiancano a questo caso altri esempi di traduzioni errate compiute da sistemi di intelligenza artificiale, fino a sostenere, sul piano teorico, che garantire la fedeltà di una formalizzazione sia un problema intrinsecamente più difficile del problema della fermata di Turing.

Trattandosi di un preprint, al quale OpenAI non risulta aver replicato e il cui abstract non indica file o versioni specifici, le sue conclusioni andranno vagliate, tenendo presente che una prova formale che segua una strada diversa da quella scritta lascia intatto il risultato finché l'enunciato formalizzato coincide con il teorema che si voleva dimostrare, e che il danno comincia soltanto quando a divergere è l'enunciato stesso. Il caso riguarda tuttavia tutti i 719 manoscritti, giacché Lean garantisce che il codice dimostri ciò che nel codice è scritto, mentre stabilire che quanto vi è scritto coincida con il teorema che interessa ai matematici resta un lavoro umano che non ammette scorciatoie, sicché quel 42 per cento misura soltanto la parte del catalogo passata al vaglio della macchina, senza dire nulla su quanta ne sia effettivamente corretta.

Il ritiro giunge al termine di un mese di tensioni, cominciato con la disputa di priorità che aveva accompagnato l'annuncio su Navier-Stokes, quando si era saputo che due matematici, Alpöge e Buckmaster, lavoravano allo stesso problema, e proseguito l'11 settembre con la dichiarazione con cui venticinque medaglie Fields, tra le quali Terence Tao, hanno contestato l'uso dei problemi matematici come banco di prova per l'industria dell'intelligenza artificiale. Ursula Martin, matematica di Oxford, ha paragonato la pubblicazione in blocco dei 722 manoscritti alla consegna di una prima bozza disordinata che la comunità dovrebbe poi incaricarsi di mettere in ordine, e il paragone trova riscontro nei numeri, giacché a OpenAI ogni manoscritto è costato in media tre ore di calcolo, mentre controllarlo richiede settimane o mesi di lavoro di specialisti che ricade su ricercatori i quali non l'avevano chiesto. L'azienda promette di finanziare workshop e convegni che aiutino i matematici a comprendere i risultati e assicura di lavorare al rilascio del modello, mentre il gruppo consultivo ha definito la pubblicazione l'inizio della comprensione umana anziché la sua conclusione, lasciando intendere che il grosso del lavoro debba ancora cominciare e che toccherà ad altri svolgerlo.

L'errore di segno è forse il più umano degli errori, quello in cui incorrono tanto gli studenti al primo esame quanto i vincitori della medaglia Fields, e ciò che la vicenda mette in discussione riguarda piuttosto la ripartizione della fatica, perché la matematica si regge su un patto in base al quale chi firma una dimostrazione la comprende e la difende, mentre la comunità si impegna a controllarla, e quel patto vacilla quando l'autore è un modello che nessuno può interrogare e i revisori sono matematici che nulla di tutto questo avevano chiesto. Lean avrebbe dovuto offrire una via d'uscita affidando il controllo al software, ma la vicenda di Navier-Stokes ricorda che il software controlla soltanto ciò che gli viene sottoposto, e finché OpenAI continuerà a produrre teoremi più in fretta di quanto il mondo riesca a leggerli, la parola "dimostrato" andrà presa con le molle anche quando a certificarla è un computer.