notizia

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Rapporto sul cuore della macchina

Dipartimento editoriale di Machine Heart

Utilizzando il modello grande Gemini e l'algoritmo di apprendimento per rinforzo AlphaZero, puoi padroneggiare la geometria, l'algebra e la teoria dei numeri.

Per l’intelligenza artificiale le Olimpiadi della matematica non sono più un problema.

Giovedì, l'intelligenza artificiale di Google DeepMind ha compiuto un'impresa: utilizzare l'intelligenza artificiale per risolvere la vera questione delle Olimpiadi internazionali della matematica IMO di quest'anno, ed è stata solo a un passo dalla vittoria della medaglia d'oro.

Il concorso IMO che si è appena concluso la scorsa settimana prevedeva sei domande che coinvolgevano algebra, calcolo combinatorio, geometria e teoria dei numeri. Il sistema di intelligenza artificiale ibrido proposto da Google ha risposto correttamente a quattro domande e ha totalizzato 28 punti, raggiungendo il livello della medaglia d'argento.

All'inizio di questo mese, il professore di ruolo dell'UCLA Terence Tao aveva appena promosso le Olimpiadi della matematica dell'intelligenza artificiale (AIMO Progress Award) con un premio da un milione di dollari. Inaspettatamente, il livello di risoluzione dei problemi dell'intelligenza artificiale era migliorato a questo livello prima di luglio.

IMO, fai le domande contemporaneamente e risolvi correttamente le domande più difficili.

L'IMO è il concorso più antico, più grande e più prestigioso per giovani matematici, che si tiene ogni anno dal 1959. Recentemente, la competizione IMO è stata ampiamente riconosciuta come una grande sfida nel campo dell’apprendimento automatico, diventando un punto di riferimento ideale per misurare le capacità di ragionamento matematico avanzato dei sistemi di intelligenza artificiale.

Alla competizione IMO di quest'anno, AlphaProof e AlphaGeometry 2 sviluppati dal team DeepMind hanno raggiunto congiuntamente una svolta fondamentale.

Tra questi, AlphaProof è un sistema di apprendimento per rinforzo per il ragionamento matematico formale e AlphaGeometry 2 è una versione migliorata del sistema di risoluzione della geometria AlphaGeometry di DeepMind.

Questa svolta dimostra il potenziale dell’intelligenza generale artificiale (AGI) con capacità avanzate di ragionamento matematico per aprire nuove aree della scienza e della tecnologia.

Allora, come ha partecipato il sistema AI di DeepMind alla competizione IMO?

Per dirla semplicemente, questi problemi matematici vengono prima tradotti manualmente in linguaggio matematico formale in modo che il sistema di intelligenza artificiale possa comprenderli. Nella competizione ufficiale, i concorrenti umani inviano le loro risposte in due sessioni (due giorni), con un limite di tempo di 4,5 ore per ciascuna sessione. Il sistema AI composto da AlphaProof+AlphaGeometry 2 ha risolto un problema in pochi minuti, ma ha impiegato tre giorni per risolvere altri problemi. Tuttavia, se segui rigorosamente le regole, il sistema di DeepMind va in timeout. Alcune persone ipotizzano che ciò possa comportare un sacco di cracking con forza bruta.

AlphaProof ha risolto due problemi di algebra e un problema di teoria dei numeri determinando le risposte e dimostrandone la correttezza, ha affermato Google. Questi includono il problema più difficile della competizione, che solo cinque concorrenti hanno risolto all'IMO di quest'anno. E AlphaGeometry 2 dimostra un problema di geometria.

Soluzione fornita dall'intelligenza artificiale: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

La medaglia d'oro IMO e medaglia Fields Timothy Gowers e il due volte medaglia d'oro IMO Dr. Joseph Myers, presidente del Comitato di selezione dei problemi IMO 2024, hanno valutato le soluzioni fornite dal sistema combinato secondo le regole di punteggio IMO.

Ognuna delle sei domande vale 7 punti, per un punteggio totale massimo di 42 punti. Il sistema di DeepMind ha ricevuto un punteggio finale di 28, il che significa che tutti e quattro i problemi risolti hanno ricevuto punteggi perfetti, equivalenti al punteggio più alto nella categoria medaglia d'argento. La soglia della medaglia d'oro di quest'anno era di 29 punti e 58 dei 609 giocatori della competizione ufficiale hanno vinto medaglie d'oro.

Questo grafico mostra le prestazioni del sistema di intelligenza artificiale di Google DeepMind rispetto ai concorrenti umani all'IMO 2024. Il sistema ha ottenuto 28 punti su un totale di 42 punti, raggiungendo lo stesso livello della medaglia d'argento della competizione. Inoltre, quest'anno, 29 punti possono vincere la medaglia d'oro.

AlphaProof: un metodo di ragionamento formale

Tra i sistemi di intelligenza artificiale ibridi utilizzati da Google, AlphaProof è un sistema auto-addestrato che utilizza il linguaggio formale Lean per dimostrare affermazioni matematiche. Combina un modello linguistico pre-addestrato con l'algoritmo di apprendimento per rinforzo AlphaZero.

Tra questi, i linguaggi formali offrono importanti vantaggi per verificare formalmente la correttezza delle dimostrazioni del ragionamento matematico. Fino ad ora, questo è stato di utilità limitata nell’apprendimento automatico perché la quantità di dati scritti dall’uomo era molto limitata.

