Ricerca
Il nostro sistema di intelligenza artificiale supera l’approccio all’avanguardia per i problemi di geometria, facendo avanzare il ragionamento dell’intelligenza artificiale in matematica
Riflettendo lo spirito olimpico dell’antica Grecia, le Olimpiadi Internazionali della Matematica è un’arena moderna per i matematici delle scuole superiori più brillanti del mondo. Il concorso non solo mette in mostra i giovani talenti, ma è emerso come un banco di prova per sistemi di intelligenza artificiale avanzati in matematica e ragionamento.
In un articolo pubblicato oggi in Naturapresentiamo AlphaGeometry, un sistema di intelligenza artificiale che risolve problemi di geometria complessi a un livello che si avvicina a quello di una medaglia d’oro alle Olimpiadi umane: una svolta nelle prestazioni dell’IA. In un test di benchmarking di 30 problemi di geometria delle Olimpiadi, AlphaGeometry ne ha risolti 25 entro il limite di tempo standard delle Olimpiadi. Per fare un confronto, il precedente sistema all’avanguardia ha risolto 10 di questi problemi di geometria e la medaglia d’oro umana media ha risolto 25,9 problemi.
Nel nostro set di benchmarking di 30 problemi di geometria delle Olimpiadi (IMO-AG-30), compilato dalle Olimpiadi dal 2000 al 2022, AlphaGeometry ha risolto 25 problemi entro i limiti di tempo della competizione. Questo si sta avvicinando al punteggio medio delle medaglie d’oro umane su questi stessi problemi. Il precedente approccio all’avanguardia, noto come “metodo Wu”, ha risolto 10.
I sistemi di intelligenza artificiale spesso lottano con problemi complessi di geometria e matematica a causa della mancanza di capacità di ragionamento e di dati di addestramento. Il sistema di AlphaGeometry combina il potere predittivo di un modello di linguaggio neurale con un motore di deduzione vincolato a regole, che lavorano in tandem per trovare soluzioni. E sviluppando un metodo per generare un vasto pool di dati di addestramento sintetici – 100 milioni di esempi unici – possiamo addestrare AlphaGeometry senza alcuna dimostrazione umana, aggirando il collo di bottiglia dei dati.
Con AlphaGeometry, dimostriamo la crescente capacità dell’intelligenza artificiale di ragionare in modo logico e di scoprire e verificare nuove conoscenze. Risolvere problemi di geometria a livello olimpico è una pietra miliare importante nello sviluppo di un ragionamento matematico profondo nel percorso verso sistemi di intelligenza artificiale più avanzati e generali. Stiamo rendendo open source il file Codice e modello AlphaGeometrye spero che, insieme ad altri strumenti e approcci alla generazione e alla formazione di dati sintetici, aiuti ad aprire nuove possibilità in matematica, scienza e intelligenza artificiale.
Per me ha perfettamente senso ora che i ricercatori nel campo dell’intelligenza artificiale stiano provando prima i problemi di geometria dell’IMO perché trovare soluzioni per loro funziona un po’ come gli scacchi, nel senso che abbiamo un numero piuttosto piccolo di mosse sensate ad ogni passo. Ma trovo ancora sorprendente che siano riusciti a farlo funzionare. È un risultato impressionante.
Ngo Bao Chau, medaglia Fields e medaglia d’oro IMO
AlphaGeometry adotta un approccio neuro-simbolico
AlphaGeometry è un sistema neuro-simbolico costituito da un modello di linguaggio neurale e un motore di deduzione simbolica, che lavorano insieme per trovare prove di teoremi di geometria complessi. Simile all’idea di “pensare, veloce e lento“, un sistema fornisce idee veloci e “intuitive” e l’altro un processo decisionale più deliberato e razionale.
Poiché i modelli linguistici eccellono nell’identificare modelli e relazioni generali nei dati, possono prevedere rapidamente costrutti potenzialmente utili, ma spesso non hanno la capacità di ragionare in modo rigoroso o di spiegare le proprie decisioni. I motori di deduzione simbolica, invece, si basano sulla logica formale e utilizzano regole chiare per arrivare a conclusioni. Sono razionali e spiegabili, ma possono essere “lenti” e inflessibili, soprattutto quando si affrontano da soli problemi grandi e complessi.
Il modello linguistico di AlphaGeometry guida il suo motore di deduzione simbolica verso soluzioni probabili ai problemi di geometria. I problemi di geometria delle Olimpiadi si basano su diagrammi che richiedono l’aggiunta di nuovi costrutti geometrici prima di poter essere risolti, come punti, linee o cerchi. Il modello linguistico di AlphaGeometry prevede quali nuovi costrutti sarebbe più utile aggiungere, da un numero infinito di possibilità. Questi indizi aiutano a colmare le lacune e consentono al motore simbolico di fare ulteriori deduzioni sul diagramma e di avvicinarsi alla soluzione.
AlphaGeometry risolve un problema semplice: dato il diagramma del problema e le sue premesse del teorema (a sinistra), AlphaGeometry (al centro) utilizza prima il suo motore simbolico per dedurre nuove istruzioni sul diagramma finché non viene trovata la soluzione o finché le nuove istruzioni non vengono esaurite. Se non viene trovata alcuna soluzione, il modello linguistico di AlphaGeometry aggiunge un costrutto potenzialmente utile (blu), aprendo nuovi percorsi di deduzione per il motore simbolico. Questo ciclo continua finché non viene trovata una soluzione (a destra). In questo esempio è richiesto un solo costrutto.
AlphaGeometry risolve un problema delle Olimpiadi: problema 3 delle Olimpiadi internazionali di matematica del 2015 (a sinistra) e una versione condensata della soluzione di AlphaGeometry (a destra). Gli elementi blu sono costrutti aggiunti. La soluzione di AlphaGeometry ha 109 passaggi logici.
Generazione di 100 milioni di esempi di dati sintetici
La geometria si basa sulla comprensione dello spazio, della distanza, della forma e delle posizioni relative ed è fondamentale per l’arte, l’architettura, l’ingegneria e molti altri campi. Gli esseri umani possono imparare la geometria usando carta e penna, esaminando diagrammi e utilizzando le conoscenze esistenti per scoprire proprietà e relazioni geometriche nuove e più sofisticate. Il nostro approccio alla generazione di dati sintetici emula questo processo di costruzione della conoscenza su larga scala, permettendoci di addestrare AlphaGeometry da zero, senza alcuna dimostrazione umana.
Utilizzando un calcolo altamente parallelizzato, il sistema ha iniziato generando un miliardo di diagrammi casuali di oggetti geometrici e ha derivato in modo esaustivo tutte le relazioni tra i punti e le linee in ciascun diagramma. AlphaGeometry ha trovato tutte le dimostrazioni contenute in ciascun diagramma, quindi ha lavorato a ritroso per scoprire quali costrutti aggiuntivi, se ce ne fossero, fossero necessari per arrivare a quelle dimostrazioni. Chiamiamo questo processo “deduzione simbolica e tracciabilità”.
Rappresentazioni visive dei dati sintetici generati da AlphaGeometry
Quell’enorme pool di dati è stato filtrato per escludere esempi simili, risultando in un set di dati di addestramento finale di 100 milioni di esempi unici di varia difficoltà, di cui nove milioni presentavano costrutti aggiunti. Con così tanti esempi di come questi costrutti abbiano portato a dimostrazioni, il modello linguistico di AlphaGeometry è in grado di fornire buoni suggerimenti per nuovi costrutti quando vengono presentati problemi di geometria delle Olimpiadi.
Ragionamento matematico pionieristico con l’intelligenza artificiale
La soluzione a ogni problema delle Olimpiadi fornita da AlphaGeometry è stata controllata e verificata dal computer. Abbiamo anche confrontato i suoi risultati con i precedenti metodi di intelligenza artificiale e con le prestazioni umane alle Olimpiadi. Inoltre, Evan Chen, allenatore di matematica ed ex medaglia d’oro alle Olimpiadi, ha valutato per noi una selezione di soluzioni AlphaGeometry.
Chen ha affermato: “Il risultato di AlphaGeometry è impressionante perché è sia verificabile che pulito. Le precedenti soluzioni di intelligenza artificiale ai problemi di concorrenza basati su prove sono state talvolta incostanti (i risultati sono corretti solo a volte e necessitano di controlli umani). AlphaGeometry non ha questo punto debole: le sue soluzioni hanno una struttura verificabile dalla macchina. Eppure, nonostante ciò, il suo risultato è ancora leggibile dall’uomo. Si sarebbe potuto immaginare un programma per computer in grado di risolvere problemi di geometria mediante sistemi di coordinate a forza bruta: si pensi a pagine e pagine di noiosi calcoli algebrici. AlphaGeometry non è questo. Utilizza le regole della geometria classica con angoli e triangoli simili proprio come fanno gli studenti.
Il risultato di AlphaGeometry è impressionante perché è verificabile e pulito… Utilizza le regole della geometria classica con angoli e triangoli simili proprio come fanno gli studenti.
Evan Chen, allenatore di matematica e medaglia d’oro alle Olimpiadi
Poiché ogni Olimpiade prevede sei problemi, solo due dei quali sono tipicamente incentrati sulla geometria, AlphaGeometry può essere applicata solo a un terzo dei problemi di una determinata Olimpiade. Tuttavia, la sua capacità geometrica da sola lo rende il primo modello AI al mondo in grado di superare la soglia della medaglia di bronzo dell’IMO nel 2000 e nel 2015.
In geometria, il nostro sistema si avvicina allo standard di una medaglia d’oro dell’IMO, ma puntiamo a un premio ancora più grande: far avanzare il ragionamento per i sistemi di intelligenza artificiale di prossima generazione. Considerato il potenziale più ampio dell’addestramento dei sistemi di intelligenza artificiale da zero con dati sintetici su larga scala, questo approccio potrebbe modellare il modo in cui i sistemi di intelligenza artificiale del futuro scoprono nuove conoscenze, in matematica e oltre.
AlphaGeometry si basa sul lavoro di Google DeepMind e Google Research per aprire la strada al ragionamento matematico con l’intelligenza artificiale esplorare la bellezza della matematica pura A risolvere problemi matematici e scientifici con modelli linguistici. E più recentemente, abbiamo introdotto FunSearchche ha fatto le prime scoperte su problemi aperti nelle scienze matematiche utilizzando Large Language Models.
Il nostro obiettivo a lungo termine resta quello di costruire sistemi di intelligenza artificiale in grado di generalizzarsi in tutti i campi matematici, sviluppando la sofisticata risoluzione dei problemi e il ragionamento da cui dipenderanno i sistemi di intelligenza artificiale generali, estendendo nel contempo le frontiere della conoscenza umana.
Fonte: deepmind.google
