AlphaProof — DeepMind Risolve i Problemi della IMO 2024 al Livello di Medaglia d'Argento

Cos'è: AlphaProof è un sistema AI di DeepMind, presentato al pubblico il 25 luglio 2024 insieme alla versione aggiornata AlphaGeometry 2. Combinato con AlphaGeometry 2, ha risolto 4 dei 6 problemi della International Mathematical Olympiad 2024 — il più prestigioso concorso matematico per studenti pre-universitari — ottenendo 28 punti su 42 possibili, esattamente la soglia della medaglia d'argento. È la prima volta che un sistema AI raggiunge un livello da medaglia in una IMO, e lo fa producendo dimostrazioni completamente formali, verificate da un proof assistant.

L'IMO e il significato del benchmark

La International Mathematical Olympiad è la competizione matematica internazionale per studenti delle scuole superiori più antica e prestigiosa, in corso dal 1959. Ogni anno i sei migliori studenti di un centinaio di paesi affrontano 6 problemi distribuiti su due giornate, con 4 ore e 30 minuti per giornata. I problemi non testano conoscenza enciclopedica ma creatività dimostrativa: ogni problema richiede di trovare un'argomentazione originale, spesso usando trucchi e insight non riconducibili a procedure meccaniche.

Il punteggio massimo è 42 (7 punti per problema). La medaglia d'oro richiede tipicamente 29-35 punti, la medaglia d'argento 22-28, la bronzo 16-21. Nel 2024 a Bath, Regno Unito, AlphaProof + AlphaGeometry 2 hanno totalizzato 28 punti: la soglia esatta del confine argento/oro. Solo 58 dei 609 partecipanti umani hanno fatto meglio. Il sistema ha risolto due problemi di algebra, uno di teoria dei numeri (P1, considerato il più difficile dell'esame) e uno di geometria, fallendo solo i due problemi di combinatoria.

Architettura: Lean, Gemini, AlphaZero search

AlphaProof si articola su tre componenti che lavorano in concerto. Il primo è Lean, un proof assistant moderno sviluppato da Leonardo de Moura: un linguaggio formale in cui le dimostrazioni matematiche sono espresse come programmi tipizzati che il sistema verifica automaticamente. Se Lean accetta una dimostrazione, è matematicamente corretta — non c'è spazio per allucinazioni o passaggi sbagliati nascosti. Lean è già usato dalla comunità matematica reale: Terence Tao e Kevin Buzzard hanno guidato sforzi di formalizzazione di interi corpi di matematica avanzata in Lean.

Il secondo componente è una versione di Gemini fine-tuned per autoformalizzazione: prendere il testo informale di un problema in inglese e tradurlo nella sintassi Lean formale. Questo passaggio è non triviale: i problemi IMO sono scritti in linguaggio matematico naturale denso di convenzioni implicite, e la traduzione in Lean richiede di esplicitare tipi, ipotesi, dominio delle variabili. DeepMind riferisce di aver generato circa un milione di varianti formalizzate di problemi pubblici per addestrare questa componente.

Il terzo componente è il solver in stile AlphaZero: data una proposizione da dimostrare in Lean, il sistema esplora alberi di possibili passi di dimostrazione (applicare un lemma, fare una case split, introdurre una variabile), guidato da una rete neurale che valuta la promessa di ogni ramo. È lo stesso paradigma che ha funzionato per gli scacchi e Go: ricerca ad albero combinata con valutazione neurale. Solo che qui le foglie dell'albero sono dimostrazioni terminate verificate da Lean.

AlphaGeometry 2 e la divisione di lavoro

I problemi di geometria della IMO seguono uno stile particolare e meritano un sistema dedicato. AlphaGeometry 2 è il successore di AlphaGeometry pubblicato a gennaio 2024 su Nature: combina un motore simbolico classico (deduzione su fatti geometrici come "i triangoli ABC e DEF sono simili") con un LLM che propone costruzioni ausiliarie creative (tracciare una linea, costruire un punto medio, considerare una circonferenza specifica). Le costruzioni ausiliarie sono ciò che rende difficile la geometria olimpica per gli AI classici: aggiungere oggetti non presenti nell'enunciato è un atto creativo che non si riduce a inferenza meccanica.

Nella IMO 2024, AlphaGeometry 2 ha risolto il problema di geometria (P4) in meno di 20 secondi. AlphaProof si è occupato degli altri tre problemi risolti — uno di teoria dei numeri e due di algebra — impiegando da minuti a tre giorni per problema. Per confronto, i partecipanti umani hanno 4 ore e 30 minuti per ogni sessione di tre problemi: AlphaProof ha quindi usato molto più tempo degli studenti, ma producendo dimostrazioni formali verificate. La differenza qualitativa non va sottovalutata.

Tim Gowers e la validazione esperta

Le soluzioni di AlphaProof e AlphaGeometry 2 sono state valutate ufficialmente da due matematici esperti: Tim Gowers, medaglia Fields 1998 e già allenatore della squadra britannica IMO, e Joseph Myers, due volte medaglia d'oro IMO e attuale presidente del comitato problemi. Hanno applicato esattamente i criteri usati per gli studenti umani. Il fatto che le dimostrazioni siano in Lean — formali, verificabili da macchina — ha reso la valutazione tecnicamente più semplice ma concettualmente più stringente: non c'era spazio per "argomento generalmente corretto ma con un gap": o la dimostrazione passa il type-checker di Lean, o non vale.

Gowers ha dichiarato pubblicamente che il livello dimostrato è "genuinamente impressionante" e che i problemi IMO non possono più essere considerati al di fuori della portata dei sistemi AI. Ha anche sottolineato le limitazioni: AlphaProof è specialistico, non generalista; richiede problemi formalizzati in Lean; non risolve combinatoria; non genera ancora congetture nuove o problemi originali. Ma il muro psicologico dell'IMO — un benchmark stabilito da 65 anni come misura dell'eccellenza matematica giovanile — è stato infranto.

Confronto con o1 e implicazioni sul reasoning AI

Settembre 2024, OpenAI rilascia o1: un modello che usa "chain-of-thought" estesa durante l'inferenza per affrontare problemi di reasoning, e ottiene 83,3% sul benchmark MATH e 13,4% sull'AIME (American Invitational Mathematics Examination, livello sotto IMO). I due approcci — o1 e AlphaProof — rappresentano due filosofie diverse del reasoning AI:

• o1 e chain-of-thought: il modello pensa in linguaggio naturale, produce passi intermedi, arriva a una risposta. È flessibile, generalista, applicabile a qualunque dominio. Ma le sue dimostrazioni non sono verificate: può convincersi (e convincere l'utente) di passaggi sbagliati. Su problemi formali genera spesso "fake proofs" — argomentazioni che suonano corrette ma contengono errori sottili.
• AlphaProof e formal verification: il modello produce output che il proof assistant verifica. È specialistico, richiede problemi formalizzati, è più lento. Ma le dimostrazioni che produce sono matematicamente certe: zero allucinazioni possibili al livello logico.

La direzione di ricerca più interessante è la combinazione: usare LLM per generare candidati di ragionamento e proof assistant per verificarli. Questo paradigma — già implicito in AlphaProof — promette reasoning AI affidabile in domini dove la verifica è possibile (matematica, parti del software engineering, parti della fisica teorica). Resta aperto il problema dei domini dove la verifica formale non è disponibile, cioè la maggior parte del mondo reale.

Il rilascio di AlphaProof a luglio 2024 ha riposizionato il dibattito sul reasoning AI da "i modelli possono ragionare?" a "i modelli possono ragionare in modo verificabile?". La risposta a questa seconda domanda è meno entusiasmante come marketing, ma è più scientificamente solida — ed è probabilmente la più rilevante per il futuro a lungo termine dell'AI applicata a problemi critici.

---