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

L’AI di DeepMind ha fatto notevoli progressi nel ragionamento matematico nell’arco di soli un anno. Dopo aver vinto una medaglia d’argento all’Olimpiade matematica internazionale (IMO) nel 2024, il loro sistema AI ha vinto la medaglia d’oro nel 2025. Questo rapido avanzamento mette in luce le crescenti capacità dell’intelligenza artificiale nel trattare problemi complessi e astratti che richiedono creatività e intuizione simili a quelle umane. Questo articolo descriverà 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ù della semplice computazione; i partecipanti devono dimostrare una vera creatività matematica, un pensiero logico rigoroso e la capacità di costruire dimostrazioni eleganti.

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

La svolta della 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 “neuro-symbolic” AI, che combinano la forza dei grandi modelli linguistici (LLM) con la rigidezza della logica simbolica.

AlphaProof è stato progettato per dimostrare affermazioni matematiche utilizzando Lean, un linguaggio matematico formale. Ha combinato Gemini, il grande modello linguistico 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 tradurre problemi in linguaggio naturale in Lean e tentare di dimostrare passaggi logici. AlphaProof è stato addestrato su milioni di problemi di campioni 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 macchina tradizionale.

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.

Innovazioni tecniche dietro la medaglia d’oro

La transizione di DeepMind da una medaglia d’argento a una medaglia d’oro è stata guidata da diversi importanti miglioramenti tecnici.

1. Linguaggio naturale come mezzo per le dimostrazioni

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 dimostrazioni. 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 passaggi critici e produce una prova raffinata in inglese. L’apprendimento per rinforzo da feedback umano (RLHF) è stato utilizzato per premiare 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 su più pagine. In secondo luogo, utilizza un ragionamento parallelo, in cui vengono generati centinaia di thread speculativi per diverse potenziali soluzioni. Un supervisore leggero quindi classifica e promuove i percorsi più promettenti, prendendo in prestito concetti dalla ricerca dell’albero di Monte Carlo ma applicati al testo. Questo approccio mimetizza 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 l’ottimizzazione 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 contest di olimpiadi e universitari. Il corpus è stato principalmente raccolto da forum matematici pubblici, preprint di arXiv e set di problemi universitari. I mentori umani hanno esaminato gli esempi di addestramento per filtrare dimostrazioni illogiche o incomplete. L’apprendimento per rinforzo ha aiutato a raffinare il modello, spingendolo a produrre dimostrazioni concise e precise. Le prime versioni producevano dimostrazioni eccessivamente verbali, ma le penalità per frasi ridondanti hanno aiutato a ridurre l’output.

A differenza della regolazione fine convenzionale, che spesso lotta con ricompense sparse dove il feedback è binario, o la dimostrazione è 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 dimostrazione completa è rara. 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 dalla medaglia d’argento alla medaglia d’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. Questo scheduling dinamico è stato particolarmente benefico 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, era 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 prevenire la fuoriuscita di problemi ufficiali nel set di addestramento. Hanno anche filtrato i dati che contenevano soluzioni a domande di olimpiadi non pubblicate in precedenza.

Durante la competizione, Gemini Deep Think è stato fornito con i sei problemi ufficiali in formato testo normale, senza accesso a Internet. Il sistema operava su un cluster configurato per simulare la potenza computazionale 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 dimostrazioni generate sono state presentate ai coordinatori dell’IMO senza alterazioni.

Gemini Deep Think ha ottenuto punteggi perfetti sui primi cinque problemi. L’ultima domanda, che era un difficile puzzle di combinatoria, 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 una medaglia d’oro. Questo punteggio era sette punti più alto della prestazione d’argento dell’anno precedente. Gli osservatori hanno successivamente descritto le dimostrazioni dell’AI come ‘diligenti’ e ‘complete’, notando che seguivano le rigorose giustificazioni 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), dove 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, 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 dimostrazioni, l’AI libera i matematici umani per concentrarsi su lavori concettuali di livello superiore. 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.

Guardando avanti

Vincere l’oro all’IMO è un importante traguardo, ma molte sfide matematiche restano ancora fuori dalla portata degli attuali sistemi AI. Tuttavia, il rapido avanzamento dalla medaglia d’argento alla medaglia d’oro in soli un anno mette in luce il ritmo accelerato delle innovazioni e degli sviluppi dell’AI. Se questo ritmo continua, i sistemi AI potrebbero presto affrontare alcuni dei più famosi problemi irrisolti della matematica. 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 notevoli progressi nel ragionamento logico.