Dopo che Google DeepMind ha sconfitto le persone in tutto, da Game vai ai giochi di tavolo strategica ,
Ora afferma di essere sul punto di battere i migliori studenti del mondo quando si risolvono le attività di matematica.

The London con sede a Londra Machine-Learning La società ha annunciato il 25 luglio che i suoi sistemi di intelligenza artificiale (KI) hanno risolto quattro dei sei compiti che sono stati assegnati agli studenti alle Olimpiadi di matematica internazionale (IMO) 2024 a Bath, Gran Bretagna. L'intelligenza artificiale ha fornito prove rigorose e graduali, che sono state valutate da due principali matematiche e ha ottenuto un punteggio di solo un punto 28/42 dall'area delle medaglie d'oro.

"È ovviamente un progresso molto importante", afferma Joseph Myers, matematico di Cambridge, in Gran Bretagna, che, insieme alla medaglia di Fields Tim Gowers, ha controllato le soluzioni e ha contribuito a selezionare i problemi originali per quest'anno.

DeepMind e altre aziende sono in corsa per fornire alla fine prove di macchine, l'essenziale Risolvi le domande di ricerca in matematica . I problemi con l'IMO, la competizione leader al mondo per i giovani matematici, sono diventati un metro per i progressi nella direzione di questo obiettivo e sono visti come una "grande sfida" per l'apprendimento automatico, secondo la compagnia.

"Questa è la prima volta che un sistema di intelligenza artificiale è stato in grado di raggiungere servizi a livello di medaglia", ha affermato Pushmeet Kohli, vicepresidente di AI in Science at DeepMind, in una consultazione della stampa. "Questa è una pietra miliare importante sulla strada per costruire prove progressive", ha detto Kohli.

estensione

Solo pochi mesi fa, a gennaio, il sistema DeepMind Servizi di alfageometria a livello di medaglie Quando si risolvono un tipo di problemi IMO, in particolare quelli nella geometria euclidea. La prima intelligenza artificiale che funziona a livello di medaglia d'oro per le domande complessive, incluso il test in algebra, combinatoria e teoria dei numeri, che sono generalmente considerate più impegnative della geometria: è il diritto di ottenere un prezzo di $ 5 milioni, il premio Olympiade di AI Math (AIMO). (Il prezzo ha criteri rigorosi come la divulgazione del codice sorgente e il lavoro con una potenza di calcolo limitata, il che significa che gli attuali sforzi di DeepMind non si qualificherebbero.)

Nel loro ultimo tentativo, i ricercatori hanno utilizzato Alphageometry2 per risolvere il problema della geometria in meno di 20 secondi; L'intelligenza artificiale è una versione migliorata e più veloce del tuo sistema di dischi, afferma lo specialista del computer DeepMind Thang Luong.

Per gli altri tipi di domande, il team ha sviluppato un sistema completamente nuovo chiamato Alphaproof. Alphaproof ha risolto due problemi di algebra nella competizione e uno in teoria dei numeri, per i quali ci sono voluti tre giorni. (I partecipanti all'IMO effettivo hanno due sessioni di 4,5 ore ciascuna.) Non è stato in grado di risolvere i due problemi nella combinazione, un'altra area della matematica.


Close-up di una medaglia d'oro, vinto nella 63a olimpiade di matematica internazionale da un partecipante rumeno.

I ricercatori hanno ottenuto risultati contrastanti quando rispondono alle domande matematiche con i modelli vocali, il tipo di sistema che guida i chatbot come Chatt. A volte i modelli danno la risposta corretta, ma non possono spiegare razionalmente il loro ragionamento, e talvolta

Solo la scorsa settimana, un team di società di software Numina e Huggingface hanno utilizzato un modello vocale per vincere un "prezzo di avanzamento" di Amio intermedio basato su versioni semplificate dei problemi IMO. Le aziende hanno reso il loro intero sistema open source e lo hanno reso disponibile per il download di altri ricercatori. Ma i vincitori hanno detto natura che i modelli linguistici da soli probabilmente non sarebbero sufficienti per risolvere problemi difficili.

solo classe

Alphaproof combina un modello vocale con la tecnologia di rafforzamento dell'apprendimento, che il motore "Alphazero" per i giochi di attacco come Go e alcuni Problemi matematici specifici . Con l'aumento dell'apprendimento, una rete neurale impara attraverso esperimenti ed errori. Funziona bene se le sue risposte possono essere valutate utilizzando una scala oggettiva. A tale scopo, Alphaproof è stato addestrato a leggere e scrivere prove in un linguaggio formale chiamato Lean, che viene utilizzato nel pacchetto software "Assistente alle prove" con lo stesso nome che è popolare tra i matematici. Per questo, Alphaproof ha testato se le sue spese fossero corrette facendole nel pacchetto snello, il che ha contribuito a compilare alcuni dei passaggi del codice.

La formazione di un modello vocale richiede enormi quantità di dati, ma solo poche prove matematiche erano disponibili in snello. Al fine di superare questo problema, il team ha sviluppato una rete aggiuntiva che ha cercato di tradurre una registrazione esistente di un milione di problemi che sono stati scritti in linguaggio naturale, ma senza tradurre soluzioni scritte in snello, afferma Thomas Hubert, un ricercatore di studenti di DeepMind Machine che ha condotto lo sviluppo dell'alfaproof con. "Possiamo imparare a dimostrare il nostro approccio, anche se in origine non abbiamo addestrato prove scritte sull'uomo?" (La compagnia era simile a quella di Go, in cui la sua AI ha imparato a giocare giocando contro se stessa, invece del modo in cui fanno le persone.)

Tasto magico

Molte delle traduzioni magre non avevano senso, ma abbastanza erano abbastanza buone da portare Alphoof al punto in cui poteva iniziare i suoi crescenti cicli di apprendimento. I risultati sono stati molto migliori del previsto, hanno affermato Gowers nella consultazione della stampa. "Molti problemi con l'IMO hanno questa proprietà della chiave magica. Il problema sembra prima difficile fino a trovare una chiave magica che la apre", ha detto Gowers, che lavora al Collège de France di Parigi.

In alcuni casi, Alphaproof sembrava essere in grado di fare questo ulteriore passo di creatività dandogli un passo corretto da una soluzione infinitamente grande possibile. Ma sono necessarie ulteriori analisi per determinare se le risposte fossero meno sorprendenti di quanto sembravano, aggiunti Gowers. Un discorso simile sorse dopo il sorprendente 'Zug 37' "https://www.nature.com/articles/529445a" data-track = "clicca" data-label = "https://www.nature.com/artics/52945a" Data Track Category = "Body Testo Link"> Victory famosa nel 2016 sul miglior giocatore di Go Human Go del mondo -Una svolta per il KI.

Resta da vedere se le tecniche possono essere perfezionate per lavorare a un livello di ricerca in matematica, ha affermato Myers alla revisione della stampa. "Può espandersi ad altri tipi di matematica in cui non possono essere formati milioni di problemi?"

"Abbiamo raggiunto il punto in cui non solo puoi dimostrare problemi di ricerca aperti, ma anche problemi che sono molto impegnativi per i migliori giovani matematici del mondo", ha detto lo specialista del computer DeepMind David Silver, che è stato il principale ricercatore nello sviluppo di Alphago a metà 2010.