L'intelligenza artificiale alle Olimpiadi internazionali della matematica: come AlphaProof e AlphaGeometry 2 hanno ottenuto la medaglia d'argento

Il ragionamento matematico è un aspetto vitale delle capacità cognitive umane, guidando il progresso nelle scoperte scientifiche e negli sviluppi tecnologici. Mentre ci sforziamo di sviluppare un’intelligenza artificiale generale che corrisponda alla cognizione umana, è essenziale dotare l’intelligenza artificiale di capacità di ragionamento matematico avanzate. Sebbene gli attuali sistemi di intelligenza artificiale siano in grado di gestire problemi matematici di base, hanno difficoltà con il ragionamento complesso necessario per discipline matematiche avanzate come l’algebra e la geometria. Tuttavia, la situazione potrebbe cambiare, come ha fatto Google DeepMind passi significativi nel promuovere le capacità di ragionamento matematico di un sistema di intelligenza artificiale. Questa svolta viene effettuata al Olimpiadi Internazionali della Matematica (IMO) 2024. Fondata nel 1959, l'IMO è la più antica e prestigiosa competizione di matematica, che sfida gli studenti delle scuole superiori di tutto il mondo con problemi di algebra, combinatoria, geometria e teoria dei numeri. Ogni anno, squadre di giovani matematici competono per risolvere sei problemi molto impegnativi. Quest’anno, Google DeepMind ha introdotto due sistemi di intelligenza artificiale: AlphaProof, che si concentra sul ragionamento matematico formale, e AlphaGeometry 2, specializzato nella risoluzione di problemi geometrici. Questi sistemi di intelligenza artificiale sono riusciti a risolvere quattro problemi su sei, esibendosi al livello di una medaglia d'argento. In questo articolo esploreremo come funzionano questi sistemi per risolvere problemi matematici.

AlphaProof: combinazione di intelligenza artificiale e linguaggio formale per la dimostrazione di teoremi matematici

AlphaProof è un sistema di intelligenza artificiale progettato per dimostrare affermazioni matematiche utilizzando il linguaggio formale Piega. Si integra Gemini, un modello linguistico pre-addestrato, con Alpha Zero, un algoritmo di apprendimento per rinforzo rinomato per padroneggiare gli scacchi, lo shogi e il Go.

Il modello Gemini traduce le dichiarazioni di problemi in linguaggio naturale in espressioni formali, creando una libreria di problemi con diversi livelli di difficoltà. Ciò ha due scopi: convertire il linguaggio naturale impreciso in un linguaggio formale preciso per verificare dimostrazioni matematiche e utilizzare le capacità predittive dei Gemelli per generare un elenco di possibili soluzioni con precisione del linguaggio formale.

Quando AlphaProof incontra un problema, genera potenziali soluzioni e cerca passaggi di prova in Lean per verificarli o confutarli. Questo è essenzialmente un approccio neuro-simbolico, in cui la rete neurale, Gemini, traduce le istruzioni del linguaggio naturale nel linguaggio formale simbolico Lean per dimostrare o confutare l'affermazione. Similmente al meccanismo di gioco autonomo di AlphaZero, in cui il sistema impara giocando contro se stesso, AlphaProof si allena tentando di dimostrare affermazioni matematiche. Ogni tentativo di prova perfeziona il modello linguistico di AlphaProof, con prove riuscite che rafforzano la capacità del modello di affrontare problemi più impegnativi.

Per le Olimpiadi Internazionali della Matematica (IMO), AlphaProof è stato addestrato dimostrando o confutando milioni di problemi che coprivano diversi livelli di difficoltà e argomenti matematici. Questa formazione è continuata durante la competizione, dove AlphaProof ha affinato le sue soluzioni fino a trovare risposte complete ai problemi.

AlphaGeometry 2: integrazione di LLM e intelligenza artificiale simbolica per risolvere problemi di geometria

AlphaGeometry 2 è l'ultima iterazione di AlphaGeometria serie, progettata per affrontare problemi geometrici con maggiore precisione ed efficienza. Basandosi sulle fondamenta del suo predecessore, AlphaGeometry 2 utilizza un approccio neuro-simbolico che unisce modelli neurali di grandi linguaggi (LLM) con l'intelligenza artificiale simbolica. Questa integrazione combina la logica basata su regole con la capacità predittiva delle reti neurali di identificare punti ausiliari, essenziali per risolvere problemi di geometria. Il LLM in AlphaGeometry prevede nuovi costrutti geometrici, mentre l'intelligenza artificiale simbolica applica la logica formale per generare prove.

