notizia

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

Nuovo rapporto sulla saggezza

Redattore: Dipartimento editoriale

[Introduzione alla Nuova Saggezza] Proprio ora, l’ultimo modello matematico di Google DeepMind ha vinto la medaglia d’argento alle Olimpiadi della matematica dell’IMO! Non solo ha risolto 4 delle 6 domande con punteggi perfetti, a solo 1 punto dalla medaglia d'oro, ma ha impiegato solo 19 secondi per risolvere la quarta domanda. La qualità e la velocità della risoluzione del problema hanno sbalordito i giudici umani che hanno assegnato il punteggio .

L'intelligenza artificiale ha vinto la medaglia d'argento alle Olimpiadi della matematica dell'IMO!

Proprio ora, Google DeepMind ha annunciato che le vere domande delle Olimpiadi internazionali della matematica di quest’anno sono state prodotte dal suo stesso sistema di intelligenza artificiale.

Tra questi, l'IA non solo ha completato con successo 4 delle 6 domande, ma ha anche ricevuto il massimo dei voti per ciascuna domanda, che equivale al punteggio più alto di una medaglia d'argento: 28 punti.

Questo risultato è a solo 1 punto dalla medaglia d'oro!

Tra 609 concorrenti, solo 58 hanno vinto medaglie d'oro

Nella competizione ufficiale, i concorrenti umani invieranno le loro risposte in due sessioni, con un limite di tempo di 4,5 ore ogni volta.

È interessante notare che l'IA ha impiegato solo pochi minuti per rispondere a una delle domande, ma le domande rimanenti hanno richiesto tre giorni interi, il che si può dire che sia un timeout serio.

Ciò che ha dato un grande contributo questa volta sono stati due sistemi di intelligenza artificiale: AlphaProof e AlphaGeometry 2.

Punto importante: l'IMO 2024 non è presente nei dati di addestramento di queste due IA.

Scott Wu, uno dei fondatori dell’ingegnere AI Devin (tre volte medaglia d’oro IOI) si è lamentato: “Quando ero bambino, le Olimpiadi erano tutto ciò che avevo, non avrei mai pensato che solo 10 anni dopo sarebbero state sostituite dall’intelligenza artificiale risolto".

Nel concorso IMO di quest'anno sono previste sei domande che coinvolgono algebra, calcolo combinatorio, geometria e teoria dei numeri. Sei percorsi fanno quattro, sentiamo il livello dell'intelligenza artificiale——

L’abilità di ragionamento matematico dell’intelligenza artificiale sconvolge il professore

Sappiamo tutti che l’intelligenza artificiale precedente era limitata nella risoluzione di problemi matematici a causa delle limitazioni nelle capacità di ragionamento e nei dati di addestramento.

I due giocatori IA apparsi insieme oggi hanno superato questa limitazione. sono, rispettivamente...

- AlphaProof, un nuovo sistema per il ragionamento matematico formale basato sull'apprendimento per rinforzo

- AlphaGeometry 2, il sistema di risoluzione dei problemi geometrici di seconda generazione

Le risposte fornite dalle due IA sono state valutate secondo le regole dai famosi matematici, il professor Timothy Gowers (medaglia d'oro IMO e medaglia Fields) e il dottor Joseph Myers (due volte medaglia d'oro IMO e presidente del comitato di selezione delle domande IMO 2024). .

Alla fine, AlphaProof ha risolto correttamente due domande di algebra e una di teoria dei numeri. Una delle domande più difficili è stata risolta da soli 5 concorrenti umani nell'IMO di quest'anno. AlphaGeometry 2 ha risolto un problema di geometria.

Ci sono solo due problemi di matematica combinatoria che non sono stati risolti.

Anche il professor Timothy Gowers è rimasto profondamente scioccato durante il processo di valutazione——

Che un programma possa trovare una soluzione così non ovvia è davvero impressionante e va ben oltre ciò che mi aspettavo, dato lo stato attuale della tecnica.

