Avete presente quella sensazione di quando provate a spiegare un concetto complicatissimo alla vostra compagna o al vostro compagno, convinti di aver dominato la materia, e poi vi rendete conto che avete appena detto una fesseria colossale? Ecco, sembra che anche i giganti della Silicon Valley debbamente occasionalmente si trovi in questa situazione imbarazzante.
OpenAI ha appena fatto un aggiornamento al suo repository GitHub dedicato alla matematica, e il log delle modifiche suona meno come un trionfo e più come un ‘scusate, stavamo testando la realtà’. Tra le novità, ci sono 6 nuove formalizzazioni in Lean (un linguaggio di programmazione per la verifica formale di teoremi, per chi non mastica abbastanza matematica per considerarsi un supercomputer) e 19 modifiche. Ma la vera notizia, quella che fa drizzare le antenne a chiunque abbia un minimo di sano scetticismo verso il marketing dell’IA, sono i 3 risultati ritirati.
Sì, avete letto bene. Hanno rimosso tre risultati perché, molto probabilmente, non stavano in piedi.
Per i non addetti ai lavori, usare Lean per la formalizzazione significa cercare di trasformare la matematica da ‘idea astratta’ a ‘codice verificabile’. È un lavoro di una complessità brutale, dove ogni errore logico salta fuori come un bug in un kernel Linux durante un aggiornamento non pianificato. Il fatto che il repo ora copra circa il 42% dei risultati principali è un dato tecnicamente interessante e decisamente figo, ma il ‘ritiro’ ci ricorda che l’hype che circonda questi modelli è spesso costruito su fondamenta di sabbia.
Siamo abituati a leggere comunicati stampa che ci vendono una singolarità imminente che risolverà il cancro e la fame nel mondo, ma la realtà è che siamo ancora in una fase di debugging pesante. Non è che la notizia sia una tragedia — anzi, l’approccio di aggiornare il repo con le correzioni è l’unico modo onesto per procedere — ma è un monito. Mentre il mondo intero si gasa per i nuovi benchmark, la verità sta nei commit di correzione.
In Italia, spesso ci limitiamo a guardare con un certo distacco le dinamiche della Bay Area, pensando che siano problemi che riguardano solo i nerd della West Coast. In realtà, questo tipo di ‘ritrattazione’ è fondamentale per la nostra community: ci dice che non dobbiamo bere ogni singola goccia di quello che viene spruzzato dai PR ufficial massivi. La scienza (e il codice) si basa sulla verifica, non sui tweet motivazionali.
Quindi, meno hype e più testing. Se OpenAI deve ritirare dei risultati, che lo faccia, ma speriamo che il prossimo aggiornamento porti meno ‘errata’ e più sostanza vera. Nel frattempo, continuiamo a sporcarci le mani con quello che è verificabile, che sia un script Python o un teorema in Lean.