OpenAI dice di aver risolto dieci problemi di matematica aperti da decenni

Il primo agosto OpenAI ha annunciato che un suo modello non ancora pubblicato, chiamato Astra, ha risolto dieci problemi di matematica e di informatica teorica rimasti aperti per almeno dieci anni. Uno di questi resisteva dal 1999, un altro dal 1980.

Annunci del genere ne circolano spesso, e quasi sempre la parte difficile è capire quanto valgano. Questa volta c’è un motivo per prenderli sul serio, e c’è una discussione seria su come sono stati presentati.

Perché stavolta la verifica non richiede fiducia

Insieme all’annuncio OpenAI ha pubblicato un manoscritto di 249 pagine e, soprattutto, le dimostrazioni scritte in Lean, un linguaggio in cui un ragionamento matematico si scrive come si scrive un programma. Un verificatore automatico lo compila e dà una risposta secca: la catena di passaggi regge oppure non regge, senza sfumature e senza bisogno di credere a chi l’ha prodotta.

È una differenza sostanziale rispetto ai proclami abituali sulle capacità dei modelli. Un risultato in linguaggio naturale va letto e giudicato da un esperto, cosa che richiede mesi. Un certificato in Lean lo controlla chiunque abbia il compilatore, in poche ore, e non lascia margine di interpretazione. I file sono pubblici con una licenza che ne consente il riuso.

OpenAI ha inoltre dichiarato che il calcolo necessario per arrivare a tutte e dieci le soluzioni è costato circa duemila dollari. Se la cifra è corretta, il messaggio implicito è che questo tipo di lavoro non richiede più il bilancio di un grande laboratorio.

La contestazione dei matematici non riguarda i risultati

Sarebbe comodo raccontarla come una comunità scettica smentita dai fatti. Non è quello che sta succedendo. Le obiezioni riguardano il metodo di pubblicazione, non la correttezza delle prove.

Il 2 giugno un gruppo internazionale di matematici ha pubblicato la Dichiarazione di Leida, sottoscritta anche dall’Unione Matematica Internazionale e firmata da oltre mille persone nel primo giorno. Il documento non chiede di vietare l’IA nella ricerca matematica: chiede regole condivise su tre punti che considera in pericolo, e cioè l’integrità della dimostrazione, il sistema con cui si attribuisce la paternità di un risultato e l’autonomia della ricerca rispetto alle aziende che finanziano gli strumenti.

Il punto più concreto è che annunciare risultati con un comunicato stampa scavalca la revisione fra pari, che è il meccanismo con cui la matematica decide cosa è vero. Chi ha firmato ritiene che un risultato certificato da un compilatore sia una garanzia diversa e non sostitutiva di quella.

Quali problemi l’IA affronta bene, secondo chi li conosce

La parte utile per chi non fa il matematico di mestiere arriva dall’analisi che Timothy Gowers ha pubblicato il 12 agosto. Gowers ha vinto la medaglia Fields, il massimo riconoscimento della disciplina, e si è messo a osservare non se questi modelli funzionano ma su quali problemi funzionano.

La sua osservazione è che i risultati più famosi ottenuti finora sono quasi tutti controesempi: casi costruiti apposta per dimostrare che un’affermazione che tutti davano per vera in realtà è falsa. Le dimostrazioni vere e proprie, cioè le costruzioni che stabiliscono che qualcosa vale sempre, restano molto più rare.

La spiegazione che ne dà è meno lusinghiera di quanto sembri e più istruttiva. Un controesempio si trova tentando molte strade e verificando ogni tentativo, e su questo terreno una macchina ha due vantaggi enormi: conosce un repertorio sterminato di argomenti standard da riutilizzare, e può permettersi un numero altissimo di tentativi falliti senza stancarsi. Dove i modelli restano indietro è nei problemi che richiedono di potare l’albero delle possibilità con l’intuito, scartando in anticipo strade che nessun calcolo dice ancora di scartare. Senza quella potatura la ricerca diventa impraticabile persino per un computer.

Gowers non conclude che sia un limite permanente: dice che i modelli continueranno a migliorare in fretta e che non è chiaro se questo confine sia strutturale o solo il punto in cui siamo arrivati.

La regola pratica che si può portare via

La distinzione di Gowers si trasferisce quasi intatta al lavoro di tutti i giorni, e vale la pena tenerla presente prima di decidere cosa affidare a uno di questi strumenti.

Un modello rende al massimo quando il compito ha due caratteristiche insieme: si può tentare molte volte e il risultato si riconosce a colpo d’occhio. Trovare il caso che manda in errore una procedura, scovare l’incongruenza in un contratto, generare venti versioni di un testo fra cui scegliere: sono tutti problemi in cui la verifica costa meno del tentativo.

Rende molto meno quando serve costruire una catena lunga di passaggi che stanno in piedi solo tutti insieme, e in cui nessun anello si può controllare separatamente. Una previsione di bilancio, una strategia, una perizia: lì l’output arriva plausibile e uniforme, e proprio per questo l’errore è difficile da vedere. La differenza non sta nella difficoltà del compito. Sta in quanto costa accorgersi che la risposta è sbagliata.

La riflessione

In filigrana, emerge una forma di resistenza all’IA. Quando una categoria professionale viene investita dal suo impatto, è naturale che cerchi di difendere la propria posizione: accade in questo caso ai matematici, sulla base di argomentazioni del tutto fondate, ed è già accaduto, e accadrà, anche ad altri. È naturale cercare riparo quando si è investiti da un potenziale terremoto.

La realtà però sembra muoversi velocemente in un’altra direzione. L’IA non è destinata a essere soltanto un acceleratore, né l’ennesimo giocatore chiamato a operare secondo le regole attuali. Il suo effetto sarà dirompente: in molti settori cambierà radicalmente le regole del gioco.

Alcune procedure sono semplicemente destinate a perdere utilità o diventare inattuabili. Per intenderci, quando l’IA sarà in grado di produrre ogni giorno migliaia di ricerche e paper di alto livello, sarà ancora possibile sottoporli tutti al tradizionale processo di revisione tra pari?