Matematici di primo piano stanno mettendo in dubbio l’affidabilità dei 719 manoscritti di matematica generati dall’intelligenza artificiale di OpenAI, dopo la pubblicazione di un articolo secondo cui la precedente dimostrazione di Navier–Stokes dell’azienda non coincide con la versione formalizzata e verificata al computer.
Punti chiave:
- Il catalogo di OpenAI è sceso da 722 a 719 manoscritti dopo il ritiro di tre articoli a causa di un errore di segno.
- Tre matematici con base nel Regno Unito hanno documentato due punti in cui la dimostrazione scritta di Navier–Stokes diverge dal codice Lean.
- Gli autori non sostengono che la dimostrazione sia falsa, ma affermano che i controlli automatici non possono sostituire la peer review.
Il rilascio dei risultati di OpenAI in matematica
OpenAI ha pubblicato la raccolta il 6 ottobre, e un’analisi diffusa giovedì ha rilevato che l’operazione si discosta dalle linee guida redatte da un panel indipendente di matematici per i laboratori di AI. Il catalogo era partito con 722 manoscritti. OpenAI ne ha poi ritirati tre il giorno successivo, dopo aver scoperto un errore di segno che invalidava un argomento e, di conseguenza, due lavori che vi si appoggiavano.
Le linee guida, pubblicate il 29 settembre dal Advisory Group on Mathematics and Artificial Intelligence, un comitato di nove membri, si aprono chiedendo ai laboratori di smettere di testare problemi avanzati di matematica su modelli proprietari. Il repository di OpenAI precisa che i lavori derivano dalla valutazione di un modello interno non ancora rilasciato su problemi di ricerca aperti.
Solo per 10 risultati sono disponibili sintesi del ragionamento del modello, e circa il 42% dei risultati principali è stato formalizzato in Lean, un linguaggio che consente al computer di verificare una dimostrazione in modo rigoroso.
Da leggere anche: Quanto guadagna il CEO di Anthropic? Il prospetto d’IPO svela la cifra
Le lacune nella dimostrazione di Navier–Stokes
Alexander Bastounis del King’s College London, insieme a Fabian Circelli e Anders Hansen dell’Università di Cambridge, hanno analizzato la dimostrazione di Navier–Stokes annunciata da OpenAI a settembre. Nel loro lavoro documentano due punti in cui l’argomentazione scritta e il codice Lean non coincidono, incluso un passaggio in cui il codice dimostra solo una stima più debole rispetto a quanto affermato nel paper.
Gli autori precisano di non esprimere un giudizio definitivo sulla correttezza della dimostrazione su carta. Il messaggio è più circoscritto: Lean certifica che il teorema finale è valido, scrivono, ma non è in grado di garantire la correttezza dei passaggi intermedi così come vengono letti da un umano. Per questo, insistono, tali dimostrazioni richiedono comunque la tradizionale peer review.
Il medagliato Fields Terence Tao ha scritto il 6 ottobre che molti problemi vengono risolti da “prompt engineer dell’AI” che non comprendono abbastanza a fondo gli output da poter rispondere alle domande o tenere conferenze sul contenuto delle dimostrazioni. La professoressa di Harvard Melanie Matchett Wood, membro del gruppo consultivo, ha osservato che al momento della pubblicazione “nessun umano capisce davvero questi risultati, e da lì inizia il vero lavoro”.
La controversia sulle dimostrazioni di OpenAI
Il gruppo consultivo ha ribadito che solo la comunità matematica nel suo complesso può valutare fino a che punto OpenAI abbia rispettato le raccomandazioni indicate. Il vaglio arriva al termine di un mese particolarmente teso. L’8 settembre OpenAI ha annunciato il risultato su Navier–Stokes, innescando una disputa sulla paternità con Tristan Buckmaster, matematico della New York University. Tre giorni dopo, 25 medaglie Fields hanno firmato una dichiarazione di allarme sul rischio che una produzione di massa di risultati “firmati” dall’intelligenza artificiale possa danneggiare lo sviluppo della disciplina.
Prossimo articolo: I 722 paper di matematica di OpenAI sono pubblici, ora la parola passa ai matematici
