I nuovi sistemi di intelligenza artificiale di Google DeepMind, AlphaProof e AlphaGeometry 2, possono risolvere complessi problemi matematici e rappresentano passi avanti verso la creazione di sistemi capaci di ragionare, il che potrebbe sbloccare nuove entusiasmanti capacità.
L’AI medaglia d’argento all’Olimpiade Internazionale di Matematica (IMO)
I modelli di intelligenza artificiale generano facilmente saggi e altri tipi di testo. Tuttavia, non sono altrettanto bravi a risolvere problemi matematici, che tendono a richiedere un ragionamento logico, una capacità che va oltre le possibilità della maggior parte dei sistemi AI attuali. Ma questa situazione potrebbe finalmente cambiare. Google DeepMind afferma di aver addestrato due sistemi AI specializzati per risolvere complessi problemi matematici che implicano un ragionamento avanzato. I sistemi, denominati AlphaProof e AlphaGeometry 2, hanno lavorato insieme riuscendo a risolvere quattro dei sei problemi proposti quest’anno all’Olimpiade Internazionale di Matematica (IMO), una prestigiosa competizione per studenti delle scuole superiori. Hanno conquistato l’equivalente di una medaglia d’argento.
È la prima volta che un sistema AI raggiunge un tasso di successo così elevato in questo tipo di problemi.
“Questo è un grande progresso nel campo dell’apprendimento automatico e dell’intelligenza artificiale,” afferma Pushmeet Kohli, vicepresidente della ricerca presso Google DeepMind, che ha lavorato al progetto. “Fino ad ora non era stato sviluppato alcun sistema in grado di risolvere problemi con questo tasso di successo e con questo livello di generalità.”
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.
I problemi matematici sono difficili da risolvere per i sistemi AI
Ci sono diverse ragioni per cui i problemi matematici che implicano un ragionamento avanzato sono difficili da risolvere per i sistemi AI. Questo tipo di problemi spesso richiede la formazione e l’utilizzo di astrazioni. Coinvolgono anche una pianificazione gerarchica complessa, oltre alla definizione di sotto-goal, al backtracking e al tentativo di nuovi percorsi. Tutti questi elementi rappresentano una sfida per l’AI. I sistemi AI in grado di risolvere matematica complessa potrebbero permetterci di sviluppare strumenti AI più potenti.
“È spesso più facile addestrare un modello per la matematica se si dispone di un modo per verificare le sue risposte (ad esempio, in una lingua formale), ma c’è relativamente meno dati matematici formali online rispetto al linguaggio naturale libero (linguaggio informale),” dice Katie Collins, ricercatrice presso l’Università di Cambridge specializzata in matematica e AI, che non ha partecipato al progetto.
AlphaProof, sistema basato su apprendimento rinforzato
Colmare questo divario è stato l’obiettivo di Google DeepMind nel creare AlphaProof, un sistema basato sull’apprendimento rinforzato che si addestra a dimostrare affermazioni matematiche nel linguaggio di programmazione formale 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 AI ibrida presso l’Università di Edimburgo, che ha sottoposto a revisione paritaria la ricerca ma non ha partecipato al progetto.
“Possiamo avere molta più fiducia nella correttezza dei risultati pubblicati se sono in grado di formulare questo sistema di dimostrazione, e può anche diventare più collaborativo”, aggiunge.
Alpha Geometry 2 è ottimizzato per affrontare problemi relativi a movimento di oggetti ed equazioni su angoli, rapporti e distanze
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 movimento di oggetti ed equazioni che coinvolgono angoli, rapporti e distanze. Essendo 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.
