Come affermano i team di AlphaProof e AlphaGeometry sul blog di Google DeepMind, l’intelligenza artificiale generale (AGI, Artificial general intelligence) con ragionamento matematico avanzato ha il potenziale per aprire nuove frontiere nella scienza e nella tecnologia.
Sono stati fatti grandi progressi nella realizzazione di sistemi di intelligenza artificiale che aiutano i matematici a scoprire nuove intuizioni, nuovi algoritmi e risposte a problemi aperti. Ma gli attuali sistemi di AI hanno ancora difficoltà a risolvere problemi matematici generali a causa delle limitazioni nelle capacità di ragionamento e nei dati di addestramento.
Ora Google DeepMind ha presentato AlphaProof, un nuovo sistema basato sul reinforcement-learning per il ragionamento matematico formale, e AlphaGeometry 2, una versione migliorata del sistema di risoluzione della geometria dell’azienda. Insieme, questi sistemi hanno risolto quattro dei sei problemi dell’International Mathematical Olympiad (IMO) – la maggiore, più antica e prestigiosa competizione per giovani matematici, che si tiene ogni anno dal 1959 – di quest’anno, raggiungendo per la prima volta lo stesso livello di una medaglia d’argento nella competizione.
Ogni anno, un’élite di matematici pre-universitari si allena, a volte per migliaia di ore, per risolvere sei problemi eccezionalmente difficili in algebra, combinatoria, geometria e teoria dei numeri. Molti dei vincitori della Fields Medal, una delle massime onorificenze per i matematici, hanno rappresentato il loro Paese alle IMO.
Più di recente, il concorso annuale IMO è diventato ampiamente riconosciuto come una grande sfida nell’apprendimento automatico e un punto di riferimento per misurare le capacità avanzate di ragionamento matematico di un sistema di intelligenza artificiale.
Quest’anno Google DeepMind ha applicato il suo sistema AI combinato ai problemi del concorso, forniti dagli organizzatori dell’IMO. Le soluzioni sono state valutate in base alle regole di assegnazione dei punti dell’IMO da matematici di spicco come il Prof. Sir Timothy Gowers, medaglia d’oro IMO e vincitore della Fields Medal, e il Dr. Joseph Myers, due volte medaglia d’oro IMO e presidente del Comitato di selezione dei problemi IMO 2024.
In primo luogo, i problemi sono stati tradotti manualmente in un linguaggio matematico formale comprensibile ai sistemi AI. Nella competizione ufficiale, gli studenti inviano le risposte in due sessioni di 4,5 ore ciascuna. I sistemi di Google DeepMind hanno risolto un problema in pochi minuti e hanno impiegato fino a tre giorni per risolvere gli altri.
AlphaProof ha risolto due problemi di algebra e uno di teoria dei numeri determinando la risposta e dimostrandone la correttezza. Questo includeva il problema più difficile della competizione, risolto solo da cinque concorrenti all’IMO di quest’anno. AlphaGeometry 2 ha risolto il problema di geometria, mentre i due problemi di combinatoria sono rimasti irrisolti.
“Il fatto che il programma sia in grado di proporre una costruzione non ovvia come questa è davvero impressionante e va ben oltre quello che pensavo fosse lo stato dell’arte”, ha comentato il Prof. Sir Timothy Gowers, IMO Gold Medalist e Fields Medal Winner.
Nell’ambito del suo lavoro dell’IMO, Google DeepMind ha anche sperimentato un sistema di ragionamento in linguaggio naturale, basato su Gemini e sulle ultime ricerche del team, per consentire capacità avanzate di risoluzione dei problemi. Questo sistema non richiede la traduzione dei problemi in un linguaggio formale e può essere combinato con altri sistemi di intelligenza artificiale. Il team ha testato questo approccio anche sui problemi IMO di quest’anno e i risultati sono stati molto promettenti.
Nel post sul blog di Google DeepMind è possibile leggere ulteriori dettagli sui modelli AlphaProof e AlphaGeometry e sulla loro performance all’International Mathematical Olympiad, comprese le soluzioni di IMO 2024.
