Per decenni, matematici e informatici hanno inseguito un obiettivo considerato visionario: costruire un’Intelligenza Artificiale capace non solo di calcolare, ma di ragionare come un matematico, scoprendo e dimostrando teoremi complessi. Questa settimana, sulle pagine della rivista Nature, Google DeepMind ha annunciato un risultato che sembra avvicinare questo traguardo: il sistema AlphaProof ha ottenuto una performance equivalente a quella di un medagliato d’argento all’IMO 2024, la più prestigiosa competizione matematica mondiale per studenti di eccellenza.
Perché è una rivoluzione?
Molte IA moderne, incluse quelle basate su modelli linguistici come ChatGPT, GPT-4/5 o Gemini, sono in grado di produrre spiegazioni e soluzioni matematiche in linguaggio naturale. Tuttavia, non è garantito che queste soluzioni siano corrette, proprio perché il linguaggio naturale tollera ambiguità. L’interpretazione umana può essere sbagliata, e i modelli possono “inventare” passaggi. AlphaProof invece evita questo problema alla radice: opera all’interno di un sistema matematico formale, il proof assistant Lean, dove ogni singolo passo logico della dimostrazione viene verificato automaticamente dal sistema. Non c’è spazio per la fantasia: o la prova è corretta, o fallisce.
Come funziona AlphaProof?
Secondo quanto descritto negli articoli tecnici e nei materiali supplementari, AlphaProof combina:
- Apprendimento rinforzato (RL), come AlphaZero (il sistema che ha sconfitto i campioni mondiali di Go).
- Un modello transformer da 3 miliardi di parametri.
- Un enorme dataset auto-formalizzato, composto da circa 80 milioni di enunciati matematici convertiti automaticamente in linguaggio Lean.
L’addestramento avviene in tre fasi:
- Pre-training su testo matematico e codice (≈300 miliardi di token).
- Fine-tuning supervisionato su prove esistenti della libreria matematica ufficiale Mathlib.
- Reinforcement Learning su vasta scala, in cui AlphaProof prova e riprova milioni di teoremi, migliorando autonomamente la propria strategia.
La mossa decisiva: il Test-Time RL (TTRL)
Quando AlphaProof incontra un problema difficile, non si limita a cercare la soluzione: genera varianti formali dello stesso problema e si allena sul momento per imparare a risolverlo. Questo può richiedere giorni di calcolo, ma funziona: è così che il sistema è riuscito a risolvere alcuni dei problemi più difficili dell’IMO 2024, inclusi problemi che solo pochi concorrenti umani hanno saputo risolvere.
I risultati all’IMO 2024
Il sistema combinato:
- AlphaProof (per algebra e teoria dei numeri),
- AlphaGeometry 2 (per geometria)
ha risolto 4 problemi su 6, totalizzando 28 punti su 42, cioè il punteggio equivalente a una medaglia d’argento.
È la prima volta nella storia che un’IA ottiene un risultato di livello medaglia in un’IMO reale.
Limiti attuali
Gli stessi ricercatori riconoscono che:
- AlphaProof non è ancora competitivo nei tempi umani (richiede molte ore o giorni per problema).
- Alcune aree matematiche più “creative” o teoriche restano difficili.
- Solo pochi gruppi al mondo hanno l’infrastruttura di calcolo per addestrare sistemi di queste dimensioni.
Vuoi ricevere le notifiche sulle nostre notizie più importanti?