OpenAI pubblica quasi 400 risultati matematici: i dubbi dei ricercatori
OpenAI ha pubblicato su GitHub quasi 400 risultati matematici prodotti dai suoi modelli, distribuiti su oltre 700 manoscritti. I matematici interpellati da The Verge parlano di una mole di lavoro tale che serviranno anni per capire davvero cosa contiene.
- OpenAI ha pubblicato quasi 400 risultati su oltre 700 manoscritti.
- Solo il 42% è formalizzato in Lean e verificabile dal computer.
- I matematici dicono che serviranno anni per valutare il materiale.
Una valanga di manoscritti
Il materiale copre discipline molto diverse: combinatoria, vari rami della geometria, teoria dei numeri, informatica teorica, algebra, topologia, probabilità, meccanica statistica e fisica matematica. La raccolta è così vasta che OpenAI ha dovuto pubblicare una guida per orientarsi nell'archivio pubblico su GitHub.
The Verge ha sentito oltre trenta matematici: le parole ricorrenti sono state sconcertante, travolgente, senza precedenti, surreale, pura follia. Alcuni hanno raccontato che leggere solo l'indice di circa 40 pagine con i riassunti ha richiesto quasi un'ora. Álvaro Lozano-Robledo, dell'Università del Connecticut, ha definito travolgente anche solo scorrere l'elenco degli abstract.
Secondo Il Sole 24 Ore, la scelta della trasparenza arriva dopo le polemiche seguite all'annuncio della soluzione del problema di Navier-Stokes, uno dei sette Problemi del Millennio, e alla lettera aperta di protesta firmata da vincitori della medaglia Fields. OpenAI dice di aver seguito il consiglio del gruppo consultivo indipendente su matematica e IA dell'Institute for Advanced Study, e indica una stima delle risorse di calcolo usate: circa tre ore di ragionamento di ChatGPT Pro per ciascun risultato.
Il nodo della verifica
Solo 300 risultati principali su 719 manoscritti, circa il 42%, sono stati formalizzati in Lean. Lean è un linguaggio di programmazione e assistente di dimostrazione: permette a un computer di controllare una dimostrazione passaggio per passaggio, dando la certezza che sia logicamente corretta anche a chi non ne segue tutti i ragionamenti.
Senza quella verifica, i ricercatori devono leggere testi che potrebbero contenere errori: lo ammette la stessa OpenAI, che parla di risultati a diversi stadi di verifica. Kevin Buzzard, dell'Imperial College di Londra, racconta a The Verge che nel suo campo, la teoria algebrica dei numeri, solo una mezza dozzina di teoremi gli è saltata all'occhio, e quasi nessuno risultava formalizzato. Anche dove il codice Lean c'è, aggiungono altri ricercatori, la qualità è disomogenea e le affermazioni verificate non sempre coincidono con quelle dei manoscritti.
Perché conta
La matematica pura diventa un terreno di competizione industriale: come nota Agenda Digitale, non basta più avere studiosi di fama, servono capitale, potenza di calcolo e modelli proprietari. Nessun ateneo, in Italia come altrove, può permettersi infrastrutture capaci di far lavorare in parallelo migliaia di agenti di intelligenza artificiale.
Il rischio segnalato dai ricercatori è uno squilibrio: produrre risultati diventa rapidissimo, verificarli e comprenderli resta lento e affidato al lavoro umano, spesso non retribuito e non riconosciuto.
Il commento
Nell'edizione video, Luca sottolinea proprio questo punto: la quantità non è ancora conoscenza finché qualcuno non legge, controlla e capisce.
