Ciò che conta è il loop
Alejandro Piad Morffis ha messo nero su bianco quello che stavo cercando di far quagliare da un pezzo nella mia mente: qual è il vero vantaggio che si può avere nell’uso dell’IA. Il punto è che al momento ci sono due narrazioni contrastanti: quella che afferma che ormai è l’IA a fare lo scienziato, e noi ci limitiamo a rimettere a posto quanto è stato da essa trovato, e quella che continua a parlare di pappagalli stocastici, che buttano fuori stringhe senza necessariamente senso lasciando all’autore l’ingrato compito di separare il grano del loglio. Piad Morffis, in modo quasi zen, afferma che entrambe le narrazioni sono sbagliate, perché rispondono alla domanda sbagliata, e cioè “l’IA fa scienza?”. Ciò che al momento sta facendo scienza è il loop: se volete dirlo in italiano, il processo iterativo (ma capite che se devo usare otto sillabe al posto di una lascio perdere). Insomma è l’interazione che produce scienza. Procedo con alcuni esempi.
Il primo esempio è quello dei cicli di Claude, con protagonisti Claude (appunto), Donald Knuth e Filip Stappers. Quest’ultimo ha usato Claude per esplorare una classe di oggetti combinatorici che Knuth stava studiando: uno dei risultati dei lanci gli è parso interessante e l’ha così passato a Knuth, che l’ha validato a mano. Quindi Stappers ha avuto l’idea e scremato l’output, Knuth è stato il verificatore, e Claude il proponente. La scelta del termine da parte di Piad Morffis è deliberata: Claude ha solo sfornato strutture (trentuno, per la cronaca). Il secondo esempio vede come protagonista Terence Tao, forse il più grande matematico vivente. Nel suo caso, gli LLM sono creativi ma inaffidabili e generano passi per le dimostrazioni; c’è poi un passo con Lean (un verificatore automatico) che è affidabile ma non creativo e butta via tutto quello che non funziona; infine Tao guarda i risultati sopravvissuti e decide quali può valer la pena di portare avanti. In questo caso cambiano le etichette, ma continuiamo ad avere un loop. Abbiamo poi AlphaFold, che genera possibili strutture 3-d di proteine. In questo caso l’IA è la proponente, il verificatore è la natura stessa, nel senso che si verifica sperimentalmente se la molecola generata si piega proprio in quel modo, e gli umani decidono se la struttura potrebbe avere un’utilità pratica. Infine c’è GNoME, che non è il desktop grafico Linux ma l’acronimo di Google DeepMind’s Graph Networks for Materials Exploration. Anche in questo caso GNoME ha proposto un enorme numero (380000) di possibili strutture cristalline. I ricercatori ne hanno selezionate 58 che hanno ritenuto essere interessanti e hanno provato ad assemblarle. Sono riusciti a ottenere 41 nuovi materiali.
La cosa più interessante è che anche in passato ci sono stati esempi simili di loop. Il più famoso è probabilmente la dimostrazione del teorema dei quattro colori da parte di Appel e Haken, che sono riusciti a dimostrare che bastava verificare la possibile colorazione per un numero finito anche se dell’ordine delle migliaia di configurazioni base e poi hanno lasciato al computer il compito di trovare la colorazione. Ma anche la dimostrazione della congettura di Keplero sull’impacchettamento ottimale per le sfere ha una storia simile: Thomas Hales ha trovato la dimostrazione nel 1998, ma ci sono voluti 16 anni perché un verificatore formale (Flyspeck) confermasse la sua correttezza. Con gli LLM sono cambiate due cose. La prima è l’equivalente del passaggio dai calcolatori analogici, che erano bravissimi a risolvere un problema specifico, a quelli digitali, che possono essere programmati per risolvere un problema generico – magari in modo meno ottimale, ma comunque con un risparmio netto rispetto al dover trovare la struttura analogica corretta. La seconda è che gli LLM non solo sono più generali ma sono anche in grado di ricevere istruzioni da sé stessi, aumentando quindi ancora di più la generalità. Ma ci sono cose che restano le stesse! Il verificatore (umano o macchina che sia) deve essere “stupido ma affidabile al 100%”, e quindi gli LLM lì sono fuorigioco; il curatore, colui che cioè decide se i risultati sono non solo corretti ma anche interessanti, continua a essere appannaggio degli umani; e così il problema di partenza è dato dagli umani. Il loop si è accelerato tantissimo, pensate solo ai sedici anni di Flyspeck contro i secondi impiegati da Lean, ma sempre loop è. Guardando la scienza da questo punto di vista possiamo insomma essere ottimisti: quello che facciamo è migliorato, ma non è davvero cambiato.
La polemica tra Croce ed Enriques sulla matematica, che per don Benedetto era uno strumento privo di contenuto speculativo autonomo, è ben nota; e del resto anche l’impostazione gentiliana del liceo scientifico. Quello che non sapevo è che la polemica era molto più ampia, soprattutto contro l’ideaismo crociano, tanto che Papini e Prezzolini nella loro rivista Leonardo accettavano volentieri contributi contro Croce da parte di matematici come Giovanni Vacca (curiosità: era il padre del futurologo Roberto Vacca), qui messo in forma di ebook. Alcuni punti del suo discorso non mi sono chiarissimi: ma ho trovato molto interessante il suo spostare il discorso dalla matematica all’arte, facendo notare che non si vede perché uno non debba rimanere estasiato dalle costruzioni di Euclide e Archimede. Una lettura molto breve ma interessante per un punto di vista spesso negletto.