Dall’argento all’oro: come l’AI di DeepMind ha conquistato l’Olimpiade matematica

L’AI di DeepMind ha fatto progressi notevoli nel ragionamento matematico nell’arco di un solo anno. Dopo aver vinto la medaglia d’argento all’Olimpiade matematica internazionale (IMO) nel 2024, il sistema AI ha vinto la medaglia d’oro nel 2025. Questo rapido progresso mette in evidenza le crescenti capacità dell’intelligenza artificiale nel risolvere problemi complessi e astratti che richiedono creatività e intuizione umana. Questo articolo esaminerà come DeepMind abbia raggiunto questa trasformazione, le scelte tecniche e strategiche dietro di essa e le più ampie implicazioni di questi progressi.

Il significato dell’IMO

L’Olimpiade matematica internazionale, fondata nel 1959, è riconosciuta a livello globale come la principale competizione matematica per studenti delle scuole superiori. Ogni anno, gli studenti migliori di tutto il mondo affrontano sei problemi impegnativi in algebra, geometria, teoria dei numeri e combinatoria. Risolvere questi problemi richiede molto più che calcoli; i partecipanti devono mostrare una vera creatività matematica, un pensiero logico rigoroso e la capacità di costruire prove eleganti.

Per l’intelligenza artificiale, l’IMO presenta una sfida unica. Mentre l’AI ha padroneggiato il riconoscimento di modelli, l’analisi dei dati e persino giochi complessi come Go e scacchi, la matematica olimpica richiede ragionamento astratto e creativo e la sintesi di nuove idee, abilità tradizionalmente considerate marchi di fabbrica dell’intelligenza umana. Di conseguenza, l’IMO è diventata una prova naturale per valutare quanto l’AI sia vicina a raggiungere un ragionamento veramente simile a quello umano.

La medaglia d’argento del 2024

Nel 2024, DeepMind ha introdotto due sistemi AI per affrontare problemi di livello IMO: AlphaProof e AlphaGeometry 2. Entrambi i sistemi sono esempi di “intelligenza neuro-simbolica“, che combina la forza dei grandi modelli linguistici (LLM) con la rigore della logica simbolica.

AlphaProof è stato progettato per dimostrare affermazioni matematiche utilizzando Lean, un linguaggio matematico formale. Ha combinato Gemini, il modello linguistico di grandi dimensioni di DeepMind, con AlphaZero, che è un motore di apprendimento per rinforzo noto per il suo successo nei giochi da tavolo. In questo contesto, il ruolo di Gemini era quello di tradurre problemi in linguaggio naturale in Lean e tentare di dimostrarli generando passaggi logici. AlphaProof è stato addestrato su milioni di problemi di esempio che coprono diverse discipline e difficoltà matematiche. Il sistema si è migliorato tentando di dimostrare affermazioni sempre più complesse, simile a come AlphaZero ha imparato giocando contro se stesso.

AlphaGeometry 2 è stato progettato per risolvere problemi di geometria. Qui, la comprensione del linguaggio di Gemini ha abilitato l’AI a prevedere costruzioni ausiliarie utili, mentre un motore di ragionamento simbolico gestiva le deduzioni logiche. Questo approccio ibrido ha permesso ad AlphaGeometry di affrontare problemi geometrici ben al di là della portata del ragionamento tradizionale delle macchine.

Insieme, questi sistemi hanno risolto quattro problemi su sei dell’IMO: due in algebra, uno in teoria dei numeri e uno in geometria, raggiungendo un punteggio di 28 su 42. Questa prestazione è stata un importante traguardo, poiché è stato il primo caso in cui un’AI ha raggiunto il livello di medaglia d’argento all’IMO. Tuttavia, questo successo si è basato fortemente su esperti umani per tradurre i problemi in linguaggi matematici formali. Hanno anche richiesto enormi risorse computazionali, che hanno richiesto giorni di tempo di elaborazione per ogni problema.

Le innovazioni tecniche dietro la medaglia d’oro

Il passaggio di DeepMind da una medaglia d’argento a una medaglia d’oro è stato guidato da diverse importanti innovazioni tecniche.

1. Il linguaggio naturale come mezzo per le prove

Il cambiamento più significativo è stato lo spostamento da sistemi che richiedevano traduzioni di esperti in linguaggi formali al trattamento del linguaggio naturale come mezzo per le prove. Questo spostamento è stato realizzato attraverso una versione migliorata di Gemini dotata di capacità Deep Think. Invece di convertire i problemi in Lean, il modello elabora il testo direttamente, genera abbozzi informali, formalizza internamente i passaggi critici e produce una prova raffinata in inglese. L’apprendimento per rinforzo da feedback umano (RLHF) è stato utilizzato per premiare le soluzioni che erano logicamente coerenti, brevi e presentate.

Gemini Deep Think differisce dalla versione pubblica di Gemini in due modi principali. In primo luogo, assegna finestre di contesto più lunghe e più token di calcolo per query, il che consente al modello di mantenere catene di pensiero multipagina. In secondo luogo, utilizza il ragionamento parallelo, in cui vengono generati centinaia di thread speculativi per diverse soluzioni potenziali. Un supervisore leggero classifica e promuove i percorsi più promettenti, prendendo in prestito concetti dalla ricerca dell’albero di Monte Carlo ma applicati al testo. Questo approccio imita il modo in cui i team umani brainstorming, scartano idee non produttive e convergono su soluzioni eleganti.

2. Addestramento e apprendimento per rinforzo