Di fronte a un problema geometrico, LLM di AlphaGeometry valuta numerose possibilità, prevedendo costrutti cruciali per la risoluzione del problema. Queste previsioni fungono da indizi preziosi, guidando il motore simbolico verso deduzioni accurate e avanzando verso una soluzione. Questo approccio innovativo consente ad AlphaGeometry di affrontare sfide geometriche complesse che vanno oltre gli scenari convenzionali.

Un miglioramento chiave in AlphaGeometry 2 è l'integrazione di Gemini LLM. Questo modello è addestrato da zero su un numero significativamente maggiore di dati sintetici rispetto al suo predecessore. Questa formazione approfondita lo equipaggia per gestire problemi di geometria più difficili, compresi quelli che coinvolgono i movimenti degli oggetti e le equazioni di angoli, rapporti o distanze. Inoltre, AlphaGeometry 2 è dotato di un motore simbolico che opera due ordini di grandezza più velocemente, consentendogli di esplorare soluzioni alternative con una velocità senza precedenti. Questi progressi rendono AlphaGeometry 2 un potente strumento per risolvere problemi geometrici complessi, stabilendo un nuovo standard nel campo.

AlphaProof e AlphaGeometry 2 all'IMO

Quest’anno alle Olimpiadi Internazionali della Matematica (IMO), i partecipanti sono stati testati con sei diversi problemi: due di algebra, uno di teoria dei numeri, uno di geometria e due di combinatoria. ricercatori di Google tradotto questi problemi in un linguaggio matematico formale per AlphaProof e AlphaGeometry 2. AlphaProof ha affrontato due problemi di algebra e un problema di teoria dei numeri, incluso il problema più difficile della competizione, risolto quest'anno da soli cinque concorrenti umani. Nel frattempo, AlphaGeometry 2 ha risolto con successo il problema della geometria, anche se non ha risolto le due sfide combinatorie

Ogni problema all'IMO vale sette punti, sommati fino a un massimo di 42. AlphaProof e AlphaGeometry 2 hanno guadagnato 28 punti, ottenendo punteggi perfetti sui problemi risolti. Ciò li ha collocati nella fascia alta della categoria delle medaglie d'argento. La soglia della medaglia d'oro quest'anno era di 29 punti, raggiunta da 58 dei 609 concorrenti.

Prossimo salto: linguaggio naturale per sfide matematiche

AlphaProof e AlphaGeometry 2 hanno messo in mostra impressionanti progressi nelle capacità di risoluzione dei problemi matematici dell'intelligenza artificiale. Tuttavia, questi sistemi fanno ancora affidamento su esperti umani per tradurre i problemi matematici in un linguaggio formale per l’elaborazione. Inoltre, non è chiaro come queste competenze matematiche specializzate potrebbero essere incorporate in altri sistemi di intelligenza artificiale, ad esempio per esplorare ipotesi, testare soluzioni innovative a problemi di vecchia data e gestire in modo efficiente aspetti delle dimostrazioni che richiedono molto tempo.

Per superare queste limitazioni, i ricercatori di Google stanno sviluppando un sistema di ragionamento in linguaggio naturale basato su Gemini e sulle loro ultime ricerche. Questo nuovo sistema mira a migliorare le capacità di risoluzione dei problemi senza richiedere la traduzione linguistica formale ed è progettato per integrarsi perfettamente con altri sistemi di intelligenza artificiale.

Conclusione

Le prestazioni di AlphaProof e AlphaGeometry 2 alle Olimpiadi internazionali della matematica rappresentano un notevole passo avanti nella capacità dell'intelligenza artificiale di affrontare ragionamenti matematici complessi. Entrambi i sistemi hanno dimostrato prestazioni da medaglia d'argento risolvendo quattro problemi impegnativi su sei, dimostrando progressi significativi nella dimostrazione formale e nella risoluzione dei problemi geometrici. Nonostante i risultati ottenuti, questi sistemi di intelligenza artificiale dipendono ancora dal contributo umano per tradurre i problemi in linguaggio formale e devono affrontare sfide di integrazione con altri sistemi di intelligenza artificiale. La ricerca futura mira a migliorare ulteriormente questi sistemi, integrando potenzialmente il ragionamento in linguaggio naturale per estendere le loro capacità a una gamma più ampia di sfide matematiche.