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, aveva prodotto nuovi risultati su dieci diversi problemi aperti di matematica. (No, non sono i problemi del Millenium Prize, ma sono comunque significativi.)

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

È molto da assimilare tutto in una volta. In questo articolo ho organizzato i problemi per campo e descritto a grandi linee cosa è successo, cosa questo potrebbe implicare per la matematica come disciplina e cosa possiamo intuire su Astra.

Quali sono i dieci problemi?

Ecco ciascun risultato, in termini semplici, insieme al campo specifico di matematica o informatica a cui appartiene.

Gruppi non sofic

Campo: Teoria dei gruppi

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

Wikipedia è già stata aggiornata:

Impacchettamento di sfere

Campo: Geometria in alta dimensione

La domanda è quanto densamente si possano impacchettare insieme 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 di questo specifico vincolo dal 1978. Non fornisce un metodo di impacchettamento migliore — restringe quanto possa essere buono qualsiasi metodo futuro.

Codici binari e sferici

Campo: Teoria dei codici

I codici correttori di errore funzionano mantenendo i messaggi validi sufficientemente distanti tra loro affinché piccoli errori non possano trasformarne uno in un altro. Astra ha dimostrato limiti molto più stretti (migliorati esponenzialmente) su quanti di questi messaggi possono esistere per una data distanza minima, con un risultato corrispondente per punti distribuiti su una sfera ad alta dimensione.

Congettura di rigidità di Connes

Campo: Algebre di operatori

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

Complessità dei circuiti aritmetici

Campo: Teoria della complessità computazionale

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

Ripetizione parallela quantistica

Campo: Teoria della complessità quantistica

La teoria classica dice che far ripetere molte volte in parallelo un gioco difficile a due giocatori che non comunicano rende esponenzialmente meno probabile che i trucchi abbiano successo. Astra ha dimostrato che la stessa garanzia vale anche quando i giocatori condividono entanglement quantistico, estendendo un principio classico fondamentale all’ambito quantistico.

Problema del vettore più vicino

Campo: Crittografia basata su reticoli

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

Congettura del volume di Ehrhart

Campo: Geometria discreta e convessa

Per una forma convessa il cui unico punto di griglia interno si trova esattamente al suo baricentro, i matematici volevano conoscere il volume massimo che una tale forma può avere in una data dimensione. Astra ha calcolato quel volume massimo per ogni dimensione, risolvendo la congettura in piena generalità.

Numeri di Ramsey multicolore

Campo: 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 con l’aumentare del numero di categorie, risolvendo il problema 183 di Erdős.

Congetture sui numeri estremali

Campo: Teoria estremale dei grafi

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

Ciascuno 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 versante della teoria dell’informatica.

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 sa qualcosa di matematica.

La cosa più comune che si dice, come critica: diversi 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, da solo, 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 bocciatura in blocco di tutto questo insieme di problemi. Primo, il risultato sui gruppi non sofic non è un piccolo aggiustamento di un quasi-centro esistente — è la prima costruzione del suo genere dopo 27 anni in cui nessuno ne aveva una, e si prevede che la tecnica alla base si generalizzi per trovarne altri.

Secondo, diversi degli altri nove risultati, compresi il vincolo sull’impacchettamento di sfere e la durezza del CVP, non sono affatto controesempi; sono miglioramenti diretti di limiti noti. 

Cosa resta irrisolto

Vale la pena tenere d’occhio alcune cose mentre il settore analizzerà il tutto nei prossimi giorni, settimane e mesi:

\n
• Nessuna peer review per ora. Questi risultati sono verificati con Lean e revisionati informalmente da matematici che hanno visto i preprint, ma nessuno è passato attraverso un processo di rivista con referaggio. 
\n
• L’autorship è ancora in negoziazione. 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.
\n

Cosa significa per la matematica

Il cambiamento più immediato riguarda ciò su cui i matematici potrebbero effettivamente passare il loro tempo. Se un problema aperto ben posto può essere affidato a un modello e controllato in Lean, il collo di bottiglia si sposta da \"qualcuno può risolverlo\" a \"abbiamo posto la domanda giusta e l’abbiamo formalizzata correttamente\". L’abilità di porre un buon problema e sapere quale valga la pena attaccare è una vera competenza che i matematici sviluppano con l’esperienza. 

C’è anche una questione latente di finanziamenti e credibilità. Borse di ricerca, pratiche di tenure e premi sono storicamente costruiti intorno alla scarsità: questi problemi erano abbastanza difficili che risolverne uno diceva qualcosa su chi lo risolveva. Se i risultati assistiti dall’IA diventano di routine, il settore avrà bisogno di nuovi modi per segnalare ciò che è davvero difficile rispetto a ciò che ora è alla portata di qualche migliaio di dollari di inferenza. Certo, la persona media non comprende pienamente questi problemi. Chi ha una formazione reale 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 cosa costituiscano una prova.

Alcuni leggono proprio il ritmo come la vera notizia: dieci problemi vecchi di decenni che arrivano in blocco, in campi non correlati, più velocemente di quanto gli esperti riescano persino a recensirli. Una domanda per il futuro: \"Riusciremo a stare al passo con tutte queste verifiche?\"

Altri ribattono che questo dica meno sull’IA in generale di quanto sembri. La matematica è un ambito raro in cui il lavoro di un modello può essere controllato in modo automatico e completo. La maggior parte dei problemi del mondo reale non offre quel tipo di chiave di risposta integrata e automatica. In questa prospettiva, 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 auditato o assimilato completamente 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 autentico: una vera, annosa questione aperta nella teoria dei gruppi, chiusa da una costruzione esplicita che i matematici del settore stanno prendendo sul serio. Gli altri nove risultati, nel complesso, rappresentano un insieme ampio e tecnicamente sostanziale 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 stata la portata. Ti terremo aggiornato.