Il prossimo modello di OpenAI, Astra, ha appena risolto dieci problemi aperti di matematica vecchi di decenni

Il 1° agosto, OpenAI ha pubblicato un report sostenendo che il suo prossimo modello, chiamato internamente Astra (non ancora disponibile), aveva prodotto nuovi risultati su dieci diversi problemi aperti in matematica. (No, non sono i problemi del Millennium Prize, ma sono comunque significativi.)

Da notare: Queste soluzioni non sono semplici progressi incrementali sui problemi: sono risoluzioni vere e proprie, verificate con Lean. (Lean è un linguaggio di programmazione e un assistente alla dimostrazione che impone di esplicitare ogni passo di un argomento matematico in dettaglio leggibile dalla macchina.) 

È molto da assimilare tutto insieme. In questo articolo ho organizzato i problemi per area e descrivo a grandi linee cosa è successo, cosa questo potrebbe implicare per la matematica come disciplina e cosa possiamo dedurre su Astra.

Quali sono i dieci problemi?

Ecco ciascun risultato, in termini semplici, insieme all'area specifica di matematica o informatica a cui appartiene.

Gruppi non sofic

Area: Teoria dei gruppi

Astra ha prodotto una costruzione esplicita di un gruppo che non può essere approssimato, per quanto da vicino, da grandi strutture finite — chiudendo una questione aperta da quando il concetto di gruppo "sofico" è stato introdotto nel 1999. La costruzione è corredata da una dimostrazione che nessuna sequenza di approssimazioni finite potrà mai funzionare, formalizzata in Lean in modo che la logica possa essere verificata meccanicamente.

Wikipedia è già stata aggiornata:

Impacchettamento di sfere

Area: Geometria in alta dimensione

La domanda è quanto densamente si possano impacchettare sfere identiche e non sovrapposte man mano che cresce il numero di dimensioni. Astra ha dimostrato un limite superiore più stretto su quella densità in alte dimensioni, il primo miglioramento a questo particolare vincolo dal 1978. Non fornisce un metodo di impacchettamento migliore — restringe quanto potrebbe essere buono qualsiasi futuro metodo.

Codici binari e sferici

Area: Teoria dei codici

I codici correttori d'errore funzionano mantenendo i messaggi validi sufficientemente distanti, così che piccoli errori non possano trasformarne uno in un altro. Astra ha dimostrato limiti molto più stretti (migliorati esponenzialmente) su quanti messaggi del genere possano esistere per una data distanza minima, con un risultato corrispondente per punti distribuiti su una sfera ad alta dimensione.

Congettura di rigidità di Connes

Area: Algebre di operatori

Alain Connes aveva congetturato che certi gruppi potessero sempre essere ricostruiti in modo univoco da una struttura algebrica, chiamata algebra di von Neumann, costruita a partire da essi. Astra ha smentito questo producendo due gruppi genuinamente diversi che danno origine alla stessa algebra, mostrando che la ricostruzione non è sempre biunivoca.

Complessità dei circuiti aritmetici

Area: Teoria della complessità computazionale

Il "permanente", un singolo numero calcolato da una griglia di numeri, è costoso da calcolare, e i teorici della complessità vogliono conoscere il numero minimo di passi aritmetici di cui qualsiasi metodo potrebbe aver bisogno. Astra ha dimostrato un nuovo limite inferiore, più forte, su quel minimo — un tipo di risultato notoriamente difficile anche solo da spostare.

Ripetizione parallela quantistica

Area: Teoria della complessità quantistica

La teoria classica afferma che far ripetere molte volte in parallelo un gioco difficile a due giocatori che non comunicano rende il barare esponenzialmente meno probabile. Astra ha dimostrato che la stessa garanzia vale anche quando i giocatori condividono entanglement quantistico, estendendo un principio classico fondativo all'ambito quantistico.

Problema del vettore più vicino

Area: Crittografia basata su reticoli

Dato un reticolo (una griglia ripetuta di punti) e una posizione bersaglio, questo problema chiede il punto del reticolo più vicino — un problema ritenuto molto difficile in alte dimensioni, motivo per cui è alla base di alcune cifrature resistenti al quantistico. Astra ha dimostrato che anche approssimare la risposta, entro un determinato fattore polinomiale, rimane dimostrabilmente difficile, rafforzando la crittografia costruita sopra di esso.

Congettura sul volume di Ehrhart

Area: Geometria discreta e convessa

Per una forma convessa il cui unico punto del reticolo interno si trova esattamente nel suo baricentro, i matematici volevano conoscere il volume massimo possibile che una tale forma potrebbe avere in una dimensione data. Astra ha determinato quel volume massimo per ogni dimensione, risolvendo la congettura in piena generalità.

Numeri di Ramsey multicolore

Area: Teoria di Ramsey / combinatoria

Con abbastanza persone e abbastanza categorie di relazione tra loro, prima o poi sei garantito di trovare tre persone tutte collegate dalla stessa categoria. Astra ha dimostrato che la dimensione minima del gruppo necessaria cresce più velocemente di qualsiasi tasso esponenziale fisso al crescere del numero di categorie, risolvendo il problema 183 di Erdős.

Congetture sul numero estremo

Area: Teoria estrema dei grafi

