AlphaGeometry: l’IA che sfida i matematici olimpici nella geometria

AlphaGeometry è un rivoluzionario sistema di intelligenza artificiale che risolve complessi problemi di geometria a un livello paragonabile a quello di un medagliato d’oro olimpico umano.

Illustrazione di un androide bianco su sfondo blu con un chip sopra la testa (a destra) e un umano su sfondo arancione con una lampadina sopra la testa (a destra)
L’IA è stata 2,5 volte più efficace del precedente sistema all’avanguardia. (elenabsl/Shutterstock.com)

Nel mondo di oggi, essere un bambino può essere difficile. Nati troppo tardi per godere appieno di Internet e troppo presto per diventare imperatori divini in un deserto post-apocalittico basato sulla scarsità di acqua e carburante – e se cerchi di distrarti con un po’ di matematica leggera, molto probabilmente sarai comunque secondo rispetto a un robot.

“L’Olimpiade Internazionale di Matematica è un’arena moderna per i migliori matematici delle scuole superiori di tutto il mondo”, scrivono Trieu Trinh e Thang Luong, scienziati di ricerca presso Google DeepMind, nel loro articolo riguardante il loro rivoluzionario sistema di intelligenza artificiale (IA), AlphaGeometry.

AlphaGeometry è “un sistema di IA che risolve complessi problemi di geometria a un livello che si avvicina a quello di un medagliato d’oro olimpico umano – una svolta nelle prestazioni dell’IA”, annunciano. “In un test di benchmarking di 30 problemi di geometria olimpica, AlphaGeometry ha risolto 25 problemi entro il limite di tempo standard dell’Olimpiade. A confronto, il medagliato d’oro umano medio ha risolto 25,9 problemi.”

Non è solo il punteggio del sistema nella competizione che è impressionante. Sono passati quasi 50 anni dalla prima dimostrazione matematica mai effettuata da un computer – essenzialmente un lavoro di forza bruta – e da allora, il campo delle dimostrazioni assistite dal computer è progredito notevolmente.

Tuttavia, di recente, con l’avvento di cose come i big data e le tecniche avanzate di apprendimento automatico, abbiamo iniziato a vedere un cambiamento nell’uso dei computer come semplici calcolatori, verso l’intelligenza artificiale in grado di produrre dimostrazioni creative.

Il fatto che AlphaGeometry possa affrontare i tipi di problemi matematici complessi affrontati dai matematici olimpici potrebbe segnalare una tappa importante nella ricerca sull’IA, secondo Trinh e Luong.

Fino ad ora, un programma del genere avrebbe affrontato almeno due ostacoli principali. In primo luogo, i computer non sono bravi nel ragionamento o nella deduzione. In secondo luogo, la matematica è difficile da insegnare anche ai sistemi di apprendimento automatico più avanzati.

Tuttavia, AlphaGeometry affronta queste sfide combinando un modello di linguaggio neurale con un motore di deduzione simbolica. Queste ultime macchine si basano sulla logica formale e utilizzano regole chiare per arrivare a conclusioni, rendendole migliori nella deduzione razionale, ma anche lente e inflessibili.

Insieme, i due sistemi lavorano in un loop: il motore di deduzione simbolica lavora sul problema fino a quando si blocca, momento in cui il modello di linguaggio suggerisce una modifica. Era una grande teoria – c’era solo un problema. Su cosa avrebbero addestrato il modello di linguaggio?

Idealemente, il programma sarebbe stato alimentato con milioni se non miliardi di dimostrazioni geometriche create dall’uomo, che avrebbe poi potuto elaborare e restituire in vari livelli di gergo. Ma “creato dall’uomo” e “geometrico” non funzionano esattamente bene con “programma informatico”.

Quindi il team ha dovuto trovare una soluzione diversa. “Utilizzando un calcolo altamente parallelizzato, il sistema ha iniziato generando un miliardo di diagrammi casuali di oggetti geometrici e ha derivato esaustivamente tutte le relazioni tra i punti e le linee in ogni diagramma”, spiegano Trinh e Luong.

“AlphaGeometry ha trovato tutte le dimostrazioni contenute in ogni diagramma, poi ha lavorato all’indietro per scoprire quali costruzioni aggiuntive, se ce n’erano, erano necessarie per arrivare a quelle dimostrazioni”, continuano. Chiamano questo processo “deduzione simbolica e tracciamento”.

Evidentemente è stato un successo: non solo l’IA era quasi brava quanto il medagliato d’oro medio dell’IMO umano, ma era 2,5 volte più brava del sistema all’avanguardia precedente che aveva tentato la sfida.

Anche se attualmente il sistema è limitato ai problemi di geometria, Trinh e Luong sperano di espandere le capacità dell’IA matematica in molte altre discipline.

“Non stiamo facendo miglioramenti incrementali”, ha detto Trinh al Times. “Stiamo facendo un grande salto, una grande svolta in termini di risultato.”

“Solo non esagerate”, ha aggiunto.