ProvaAlfa

AlphaProof è un sistema in grado di dimostrare proposizioni matematiche nel linguaggio formale Lean.

Combina un modello linguistico di grandi dimensioni pre-addestrato con l'algoritmo di apprendimento per rinforzo AlphaZero, che ha imparato da solo a padroneggiare gli scacchi, lo shogi e il Go.

Un vantaggio chiave dei linguaggi formali è che possono essere formalmente verificati per dimostrazioni che coinvolgono il ragionamento matematico. Tuttavia, la loro applicazione nell’apprendimento automatico è stata limitata a causa della quantità molto limitata di dati rilevanti scritti dagli esseri umani.

Al contrario, gli approcci basati sul linguaggio naturale, pur avendo accesso a grandi quantità di dati, possono produrre passaggi e soluzioni di ragionamento intermedi plausibili, ma errati.

Per superare questo problema, i ricercatori di Google DeepMind hanno messo a punto il modello Gemini per tradurre automaticamente le dichiarazioni dei problemi del linguaggio naturale in dichiarazioni formali, costruendo un’ampia libreria contenente problemi formali di varia difficoltà, costruendo così un ponte tra i due campi complementari.

Quando si risolve un problema, AlphaProof genera soluzioni candidate e le dimostra o le confuta cercando possibili passaggi di prova in Lean.

Ogni prova trovata e verificata viene utilizzata per rafforzare il modello linguistico di AlphaProof in modo che possa risolvere problemi più difficili in futuro.

Per addestrare AlphaProof, i ricercatori hanno dimostrato o confutato milioni di domande che coprivano un'ampia gamma di difficoltà e aree tematiche matematiche nelle settimane precedenti e durante la competizione.

Durante la competizione, hanno anche applicato un ciclo di formazione rafforzando le dimostrazioni sulle variazioni autogenerate del problema della competizione fino a quando non è stata trovata una soluzione completa.

Infografica del flusso del ciclo di formazione dell'apprendimento per rinforzo AlphaProof: circa un milione di problemi matematici informali vengono tradotti dalla rete formale in un linguaggio matematico formale; la rete di solutori si allena poi gradualmente utilizzando l'algoritmo AlphaZero cercando prove o confutazioni di questi problemi , per risolvere problemi più impegnativi

Geometria alfa 2

AlphaGeometry 2, la versione aggiornata di AlphaGeometry, è un sistema ibrido neurale-simbolico addestrato da zero basato sul modello linguistico di Gemini.

Basato su un numero di dati sintetici di un ordine di grandezza maggiore rispetto alla generazione precedente, può risolvere problemi geometrici più difficili, comprese equazioni che coinvolgono il movimento degli oggetti, angoli, proporzioni, distanze, ecc.

Inoltre, presenta un motore simbolico che è due ordini di grandezza più veloce del suo predecessore. Quando si incontrano nuovi problemi, utilizza un nuovo meccanismo di condivisione delle conoscenze che consente combinazioni avanzate di diversi alberi di ricerca per risolvere problemi più complessi.

Prima di partecipare all'IMO di quest'anno, AlphaGeometry 2 aveva già ottenuto molto successo: poteva risolvere l'83% dei problemi di geometria dell'IMO negli ultimi 25 anni, mentre la prima generazione poteva risolverne solo il 53%.

In questa IMO, la velocità di AlphaGeometry 2 ha scioccato tutti: entro 19 secondi dalla ricezione della domanda formale, ha risolto la domanda 4!

La domanda 4 richiede la prova che la somma di ∠KIL e ∠XPY è uguale a 180°. AlphaGeometry 2 consiglia di costruire un punto E sulla linea BI in modo tale che ∠AEB=90°.Il punto E aiuta a determinare il punto medio L di AB, formando molte coppie simili di triangoli, come ABE ~ YBI e ALE ~ IPC, dimostrando così la conclusione

Processo di risoluzione dei problemi dell'intelligenza artificiale