Questo ramo della matematica chiede quante connessioni possa avere una rete evitando comunque certi piccoli schemi proibiti. Astra ha risolto due congetture correlate qui, corrispondenti ai problemi 146 e 180 di Erdős, definendo quanto possano diventare dense tali reti prima che quegli schemi diventino inevitabili.

Ognuno di questi problemi era aperto da almeno un decennio; diversi resistevano da trent'anni o più, inclusi problemi su cui hanno lavorato vincitori del Turing Award nel lato di informatica teorica dell'elenco.

Aspetta, un controesempio è il tipo di dimostrazione "facile"?

Chi sono io per dire qualcosa di negativo qui, ma so che è una domanda o reazione comune, soprattutto da parte di chi conosce un po' di matematica.

La cosa più comune che si sente dire, come critica: parecchi di questi risultati sono controesempi piuttosto che nuova teoria generale. Questa idea è importante perché un controesempio risponde a una domanda sì/no ma non ti dice, di per sé, perché lo schema si rompe o non ti consegna una famiglia di oggetti simili da studiare dopo, mentre qualcos'altro, come un teorema di classificazione o una nuova tecnica, apre più porte.

Direi che questa critica regge in generale, ma non vale come liquidazione totale di tutta questa serie di problemi. Primo, il risultato sui gruppi non sofic non è un piccolo ritocco a un quasi-successo esistente — è la prima costruzione del suo genere dopo 27 anni in cui nessuno ne aveva una, e la tecnica alla base si prevede si generalizzi per trovarne altri.

Secondo, parecchi degli altri nove risultati, compreso il vincolo sull'impacchettamento di sfere e il risultato di durezza del CVP, non sono affatto controesempi; sono miglioramenti diretti ai limiti esistenti. 

Cosa resta irrisolto

Ci sono alcune cose da tenere d'occhio mentre il campo analizzerà il tutto nei prossimi giorni, settimane e mesi:

• Nessuna peer review finora. Sono verificate con Lean e revisionate informalmente da matematici che hanno visto i preprint, ma nessuna è passata attraverso un processo di rivista con referaggio. 
• L'attribuzione è ancora in discussione. OpenAI afferma di assumersi la responsabilità dei manoscritti e delle formalizzazioni in Lean, attribuendo invece gli argomenti matematici al modello. La replica indipendente del processo (in contrapposizione alla verifica delle dimostrazioni) è difficile da fare al momento.

Cosa significa per la matematica

Il cambiamento più immediato riguarda ciò su cui i matematici potrebbero effettivamente dedicare il proprio tempo. Se un problema aperto ben posto può essere affidato a un modello e verificato in Lean, il collo di bottiglia si sposta da "qualcuno può risolverlo" a "abbiamo posto la domanda giusta e l'abbiamo formalizzata correttamente". La capacità di porre un buon problema e sapere quale valga la pena affrontare è una competenza reale che i matematici sviluppano con l'esperienza. 

C'è anche una questione di finanziamenti e credibilità che ribolle. I grant di ricerca, le carriere accademiche e i premi sono stati storicamente costruiti attorno alla scarsità: questi problemi erano abbastanza difficili che risolverne uno diceva qualcosa su chi lo risolveva. Se i risultati assistiti dall'IA diventano routine, il campo avrà bisogno di nuovi modi per segnalare cosa è davvero difficile rispetto a ciò che ora è alla portata di qualche migliaio di dollari di inferenza. Ovviamente, la persona media non capisce appieno questi problemi. Le persone con una vera formazione sì, e questo non cambia. Quindi la conoscenza matematica è più preziosa che mai. 

Come stanno reagendo le persone

Le reazioni sui social media si sono divise meno sul fatto che le dimostrazioni tornino, e più su ciò di cui sarebbero la prova.

Alcuni leggono proprio il ritmo come la vera notizia: dieci problemi vecchi di decenni risolti tutti insieme, in campi non correlati, più velocemente di quanto gli esperti possano persino revisionarli. Una domanda per il futuro: "Riusciremo a tenere il passo con tutte queste verifiche?"

Altri ribattono che questo dica meno sull'IA in generale di quanto sembri. La matematica è un dominio raro in cui il lavoro di un modello può essere verificato in modo automatico e completo. La maggior parte dei problemi del mondo reale non offre quel tipo di soluzione automatica incorporata. Da questo punto di vista, il risultato è reale, ma potrebbe dire di più sul fatto che la matematica sia insolitamente adatta all'IA.

Un terzo filone di commenti: una dimostrazione corretta che nessuno ha ancora completamente revisionato o assimilato non è stata davvero compresa, solo verificata. Scoprire un teorema e capirne il significato, in questa visione, sono due lavori diversi.

Considerazioni finali

I matematici dicono che il risultato sui gruppi non sofic sembra quello vero: un autentico problema aperto da decenni nella teoria dei gruppi, chiuso da una costruzione esplicita che i matematici del campo stanno prendendo sul serio. Gli altri nove risultati, nel loro insieme, rappresentano un ampio e tecnicamente sostanziale pacchetto di progressi nella matematica pura.

Quello che non è ancora successo è la parte più lenta: peer review, replica del processo di ricerca e il campo che effettivamente costruisce sopra questi risultati. Quella parte richiede più tempo di un post sul blog, ed è la parte che ci dirà davvero quanto grande sia stato tutto questo. Ti terremo aggiornato.