AlphaProof e AlphaGeometry 2 di Google DeepMind sono pietre miliari per il ragionamento dell’intelligenza artificiale.
È stata un’altra settimana importante per l’IA. Meta ha aggiornato il suo nuovo potente modello Llama, che sta distribuendo gratuitamente, e OpenAI ha dichiarato che sperimenterà uno strumento di ricerca online alimentato dall’intelligenza artificiale con cui si può chattare, chiamato SearchGPT.
Ma la notizia che mi ha davvero colpito è una che non ha ricevuto l’attenzione che avrebbe dovuto. Ha il potenziale per inaugurare un’intelligenza artificiale e una scoperta scientifica più potenti di quanto sia stato possibile in precedenza.
Giovedì scorso, Google DeepMind ha annunciato di aver costruito sistemi di intelligenza artificiale in grado di risolvere complessi problemi matematici. I sistemi, chiamati AlphaProof e AlphaGeometry 2, hanno lavorato insieme per risolvere con successo quattro dei sei problemi dell’International Mathematical Olympiad di quest’anno, una prestigiosa competizione per studenti delle scuole superiori. La loro performance è stata equivalente alla conquista di una medaglia d’argento. È la prima volta che un sistema di intelligenza artificiale raggiunge un tasso di successo così alto su questo tipo di problemi. La collega Rhiannon Williams ne dà notizia qui.
Matematica! Immagino già i vostri occhi che si stanno sgranando. Ma abbiate pazienza. Questo annuncio non riguarda solo la matematica. Anzi, segnala un nuovo ed entusiasmante sviluppo del tipo di IA che possiamo costruire. I motori di ricerca AI con cui si può chattare possono dare un’illusione di intelligenza, ma sistemi come quello di Google DeepMind potrebbero migliorare l’intelligenza effettiva dell’IA. Per questo motivo, la costruzione di sistemi che migliorano la matematica è un obiettivo di molti laboratori di IA, come OpenAI.
Questo perché la matematica è un punto di riferimento per il ragionamento. Per completare questi esercizi rivolti agli studenti delle scuole superiori, i sistemi di intelligenza artificiale dovevano fare cose molto complesse, come pianificare per comprendere e risolvere problemi astratti. I sistemi erano anche in grado di generalizzare, consentendo loro di risolvere un’intera gamma di problemi diversi in varie branche della matematica.
“Quello che abbiamo visto qui è che è possibile combinare [l’apprendimento per rinforzo] che ha avuto tanto successo in cose come AlphaGo con modelli linguistici di grandi dimensioni e produrre qualcosa che è estremamente capace nello spazio del testo”, ha detto David Silver, ricercatore principale di Google DeepMind e indiscutibilmente un pioniere dell’apprendimento per rinforzo profondo, in una conferenza stampa. In questo caso, tale capacità è stata utilizzata per costruire programmi nel linguaggio informatico Lean che rappresentano prove matematiche. Secondo l’esperto, le Olimpiadi Internazionali di Matematica rappresentano un banco di prova per le possibilità di successo e aprono la strada a ulteriori scoperte.
Questa stessa ricetta potrebbe essere applicata in qualsiasi situazione con segnali di ricompensa davvero chiari e verificati per gli algoritmi di apprendimento per rinforzo e un modo inequivocabile di misurare la correttezza come si può fare in matematica, ha detto Silver. Una potenziale applicazione potrebbe essere, ad esempio, la codifica.
Ora è d’obbligo una verifica della realtà: AlphaProof e AlphaGeometry 2 possono ancora risolvere solo problemi difficili di livello liceale. Questo è molto lontano dai problemi estremamente difficili che i migliori matematici umani possono risolvere. Google DeepMind ha sottolineato che il suo strumento non aggiunge nulla all’insieme delle conoscenze matematiche create dall’uomo. Ma non era questo il punto.
“Il nostro obiettivo è fornire un sistema in grado di dimostrare qualsiasi cosa”, ha dichiarato Silver. Pensate a un sistema di intelligenza artificiale affidabile come una calcolatrice, per esempio, in grado di fornire prove per molti problemi difficili, o di verificare test per software informatici o esperimenti scientifici. O magari di costruire migliori tutor di intelligenza artificiale in grado di fornire un feedback sui risultati degli esami o di verificare i fatti degli articoli di cronaca.
Ma la cosa che mi entusiasma di più è ciò che ha detto a Rhiannon Katie Collins, una ricercatrice dell’Università di Cambridge specializzata in matematica e IA (e non coinvolta nel progetto). Afferma che questi strumenti creano e valutano nuovi problemi, motivano nuove persone a entrare nel settore e suscitano maggiore meraviglia. È qualcosa di cui abbiamo decisamente bisogno in questo mondo.