Vale la pena ricordare che queste domande verranno prima tradotte manualmente in linguaggio matematico formale prima di essere sottoposte all’intelligenza artificiale.
La prima

In generale, la prima domanda (P1) in ogni test IMO è relativamente semplice.

I Netizens hanno detto: "P1 richiede solo conoscenze di matematica delle scuole superiori e i giocatori umani di solito lo completano entro 60 minuti".

La prima domanda dell’IMO 2024 esamina principalmente le proprietà del numero reale α e richiede di trovare un numero reale α che soddisfi determinate condizioni.

L'intelligenza artificiale ha dato la risposta corretta: α è un numero intero pari. Quindi, come si risponde esattamente?

Nella prima fase della risoluzione del problema, l'intelligenza artificiale ha innanzitutto fornito un teorema secondo cui gli insiemi sinistro e destro sono uguali.

L'insieme a sinistra rappresenta che tutti i numeri reali α che soddisfano le condizioni, per qualsiasi intero positivo n, n possono dividere ⌊i*α⌋ da 1 a n; l'insieme a destra rappresenta che esiste un intero k, k è un numero pari e il numero reale α è uguale a k.

La dimostrazione seguente si divide in due direzioni.

Per prima cosa prova che l'insieme a destra è un sottoinsieme (direzione semplice) dell'insieme a sinistra.

Quindi, prova che l'insieme a sinistra è un sottoinsieme dell'insieme a destra (direzione difficile).

Fino alla fine del codice, l'intelligenza artificiale ha prodotto un'equazione chiave ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋), utilizzando l'equazione per dimostrare che α deve essere un numero pari.

Infine, DeepMind ha riassunto i tre assiomi su cui si basa l’intelligenza artificiale nel processo di risoluzione dei problemi: propext, Classical.choice e Quot.sound.

Quello che segue è il processo completo di risoluzione dei problemi di P1: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

P2

La seconda domanda esamina la relazione tra la coppia di interi positivi (a, b), che coinvolge la proprietà del massimo comun divisore.

La risposta risolta dall’intelligenza artificiale è:

Il teorema è che per una coppia di interi positivi (a, b) che soddisfa determinate condizioni, il suo insieme può contenere solo (1,1).

Nel successivo processo di risoluzione del problema, la strategia di dimostrazione adottata dall'IA consiste nel dimostrare prima che (1,1) soddisfa le condizioni date, e poi dimostrare che questa è l'unica soluzione.

Dimostrare che (1,1) è la soluzione finale, utilizzando g=2, N=3.

Mostra che se (a,b) è la soluzione, allora ab+1 deve dividere g.

In questo processo, l'intelligenza artificiale ha utilizzato il teorema di Eulero e le proprietà delle operazioni modulari per il ragionamento.

Infine, prova che a=b=1 è l’unica soluzione possibile.

Quello che segue è il processo completo di risoluzione dei problemi di P2: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

Numero 4

P4 è una domanda di prova geometrica che richiede la dimostrazione di una specifica relazione angolare geometrica.

Come accennato in precedenza, AlphaGeometry 2 lo ha completato in 19 secondi, stabilendo un nuovo record.

A seconda della soluzione data, come con la prima generazione di AlphaGeometry, i punti ausiliari in tutte le soluzioni vengono generati automaticamente dal modello linguistico.

Nella dimostrazione, tutto il tracciamento degli angoli utilizza l'eliminazione gaussiana e d(AB)−d(CD) è uguale all'angolo direzionale da AB a CD (modulo π).

Durante il processo di risoluzione del problema, l'intelligenza artificiale contrassegnerà manualmente le coppie di triangoli simili e triangoli congruenti (contrassegnati in rosso).

Successivamente, ci sono i passaggi per risolvere il problema di AlphaGeometry, che viene completato utilizzando il "metodo di ricontraddizione".

Innanzitutto utilizzare Lean per formalizzare le proposizioni che devono essere dimostrate e visualizzare la costruzione geometrica.

