AlphaProof e AlphaGeometry sono passi avanti verso la costruzione di sistemi in grado di ragionare, che potrebbero sbloccare nuove ed entusiasmanti capacità.
I modelli di intelligenza artificiale possono generare facilmente saggi e altri tipi di testo. Tuttavia, non sono neanche lontanamente in grado di risolvere problemi matematici, che tendono a coinvolgere il ragionamento logico, cosa che è al di là delle capacità della maggior parte degli attuali sistemi di IA.
Ma questo potrebbe finalmente cambiare. Google DeepMind ha dichiarato di aver addestrato due sistemi di intelligenza artificiale specializzati a risolvere complessi problemi matematici che richiedono un ragionamento avanzato. I sistemi, chiamati AlphaProof e AlphaGeometry 2, hanno lavorato insieme per risolvere con successo quattro dei sei problemi dell’International Mathematical Olympiad (IMO) di quest’anno, una prestigiosa competizione per studenti delle scuole superiori. Hanno vinto l’equivalente di una medaglia d’argento all’evento.
È la prima volta che un sistema di intelligenza artificiale raggiunge un tasso di successo così alto su questo tipo di problemi. “Si tratta di un grande progresso nel campo dell’apprendimento automatico e dell’IA”, afferma Pushmeet Kohli, vicepresidente della ricerca di Google DeepMind, che ha lavorato al progetto. “Finora non era stato sviluppato alcun sistema in grado di risolvere problemi con questo tasso di successo e con questo livello di generalità”.
Ci sono alcuni motivi per cui i problemi matematici che implicano un ragionamento avanzato sono difficili da risolvere per i sistemi di intelligenza artificiale. Questi tipi di problemi richiedono spesso la formazione e l’utilizzo di astrazioni. Comportano anche una complessa pianificazione gerarchica, nonché la definizione di sotto-obiettivi, il backtracking e la sperimentazione di nuovi percorsi. Tutti questi aspetti rappresentano una sfida per l’IA.
“Spesso è più facile addestrare un modello per la matematica se si ha un modo per verificare le sue risposte (ad esempio, in un linguaggio formale), ma ci sono relativamente meno dati matematici formali online rispetto al linguaggio naturale libero (linguaggio informale)”, afferma Katie Collins, ricercatrice dell’Università di Cambridge specializzata in matematica e IA ma non coinvolta nel progetto.
Colmare questo divario è stato l’obiettivo di Google DeepMind nel creare AlphaProof, un sistema basato sull’apprendimento per rinforzo che si addestra a dimostrare affermazioni matematiche nel linguaggio formale di programmazione Lean. La chiave è una versione dell’intelligenza artificiale Gemini di DeepMind, messa a punto per tradurre automaticamente i problemi matematici formulati in un linguaggio naturale e informale in affermazioni formali, più facili da elaborare per l’intelligenza artificiale. In questo modo è stata creata un’ampia libreria di problemi matematici formali con diversi gradi di difficoltà.
Automatizzare il processo di traduzione dei dati in linguaggio formale è un grande passo avanti per la comunità matematica, afferma Wenda Li, docente di IA ibrida presso l’Università di Edimburgo, che ha sottoposto a revisione paritaria la ricerca ma non ha partecipato al progetto.
“Possiamo avere una fiducia molto maggiore nella correttezza dei risultati pubblicati se sono in grado di formulare questo sistema di prova, e può anche diventare più collaborativo”, aggiunge.
Il modello Gemini lavora insieme ad AlphaZero – il modello di apprendimento per rinforzo che Google DeepMind ha addestrato per padroneggiare giochi come il Go e gli scacchi – per dimostrare o confutare milioni di problemi matematici. Più problemi ha risolto con successo, più AlphaProof è diventato bravo ad affrontare problemi di complessità crescente.
Sebbene AlphaProof sia stato addestrato per affrontare problemi relativi a un’ampia gamma di argomenti matematici, AlphaGeometry 2, una versione migliorata di un sistema annunciato da Google DeepMind a gennaio, è stato ottimizzato per affrontare problemi relativi a movimenti di oggetti ed equazioni che coinvolgono angoli, rapporti e distanze. Poiché è stato addestrato su un numero significativamente maggiore di dati sintetici rispetto al suo predecessore, è stato in grado di affrontare domande di geometria molto più impegnative.
Per testare le capacità dei sistemi, i ricercatori di Google DeepMind li hanno incaricati di risolvere i sei problemi assegnati agli esseri umani in gara alle IMO di quest’anno e di dimostrare che le risposte erano corrette. AlphaProof ha risolto due problemi di algebra e uno di teoria dei numeri, uno dei quali era il più difficile della competizione. AlphaGeometry 2 ha risolto con successo un problema di geometria, ma due domande di combinatoria (un’area della matematica incentrata sul conteggio e sulla disposizione degli oggetti) sono rimaste irrisolte.
“In generale, AlphaProof funziona molto meglio con l’algebra e la teoria dei numeri che con la combinatoria”, afferma Alex Davies, ingegnere ricercatore del team AlphaProof. “Stiamo ancora lavorando per capire il perché di questa situazione, che speriamo ci porti a migliorare il sistema”.
Due matematici di fama, Tim Gowers e Joseph Myers, hanno controllato i sistemi presentati. Hanno assegnato a ciascuna delle quattro risposte corrette il massimo dei voti (sette su sette), assegnando ai sistemi un totale di 28 punti su un massimo di 42. Un partecipante umano che avesse ottenuto questo punteggio sarebbe stato premiato con una medaglia d’argento e avrebbe mancato di poco l’oro, la cui soglia parte da 29 punti.
È la prima volta che un sistema di intelligenza artificiale riesce a ottenere una prestazione di livello medaglia su quesiti IMO. “Come matematico, lo trovo davvero impressionante e un salto significativo rispetto a quanto era possibile fare in precedenza”, ha dichiarato Gowers durante una conferenza stampa.
Myers concorda sul fatto che le risposte matematiche del sistema rappresentano un progresso sostanziale rispetto a ciò che l’IA poteva ottenere in precedenza. “Sarà interessante vedere come le cose si scalano, se possono essere rese più veloci e se si possono estendere ad altri tipi di matematica”, ha detto.
La creazione di sistemi di intelligenza artificiale in grado di risolvere problemi matematici più impegnativi potrebbe aprire la strada a interessanti collaborazioni tra uomo e IA, aiutando i matematici a risolvere e inventare nuovi tipi di problemi, afferma Collins. Questo, a sua volta, potrebbe aiutarci a capire meglio come noi umani affrontiamo la matematica.
“Ci sono ancora molte cose che non sappiamo su come gli esseri umani risolvono i problemi matematici complessi”, afferma l’autrice.
