La notizia non arriva completamente a sorpresa: alcuni segnali, alcune anticipazioni erano nell’aria da alcuni mesi. Ma sapere che un’intelligenza artificiale è riuscita a risolvere correttamente 4 problemi dei 6 dell’ultima Olimpiade Internazionale di Matematica (IMO) fa comunque un certo effetto. Ce ne parla Luigi Amedeo Bianchi.

Se avesse partecipato come essere umano, il progetto di Google DeepMind avrebbe vinto una medaglia d’argento, direttamente sul cut-off (con un punto in più sarebbe stata d’oro). Il risultato è eccezionale! Ma andiamo a guardare qualche dettaglio in più.

Innanzitutto perché parlare di “progetto” e non di IA di Google DeepMind? La precisazione è necessaria perché sono stati usati due diversi sistemi: AlphaGeometry per il problema di geometria e AlphaProof per gli altri. AlphaGeometry aveva già dato notizia lo scorso gennaio, quando una versione preliminare aveva risolto buona parte dei problemi di geometria delle vecchie edizioni delle Olimpiadi. Dei due sistemi è stato in qualche modo quello di maggior successo: una volta “letto” il problema lo ha risolto in 19 secondi.

Anche qui ci sono alcune informazioni da mettere in evidenza. La prima è che il problema di geometria era il numero 4, ossia il problema “più semplice” del secondo giorno di gara (per gli esseri umani concorrenti). La seconda è specificare cosa intendiamo con “letto”.

Per approfondire questo aspetto, passiamo al secondo sistema: AlphaProof, di sono state condivise le soluzioni. Per poter affrontare i problemi, AlphaProof ha avuto bisogno di qualche concessione. Innanzitutto non ha avuto i vincoli temporali degli esseri umani in gara e ha quindi potuto consegnare le sue risposte dopo 3 giorni invece che dopo 4 ore e mezza. Inoltre i problemi, proposti in linguaggio naturale (ossia nel linguaggio che usiamo normalmente) agli umani, sono stati tradotti in linguaggio formalizzato (in Lean, per chi avesse curiosità in merito) dagli “assistenti umani” prima di essere dati in pasto all’intelligenza artificiale.

Gli sviluppatori hanno sottolineato due aspetti di questo “pre-processing” del testo. Da un lato non è stata scelta la via “facile”, ossia dichiarare già il risultato da dimostrare, ma è stata posta la domanda in maniera formalizzata ma aperta, con alcune accortezze per evitare che l’IA modificasse la natura del problema. Dall’altro già ora nella fase di allenamento di AlphaProof è coinvolto un “formalizzatore” automatico basato su Gemini, che prende in pasto problemi in linguaggio naturale e li formalizza in Lean. È previsto che in futuro anche la parte di formalizzazione sia automatizzata, ma per evitare che un errore in questa prima fase inficiasse tutta la parte successiva, gli sviluppatori hanno preferito concentrarsi sulla parte di risoluzione e non sulla parte della formalizzazione.

Particolarmente interessante è che l’allenamento non è stato fatto solamente prima della gara (cosa vera anche per gli umani in gara), ma anche durante la competizione, con AlphaProof che ha generato varianti dei problemi proposti, tentando di risolverli, adottando in un certo senso una delle euristiche di Polya per la soluzione di problemi.

Per quanto riguarda i punti fatti: AlphaGeometry e AlphaProof hanno fatto punteggio pieno sui 4 problemi su 6 che sono riusciti a risolvere: AlphaGeometry per geometria, come detto, e AlphaProof per Algebra e Teoria dei Numeri. Sono rimasti fuori il problema 3, il più difficile del primo giorno, e il problema 5. La loro caratteristica comune? Essere problemi di Combinatoria. Questi sono noti per essere spesso particolarmente subdoli da formalizzare (anche per gli esseri umani: è molto facile perdere punti in un problema di combinatoria, se la valutazione è “rigorosa”) e per richiedere spesso strategie risolutive “ad hoc”.

Insomma, è un evento storico, ma come riconosciuto anche dagli stessi team di Google DeepMind, il sistema non è ancora perfetto, non ha ancora raggiunto capacità umane o superumane, come accaduto in passato con AlphaGo per il Go e con AlphaZero per gli scacchi.

Per chi volesse saperne di più, rimandiamo al blog post con cui DeepMind ha annunciato il risultato e a un articolo (paywalled) del New York Times in merito, oltre a segnalare anche l’interessante discussione della comunità Lean.

Immagine di copertina creata con Microsoft Copilot in Bing