I passaggi chiave della dimostrazione sono i seguenti.

Guarda l'immagine qui sotto per il processo completo di risoluzione dei problemi: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

Numero 6

La sesta domanda dell'IMO è il "boss finale", che esplora le proprietà delle funzioni e richiede di dimostrare conclusioni specifiche sui numeri razionali.

L'AI risolve, c=2.

Diamo prima un'occhiata all'enunciato del teorema, che definisce le proprietà della "funzione aquaesuliana" e dichiara che per tutte queste funzioni, l'insieme di valori di f(r)+f(-r) ha al massimo 2 elementi.

La strategia di dimostrazione consiste nel dimostrare innanzitutto che per qualsiasi funzione acquaesuliana, l'insieme di valori di f(r)+f(-r) ha al massimo 2 elementi. Quindi costruisci una specifica funzione acquaesuliana in modo che f(r)+f(-r) abbia esattamente 2 valori diversi.

Dimostrare che quando f(0)=0, f(x)+f(-x) assume al massimo due valori diversi, e dimostrare che non esiste una funzione acquaesuliana f(0)≠0.

Costruisci la funzione f(x)=-x+2⌈x⌉ e dimostra che è una funzione acquaesuliana.

Infine, prova che per questa funzione f(-1)+f(1) =0 e f(1/2)+f(-1/2)=2 sono due valori diversi.

Quello che segue è il processo completo di risoluzione dei problemi: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Puoi fare domande di matematica sulle Olimpiadi, ma puoi dire quale è più grande, 9.11 o 9.9?

Andrew Gao, ricercatore presso la Stanford University e la Sequoia, ha affermato l'importanza di questa svolta nell'intelligenza artificiale:

La cosa fondamentale è che le ultime domande del test IMO non sono incluse nel set di formazione. Questo è importante perché dimostra che l’intelligenza artificiale può gestire problemi nuovi e invisibili.

Inoltre, i problemi geometrici risolti con successo dall’intelligenza artificiale sono sempre stati considerati estremamente impegnativi a causa della natura dello spazio coinvolto (che richiede pensiero intuitivo e immaginazione spaziale).

Jim Fan, uno scienziato senior di Nvidia, ha pubblicato un lungo articolo in cui afferma che i modelli di grandi dimensioni sono esistenze misteriose...

Possono vincere medaglie d'argento alle Olimpiadi della matematica e spesso commettono errori su domande come "Quale numero è più grande, 9,11 o 9,9?"

Non solo Gemini, ma anche GPT-4o, Claude-3.5 e Llama-3 non possono rispondere correttamente al 100%.

Addestrando i modelli di intelligenza artificiale, stiamo esplorando vaste aree oltre la nostra intelligenza.Nel processo, abbiamo scoperto un'area molto strana: un pianeta extrasolare che assomiglia alla Terra ma è pieno di strane valli

Ciò sembra irragionevole, ma possiamo spiegarlo utilizzando la distribuzione dei dati di addestramento:

AlphaProof e AlphaGeometry 2 sono addestrati su dimostrazioni formali e motori simbolici specifici del dominio. In una certa misura, sono più bravi a risolvere i problemi specializzati delle Olimpiadi, anche se sono costruiti su un LLM generico. Il set di addestramento di GPT-4o è combinato con una grande quantità di dati di codice GitHub, che potrebbero superare di gran lunga i dati matematici. Tra le versioni software, "v9.11 > v9.9" può distorcere seriamente la distribuzione dei dati. Pertanto, questo errore è comprensibile in una certa misura.

Il capo degli sviluppatori di Google ha affermato che i modelli in grado di risolvere difficili problemi matematici e fisici sono il percorso chiave verso l'AGI, e oggi abbiamo fatto un altro passo in questo percorso.

Altri netizen hanno detto che ci sono state troppe informazioni questa settimana.

Riferimenti:

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

https://x.com/DrJimFan/status/1816521330298356181