Un modello OpenAI ha confutato una congettura centrale della geometria discreta

Per quasi 80 anni, i matematici hanno studiato una domanda ingannevolmente semplice: se si collocano $n$ punti nel piano, quante coppie di punti possono trovarsi esattamente a distanza $1$?

Questo è il problema delle distanze unitarie nel piano, formulato per la prima volta da Paul Erdős nel 1946. È una delle questioni più note della geometria combinatoria, facile da enunciare e straordinariamente difficile da risolvere. Il libro del 2005 Research Problems in Discrete Geometry, di Brass, Moser e Pach, lo definisce "forse il problema più noto (e il più semplice da spiegare) della geometria combinatoria". Noga Alon, uno dei massimi esperti di combinatoria a Princeton, lo descrive come "uno dei problemi preferiti di Erdős". Erdős offrì persino un premio in denaro per la risoluzione di questo problema.

Oggi presentiamo una svolta nel problema delle distanze unitarie. Dal lavoro originale di Erdős, la convinzione prevalente è stata che le costruzioni a "griglia quadrata" mostrate più sotto fossero sostanzialmente ottimali per massimizzare il numero di coppie a distanza unitaria. Un modello interno di OpenAI ha confutato questa congettura di lunga data, fornendo una famiglia infinita di esempi che produce un miglioramento polinomiale. La dimostrazione è stata verificata da un gruppo di matematici esterni. Hanno anche scritto un articolo di accompagnamento che spiega l'argomentazione e fornisce ulteriori informazioni di contesto e sul significato del risultato.

Il risultato è notevole anche per il modo in cui è stato ottenuto. La dimostrazione è stata prodotta da un nuovo modello di ragionamento generalista, anziché da un sistema addestrato specificamente per la matematica, progettato per esplorare strategie dimostrative o mirato in particolare al problema delle distanze unitarie. Nell'ambito di uno sforzo più ampio per verificare se i modelli avanzati possano contribuire alla ricerca di frontiera, lo abbiamo valutato su una raccolta di problemi di Erdős. In questo caso, ha prodotto una dimostrazione che risolve il problema aperto.

Questa dimostrazione rappresenta una tappa importante per le comunità della matematica e dell'IA. Segna la prima volta in cui un importante problema aperto, centrale per un sottoambito della matematica, è stato risolto autonomamente dall'IA. Dimostra anche la profondità di ragionamento che questi sistemi oggi supportano. La matematica offre un banco di prova particolarmente chiaro per il ragionamento: i problemi sono precisi, le possibili dimostrazioni possono essere verificate e un'argomentazione lunga funziona solo se il ragionamento regge dall'inizio alla fine. È notevole anche il metodo con cui il problema è stato risolto. La dimostrazione applica a una questione geometrica elementare idee inattese e sofisticate della teoria algebrica dei numeri.

Tim Gowers, vincitore della Medaglia Fields, definisce il risultato "una tappa fondamentale nella matematica dell'IA" nell'articolo di accompagnamento. Secondo il noto teorico dei numeri Arul Shankar, "A mio parere questo articolo dimostra che gli attuali modelli di IA vanno oltre il semplice ruolo di assistenti dei matematici: sono capaci di avere idee originali e ingegnose, e poi di portarle a compimento".

La dimostrazione è disponibile qui⁠(si apre in una nuova finestra). L'articolo di accompagnamento di importanti matematici esterni è disponibile qui⁠(si apre in una nuova finestra). Puoi trovare una versione abbreviata della chain of thought del modello qui⁠(si apre in una nuova finestra).

Sia $u(n)$ il massimo numero possibile di coppie a distanza unitaria tra $n$ punti nel piano. È facile costruire esempi che raggiungono un tasso di crescita lineare: collocare $n$ punti su una linea dà $n-1$ coppie, mentre una griglia quadrata ne dà circa $2n$. La costruzione precedentemente migliore conosciuta, derivata da una griglia quadrata riscalata, risulta dare ancora di più: $n^{1 + C / \log \log(n)}$ per una costante $C$. Poiché $\log \log(n)$ tende all'infinito con $n$, il termine aggiuntivo nell'esponente tende a $0$, il che significa che queste costruzioni ottengono una crescita solo leggermente più rapida di quella lineare. Per decenni si è ampiamente creduto che questo tasso fosse sostanzialmente il migliore possibile e che nessuna costruzione potesse migliorare in modo significativo la griglia quadrata. In termini tecnici, Erdős congetturò un limite superiore di $n^{1+o(1)}$, in cui il termine aggiuntivo $o(1)$ indica un termine che tende a $0$ con $n$.