L’addestramento di Gemini Deep Think ha comportato la fine-tuning del modello per prevedere i passaggi successivi invece delle risposte finali. A questo scopo, è stato compilato un corpus di 100.000 soluzioni di alta qualità di problemi olimpici e di concorso universitario. Il corpus è stato principalmente raccolto da forum matematici pubblici, pre-stampe arXiv e set di problemi universitari. I mentori umani hanno esaminato gli esempi di addestramento per filtrare le prove illogiche o incomplete. L’apprendimento per rinforzo ha aiutato a raffinare il modello, spingendolo a produrre prove concise e precise. Le prime versioni producevano prove eccessivamente verbali, ma le penalità sulle frasi ridondanti hanno aiutato a ridurre l’output.

A differenza della fine-tuning convenzionale, che spesso lotta con ricompense sparse in cui il feedback è binario, o la prova è corretta o no. DeepMind ha implementato un sistema di ricompensa passo-passo, in cui ogni sottolemma verificato ha contribuito al punteggio complessivo. Questo meccanismo di ricompensa guida Gemini anche quando la prova completa è infrequente. Il processo di addestramento è durato tre mesi e ha utilizzato circa 25 milioni di ore TPU.

3. Massiva parallelizzazione

La parallelizzazione ha anche svolto un ruolo critico nel progresso di DeepMind da argento a oro. Ogni problema ha generato più rami di ragionamento in parallelo, con risorse che si spostavano dinamicamente verso percorsi più promettenti quando altri si bloccavano. Questa pianificazione dinamica è stata particolarmente utile per i problemi di combinatoria, che hanno grandi spazi di soluzione. L’approccio è simile a come gli esseri umani testano disuguaglianze ausiliarie prima di impegnarsi in una completa induzione. Sebbene questa tecnica fosse computazionalmente costosa, è stata gestibile utilizzando i cluster TPU v5 di DeepMind.

DeepMind all’IMO 2025

Per mantenere l’integrità della competizione, DeepMind ha congelato i pesi del modello tre settimane prima dell’IMO per evitare la fuoriuscita di problemi ufficiali nel set di addestramento. Hanno anche filtrato i dati che contenevano soluzioni a problemi olimpici non pubblicati in precedenza.

Durante la competizione, Gemini Deep Think è stato fornito con i sei problemi ufficiali in formato testo semplice, senza accesso a Internet. Il sistema è stato eseguito su un cluster configurato per simulare la potenza di calcolo di un laptop standard per processo. L’intero processo di risoluzione dei problemi è stato completato in meno di tre ore, ben entro i limiti di tempo. Le prove generate sono state inviate ai coordinatori dell’IMO senza alterazioni.

Gemini Deep Think ha ottenuto punteggi perfetti sui primi cinque problemi. L’ultima domanda, che era un rompicapo di combinatoria impegnativo, tuttavia, ha bloccato sia l’AI che il 94% dei partecipanti umani. Nonostante ciò, l’AI ha terminato con un punteggio totale di 35/42 per assicurarsi la medaglia d’oro. Questo punteggio è stato sette punti più alto della prestazione d’argento dell’anno precedente. Gli osservatori hanno successivamente descritto le prove dell’AI come ‘diligenti’ e ‘complete’, notando che seguivano le giustificazioni rigorose attese dai concorrenti umani.

Implicazioni per l’AI e la matematica

Il risultato di DeepMind è un importante traguardo sia per l’AI che per la matematica. Per l’AI, padroneggiare l’IMO è un passo verso l’intelligenza artificiale generale (AGI), in cui i sistemi possono eseguire qualsiasi compito intellettuale che un essere umano possa eseguire. Risolvere problemi matematici complessi richiede ragionamento e comprensione, che sono componenti fondamentali dell’intelligenza generale. Questo successo indica che l’AI sta facendo progressi verso abilità cognitive più simili a quelle umane.

Per la matematica, i sistemi AI come Gemini Deep Think possono diventare strumenti inestimabili per i matematici. Possono aiutare nell’esplorazione di nuove aree, nella verifica di congetture e persino nella scoperta di nuovi teoremi. Automatizzando gli aspetti più tediosi della costruzione delle prove, l’AI libera i matematici umani per concentrarsi sul lavoro concettuale di alto livello. Inoltre, le tecniche sviluppate per questi sistemi AI potrebbero ispirare nuovi metodi nella ricerca matematica che potrebbero non essere possibili attraverso lo sforzo umano solo.

Tuttavia, il progresso dell’AI nella matematica solleva anche domande sul ruolo dell’AI negli ambienti educativi e nelle competizioni. Man mano che le capacità dell’AI continuano a crescere, ci saranno dibattiti su come il suo coinvolgimento potrebbe alterare la natura dell’istruzione e della competizione matematica.

Guardando avanti

Vincere la medaglia d’oro all’IMO è un importante traguardo, ma molte sfide matematiche rimangono ancora fuori dalla portata degli attuali sistemi AI. Tuttavia, il rapido progresso da argento a oro in soli un anno mette in evidenza il ritmo accelerato delle innovazioni e degli sviluppi dell’AI. Se questo ritmo continua, i sistemi AI potrebbero presto affrontare alcuni dei problemi matematici più famosi irrisolti. Mentre la questione se l’AI sostituirà o migliorerà la creatività umana rimane irrisolta, l’IMO del 2025 è un chiaro indicatore che l’intelligenza artificiale ha fatto importanti passi avanti nel ragionamento logico.