Al contrario, i metodi basati sul linguaggio naturale, pur avendo accesso a maggiori quantità di dati, producono passaggi intermedi di ragionamento e soluzioni che appaiono ragionevoli ma non sono corrette.

Google DeepMind costruisce un ponte tra questi due campi complementari mettendo a punto il modello Gemini per tradurre automaticamente le dichiarazioni di problemi in linguaggio naturale in dichiarazioni formali, creando così un'ampia libreria di problemi formali di varia difficoltà.

Dato un problema matematico, AlphaProof genera soluzioni candidate e poi le dimostra cercando possibili passaggi di dimostrazione in Lean. Ogni soluzione di prova trovata e verificata viene utilizzata per rafforzare il modello linguistico di AlphaProof e migliorare la sua capacità di risolvere problemi successivi più impegnativi.

Per addestrare AlphaProof, Google DeepMind ha dimostrato o confutato milioni di problemi matematici che coprivano un'ampia gamma di difficoltà e argomenti nelle settimane precedenti la competizione IMO. Durante la competizione viene anche applicato un ciclo di formazione per rafforzare la prova delle varianti del problema della competizione autogenerate fino a quando non viene trovata una soluzione completa.

Infografica sul processo del ciclo di formazione dell'apprendimento per rinforzo di AlphaProof: circa un milione di problemi matematici informali vengono tradotti in linguaggio matematico formale dalla rete formale. Il risolutore cerca quindi nella rete prove o confutazioni del problema, addestrandosi gradualmente a risolvere problemi più impegnativi utilizzando l'algoritmo AlphaZero.

AlphaGeometry 2 più competitivo

AlphaGeometry 2 è una versione notevolmente migliorata di AlphaGeometry, l'intelligenza artificiale matematica apparsa quest'anno sulla rivista Nature. Si tratta di un sistema ibrido neuro-simbolico in cui il modello linguistico è basato sui Gemelli e addestrato da zero su un ordine di grandezza di dati più sintetici rispetto al suo predecessore. Ciò aiuta il modello a risolvere problemi geometrici più impegnativi, compresi quelli relativi al movimento degli oggetti e alle equazioni di angoli, proporzioni o distanze.

AlphaGeometry 2 presenta un motore simbolico che è due ordini di grandezza più veloce del suo predecessore. Quando si incontrano nuovi problemi, nuovi meccanismi di condivisione della conoscenza consentono combinazioni avanzate di diversi alberi di ricerca per risolvere problemi più complessi.

Prima della competizione di quest'anno, AlphaGeometry 2 poteva risolvere l'83% di tutti i problemi storici di geometria IMO negli ultimi 25 anni, rispetto solo al 53% del suo predecessore. Nell'IMO 2024, AlphaGeometry 2 ha risolto il problema 4 entro 19 secondi dalla ricezione della sua formalizzazione.

Un esempio della domanda 4 richiede di dimostrare che la somma di ∠KIL e ∠XPY è uguale a 180°. AlphaGeometry 2 propone di costruire il punto E sulla retta BI tale che ∠AEB = 90°. Il punto E aiuta a dare significato al punto medio L del segmento AB, creando così molte coppie di triangoli simili, come ABE ~ YBI e ALE ~ IPC, per dimostrare la conclusione.

Google DeepMind riferisce inoltre che, come parte del lavoro dell'IMO, i ricercatori stanno anche sperimentando un nuovo sistema di ragionamento in linguaggio naturale basato su Gemini e un sistema di ragionamento in linguaggio naturale all'avanguardia, nella speranza di ottenere capacità avanzate di risoluzione dei problemi. Il sistema non richiede la traduzione delle domande in un linguaggio formale e può essere combinato con altri sistemi di intelligenza artificiale. Nel test delle domande del concorso IMO di quest'anno, "ha mostrato un grande potenziale".

Google continua a esplorare metodi di intelligenza artificiale per far avanzare il ragionamento matematico e prevede di rilasciare presto ulteriori dettagli tecnici su AlphaProof.

Siamo entusiasti di un futuro in cui i matematici utilizzeranno gli strumenti di intelligenza artificiale per esplorare ipotesi, provare nuovi approcci audaci per risolvere problemi di vecchia data e completare rapidamente elementi di dimostrazioni che richiedono molto tempo: e i sistemi di intelligenza artificiale come Gemini faranno la differenza in matematica e altro ancora.

gruppo di ricerca

Google ha affermato che la nuova ricerca è stata supportata dalle Olimpiadi internazionali della matematica e inoltre:

Lo sviluppo di AlphaProof è stato guidato da Thomas Hubert, Rishi Mehta e Laurent Sartran. I principali contributori includono Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland e Grace Margand.

Tra questi, Aja Huang, Julian Schrittwieser, Yannick Schroecker e altri membri erano anche membri principali del giornale AlphaGo 8 anni fa (2016). Otto anni fa, AlphaGo, costruito sulla base dell’apprendimento per rinforzo, divenne famoso. Otto anni dopo, l’apprendimento per rinforzo torna a brillare in AlphaProof. Qualcuno nel circolo degli amici si è lamentato: RL è tanto tornato!

AlphaGeometry 2 e il lavoro di inferenza del linguaggio naturale sono guidati da Thang Luong. Lo sviluppo di AlphaGeometry 2 è stato guidato da Trieu Trinh e Yuri Chervonyi, con importanti contributi di Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang e Marcelo Menegali.

Inoltre, David Silver, Quoc Le, Hassabis e Pushmeet Kohli sono responsabili del coordinamento e della gestione dell'intero progetto.

Contenuto di riferimento:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/