L’AI all’Olimpiade Matematica Internazionale: Come AlphaProof e AlphaGeometry 2 Hanno Raggiunto il Livello di Medaglia d’Argento

La ragione matematica è un aspetto vitale delle capacità cognitive umane, che guidano il progresso nelle scoperte scientifiche e negli sviluppi tecnologici. Mentre cerchiamo di sviluppare un’intelligenza artificiale generale che eguagli la cognizione umana, è essenziale dotare l’AI di capacità di ragionamento matematico avanzate. Sebbene i sistemi AI attuali possano gestire problemi matematici di base, lottano con il ragionamento complesso necessario per discipline matematiche avanzate come l’algebra e la geometria. Tuttavia, questo potrebbe cambiare, poiché Google DeepMind ha fatto passi significativi nell’avanzare le capacità di ragionamento matematico di un sistema AI. Questo passo avanti è stato fatto all’Olimpiade Matematica Internazionale (IMO) 2024. Fondata nel 1959, l’IMO è la più antica e prestigiosa competizione 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 presentato due sistemi AI: AlphaProof, che si concentra sul ragionamento matematico formale, e AlphaGeometry 2, che si specializza nella risoluzione di problemi geometrici. Questi sistemi AI sono riusciti a risolvere quattro problemi su sei, eseguendo al livello di un medaglia d’argento. In questo articolo, esploreremo come questi sistemi funzionano per risolvere problemi matematici.

AlphaProof: Combinando AI e Linguaggio Formale per la Dimostrazione di Teoremi Matematici

AlphaProof è un sistema AI progettato per dimostrare affermazioni matematiche utilizzando il linguaggio formale Lean. Integra Gemini, un modello di linguaggio pre-addestrato, con AlphaZero, un algoritmo di apprendimento per rinforzo noto per aver padroneggiato scacchi, shogi e Go.

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

Quando AlphaProof incontra un problema, genera soluzioni potenziali e cerca passaggi di dimostrazione in Lean per verificarle o smentirle. Ciò è essenzialmente un approccio neuro-simbolico, in cui la rete neurale, Gemini, traduce le istruzioni del linguaggio naturale in linguaggio formale simbolico Lean per dimostrare o smentire l’affermazione. Simile al meccanismo di auto-gioco di AlphaZero, in cui il sistema apprende giocando contro se stesso, AlphaProof si addestra tentando di dimostrare affermazioni matematiche. Ogni tentativo di dimostrazione raffina il modello linguistico di AlphaProof, con dimostrazioni riuscite che rafforzano la capacità del modello di affrontare problemi più impegnativi.

Per l’Olimpiade Matematica Internazionale (IMO), AlphaProof è stato addestrato dimostrando o smentendo milioni di problemi che coprono diversi livelli di difficoltà e argomenti matematici. Questo addestramento è continuato durante la competizione, in cui AlphaProof ha raffinato le sue soluzioni fino a quando non ha trovato risposte complete ai problemi.

AlphaGeometry 2: Integrando LLM e AI Simbolica per la Risoluzione di Problemi Geometrici

AlphaGeometry 2 è l’ultima iterazione della serie AlphaGeometry, progettata per affrontare problemi geometrici con precisione e efficienza avanzate. Costruendo sulla base del suo predecessore, AlphaGeometry 2 impiega un approccio neuro-simbolico che combina grandi modelli di linguaggio neurali (LLM) con AI simbolica. Questa integrazione combina logica basata su regole con la capacità predittiva delle reti neurali per identificare punti ausiliari, essenziali per la risoluzione di problemi geometrici. L’LLM in AlphaGeometry prevede nuove costruzioni geometriche, mentre l’AI simbolica applica logica formale per generare dimostrazioni.

Quando si confronta con un problema geometrico, l’LLM di AlphaGeometry valuta numerose possibilità, prevedendo costrutti cruciali per la risoluzione del problema. Queste previsioni servono come 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 si estendono oltre scenari convenzionali.

Un miglioramento chiave in AlphaGeometry 2 è l’integrazione del modello LLM Gemini. Questo modello è stato addestrato da zero su dati sintetici significativamente più ampi del suo predecessore. Questo addestramento estensivo lo rende in grado di gestire problemi geometrici più difficili, compresi quelli che coinvolgono movimenti di oggetti ed equazioni di angoli, rapporti o distanze. Inoltre, AlphaGeometry 2 presenta un motore simbolico che opera due ordini di grandezza più veloce, consentendogli di esplorare soluzioni alternative con una velocità senza precedenti. Questi progressi rendono AlphaGeometry 2 uno strumento potente per la risoluzione di problemi geometrici intricati, stabilendo un nuovo standard nel settore.

AlphaProof e AlphaGeometry 2 all’IMO

Quest’anno all’Olimpiade Matematica Internazionale (IMO), i partecipanti sono stati testati con sei problemi diversi: due in algebra, uno in teoria dei numeri, uno in geometria e due in combinatoria. I ricercatori di Google hanno tradotto questi problemi in linguaggio matematico formale per AlphaProof e AlphaGeometry 2. AlphaProof ha affrontato due problemi di algebra e uno di teoria dei numeri, compreso il problema più difficile della competizione, risolto da soli cinque concorrenti umani quest’anno. Nel frattempo, AlphaGeometry 2 ha risolto con successo il problema di geometria, sebbene non abbia risolto le due sfide di combinatoria.

Ogni problema all’IMO vale sette punti, per un massimo di 42. AlphaProof e AlphaGeometry 2 hanno ottenuto 28 punti, raggiungendo punteggi perfetti sui problemi che hanno risolto. Ciò li ha posizionati nella fascia alta della categoria di medaglia d’argento. La soglia per la medaglia d’oro quest’anno era di 29 punti, raggiunta da 58 dei 609 concorrenti.

Prossimo Passo: Linguaggio Naturale per Sfide Matematiche

AlphaProof e AlphaGeometry 2 hanno mostrato progressi impressionanti nelle capacità di risoluzione di problemi matematici dell’AI. Tuttavia, questi sistemi ancora dipendono da esperti umani per tradurre problemi matematici in linguaggio formale per l’elaborazione. Inoltre, non è chiaro come queste abilità matematiche specializzate potrebbero essere incorporate in altri sistemi AI, come per esplorare ipotesi, testare soluzioni innovative a problemi di lunga data e gestire efficientemente aspetti impegnativi delle dimostrazioni.

Per superare queste limitazioni, i ricercatori di Google stanno sviluppando un sistema di ragionamento del linguaggio naturale basato su Gemini e sulla loro ultima ricerca. Questo nuovo sistema mira ad avanzare le capacità di risoluzione dei problemi senza richiedere la traduzione del linguaggio formale e è progettato per integrarsi senza problemi con altri sistemi AI.

Il Punto di Partenza

La performance di AlphaProof e AlphaGeometry 2 all’Olimpiade Matematica Internazionale è un notevole passo avanti nelle capacità dell’AI di affrontare il ragionamento matematico complesso. Entrambi i sistemi hanno dimostrato un livello di medaglia d’argento, risolvendo quattro problemi su sei, mostrando progressi significativi nella dimostrazione formale e nella risoluzione di problemi geometrici. Nonostante i loro risultati, questi sistemi AI ancora dipendono dall’input umano per la traduzione dei problemi in linguaggio formale e affrontano sfide di integrazione con altri sistemi AI. La ricerca futura mira a migliorare ulteriormente questi sistemi, potenzialmente integrando il ragionamento del linguaggio naturale per estendere le loro capacità su un’ampia gamma di sfide matematiche.