Il nostro nuovo risultato confuta questa congettura. Più precisamente, per infiniti valori di $n$, la dimostrazione costruisce configurazioni di $n$ punti con almeno $n^{1+\delta}$ coppie a distanza unitaria, per un certo esponente fisso $\delta > 0$. (La dimostrazione originale dell'IA non fornisce un $\delta$ esplicito, ma un imminente affinamento dovuto al professore di matematica di Princeton Will Sawin ha mostrato che si può prendere $\delta=0.014$.)

La storia del problema aiuta a comprendere perché il risultato sia sorprendente. Il miglior limite inferiore noto era rimasto sostanzialmente invariato dalla costruzione originale di Erdős del 1946. Il miglior limite superiore, $O(n^{4/3})$, risale al lavoro di Spencer, Szemerédi e Trotter del 1984 e, nonostante successivi affinamenti e lavori strutturali correlati di Székely, Katz e Silier, Pach, Raz e Solymosi e di altri, il limite superiore è rimasto sostanzialmente invariato. Come prova a favore della congettura, Matoušek e Alon-Bucić-Sauermann hanno studiato il problema con distanze non euclidee nel piano e hanno dimostrato che "la maggior parte" di queste distanze non euclidee obbedisce in un certo senso alla congettura.

Sorprendentemente, gli ingredienti chiave della costruzione provengono da una parte molto diversa della matematica nota come teoria algebrica dei numeri, che studia concetti come la fattorizzazione nelle estensioni degli interi note come campi di numeri algebrici.

A un livello generale, la dimostrazione parte da un'idea geometrica familiare e la spinge in una direzione inattesa.

Il limite inferiore originale di Erdős può essere compreso attraverso gli interi gaussiani: numeri della forma $a+bi$, dove $a$ e $b$ sono interi e $i$ è la radice quadrata di $-1$. Gli interi gaussiani estendono gli interi ordinari e, come questi, godono di proprietà come la fattorizzazione unica in numeri primi. Tali estensioni degli interi ordinari o dei razionali sono note come campi di numeri algebrici. La nuova argomentazione sostituisce gli interi gaussiani con generalizzazioni più complicate della teoria algebrica dei numeri, dotate di simmetrie più ricche che possono creare molte più differenze di lunghezza unitaria.

L'argomentazione precisa usa strumenti come torri infinite di campi di classe e la teoria di Golod–Shafarevich per mostrare che i campi numerici richiesti dall'argomentazione esistono davvero. Queste idee erano ben note ai teorici algebrici dei numeri, ma è stata una grande sorpresa che tali concetti abbiano implicazioni per questioni geometriche nel piano euclideo.

Questo risultato segna un momento importante nell'interazione tra IA e matematica: un sistema di IA ha risolto autonomamente un problema aperto di lunga data al centro di un campo attivo. Offre anche un primo scorcio di un nuovo tipo di collaborazione tra IA e matematici umani. In questo caso, il lavoro di accompagnamento dei matematici esterni offre un quadro sostanzialmente più ricco rispetto alla sola soluzione originale.

Come scrive Thomas Bloom nella nota di accompagnamento:

"Quando valuto l'importanza e l'influenza di una dimostrazione generata dall'IA, una domanda che mi pongo è: ci ha insegnato qualcosa di nuovo sul problema? Comprendiamo meglio la geometria discreta adesso? Penso che la risposta sia un sì moderato: questo mostra che le costruzioni di teoria dei numeri hanno molto più da dire su questo tipo di questioni di quanto sospettassimo; inoltre, che la teoria dei numeri richiesta può essere molto profonda. Senza dubbio molti teorici algebrici dei numeri esamineranno da vicino altri problemi aperti della geometria discreta nei prossimi mesi."

L'inaspettato legame tra teoria algebrica dei numeri e geometria discreta rivelato da questa soluzione è uno degli elementi che rendono il risultato così notevole. Non si limita semplicemente a risolvere una specifica congettura, ma può offrire ai matematici un ponte per iniziare a esplorare ulteriori problemi correlati.

Bloom indica anche una possibilità più ampia:

"Le frontiere della conoscenza sono molto frastagliate e senza dubbio i prossimi mesi e anni vedranno successi simili in molte altre aree della matematica, dove problemi aperti di lunga data saranno risolti da un'IA che rivela connessioni inattese e spinge al limite l'apparato tecnico esistente. L'IA ci sta aiutando a esplorare più pienamente la cattedrale della matematica che abbiamo costruito nel corso dei secoli; quali altre meraviglie ancora invisibili ci aspettano dietro le quinte?"

Questo risultato offre un esempio promettente: l'IA contribuisce non solo con una soluzione, ma con una scoperta matematica il cui significato diventa più chiaro e più ricco grazie alla successiva comprensione umana.

La lezione va oltre questo particolare risultato. Un migliore ragionamento matematico può rendere l'IA un partner di ricerca più forte: qualcosa che può tenere insieme linee di pensiero difficili, collegare idee tra aree lontane della conoscenza, far emergere percorsi promettenti che gli esperti potrebbero non aver considerato prioritari e aiutare i ricercatori a fare progressi su problemi che altrimenti sarebbero troppo complessi o richiederebbero troppo tempo per essere affrontati.

Queste capacità contano anche oltre la matematica. Se un modello può mantenere coerente un'argomentazione complessa, collegare idee tra aree lontane della conoscenza e produrre lavoro che resiste all'esame degli esperti, allora queste sono capacità utili anche in biologia, fisica, scienza dei materiali, ingegneria e medicina, e fanno parte del nostro percorso di più lungo termine verso una ricerca più automatizzata: sistemi che possano aiutare scienziati e ingegneri a esplorare più idee e affrontare questioni tecniche più difficili.

L'IA sta per assumere un ruolo molto serio nelle parti creative della ricerca, e soprattutto della stessa ricerca sull'IA. Sebbene questo progresso non sia inatteso, rafforza l'urgenza che sentiamo nel comprendere questa prossima fase dello sviluppo dell'IA, le sfide dell'allineamento di sistemi molto intelligenti e il futuro della collaborazione tra esseri umani e IA.

Quel futuro dipende ancora dal giudizio umano. La competenza diventa più preziosa, non meno. L'IA può aiutare a cercare, suggerire e verificare. Le persone scelgono i problemi che contano, interpretano i risultati e decidono quali domande perseguire in seguito.