Matematici di primo piano si interrogano sull’affidabilità dei 719 manoscritti matematici generati dall’IA di OpenAI, dopo che un nuovo lavoro ha evidenziato come la precedente dimostrazione di Navier-Stokes dell’azienda non coincida 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 lavori a causa di un errore di segno.
- Tre matematici con base nel Regno Unito hanno documentato due divergenze tra la versione scritta della prova di Navier-Stokes e il relativo codice Lean.
- Gli autori non affermano che la dimostrazione sia sbagliata, ma sostengono che i controlli automatici non possono sostituire la peer review.
Il rilascio dei risultati matematici di OpenAI
La società ha pubblicato la raccolta il 6 ottobre. Un’inchiesta uscita giovedì ha rilevato che il progetto si discosta dalle linee guida messe nero su bianco da un comitato indipendente di matematici per i laboratori di IA. Il catalogo si è aperto con 722 manoscritti. OpenAI ne ha poi ritirati tre il giorno successivo, dopo che un errore di segno aveva compromesso un argomento centrale e due lavori che su di esso facevano affidamento.
Quelle linee guida, pubblicate il 29 settembre dal Advisory Group on Mathematics and Artificial Intelligence, composto da nove membri, si aprono chiedendo ai laboratori di sospendere i test su problemi avanzati di matematica con modelli proprietari. Il repository di OpenAI precisa che gli articoli derivano dalla valutazione di un modello interno non rilasciato su problemi di ricerca aperti.
Soltanto per 10 risultati sono disponibili sommari del ragionamento del modello, e circa il 42% dei risultati principali è stato formalizzato in Lean, un linguaggio che consente al computer di verificare la correttezza dei passaggi logici.
Da leggere anche: Quanto guadagna il CEO di Anthropic? La risposta nel prospetto di IPO
Le lacune nella dimostrazione di Navier-Stokes
Alexander Bastounis del King’s College London e Fabian Circelli e Anders Hansen dell’Università di Cambridge hanno analizzato la dimostrazione di Navier-Stokes annunciata da OpenAI a settembre. Nel loro lavoro individuano due punti in cui l’argomentazione scritta e il codice Lean divergono, tra cui un caso in cui il codice dimostra una stima più debole di quanto dichiarato nel paper.
Gli autori precisano di non esprimersi sulla correttezza complessiva della dimostrazione scritta. Il loro messaggio è più circoscritto. Lean conferma che il teorema finale è vero, spiegano, ma non garantisce che i passaggi intermedi, quelli che il lettore umano vede nel testo, siano rigorosi. Per questo, concludono, dimostrazioni di questo tipo richiedono comunque un vaglio di peer review tradizionale.
Il medagliato Fields Terence Tao ha osservato il 6 ottobre che molti problemi vengono risolti da “prompt engineer dell’IA” che non comprendono abbastanza a fondo gli output per rispondere alle domande o tenere conferenze sul contenuto dei lavori. La professoressa di Harvard Melanie Matchett Wood, membro del gruppo consultivo, ha sottolineato che, al momento della pubblicazione, “nessun essere umano capisce davvero questi risultati, ed è solo allora che il lavoro vero comincia”.
La controversia sulle prove di OpenAI
Il gruppo consultivo ha ribadito che solo la comunità matematica nel suo complesso può valutare quanto fedelmente OpenAI abbia seguito le sue raccomandazioni. Questo scrutinio arriva al termine di un mese teso. OpenAI ha annunciato il risultato su Navier-Stokes l’8 settembre, innescando una disputa sul merito con il matematico della New York University Tristan Buckmaster; tre giorni dopo, 25 medagliati Fields hanno promosso una dichiarazione in cui avvertono che una produzione di massa di risultati matematici generati dall’IA potrebbe danneggiare la disciplina.
Da leggere dopo: I 722 articoli matematici IA di OpenAI sono pubblici, ora tocca ai matematici valutarli
