Ipotesi del tempo esponenziale confutata da un modello di OpenAI?

Il 26 ottobre OpenAI ha pubblicato nel repository openai/math l’articolo “The Exponential Time Hypothesis is False”. Secondo il testo, un modello interno di OpenAI non rivelato ha confutato l’ipotesi del tempo esponenziale (ETH), uno dei presupposti di base della teoria della complessità computazionale. Un gruppo indipendente di informatici, tra cui due coautori dell’ipotesi stessa, sta esaminando l’articolo insieme alla sua formalizzazione in Lean.

Che cos’è l’ipotesi del tempo esponenziale?

L’ETH (Exponential Time Hypothesis) presuppone che il problema 3-SAT, cioè stabilire se una formula logica con clausole di tre variabili sia soddisfacibile, non possa essere deciso più velocemente che in tempo 2^Ω(n) per n variabili. In parole semplici: a ogni variabile in più il tempo cresce in modo esponenziale e nessun algoritmo ingegnoso può cambiarlo.

L’ipotesi è stata formulata da Russell Impagliazzo e Ramamohan Paturi (con Francis Zane). Sull’ETH si basano centinaia di lavori che dimostrano che un certo problema su grafi, basi di dati o biologia computazionale “non può” essere risolto più velocemente (come ricorda The Next Web).

Che cosa ha dimostrato esattamente il modello di OpenAI?

L’articolo presenta un algoritmo deterministico che conta esattamente tutti gli assegnamenti che soddisfano una formula k-CNF per ogni k ≥ 2 fissato. Funziona in spazio polinomiale e in tempo (n + m)^O(1) · 2^(n/(log n)^(1/2+o(1))), cioè subesponenziale. Il caso 3-SAT basta per confutare l’ETH.

Curiosamente, l’algoritmo non risponde solo “sì” o “no”, ma conta le soluzioni. Da qui l’articolo ricava ulteriori conseguenze:

1. algoritmi subesponenziali per contare le colorazioni dei grafi, gli insiemi indipendenti e gli accoppiamenti perfetti,
2. approssimazioni arbitrariamente precise per Max-k-SAT in tempo subesponenziale,
3. un nuovo limite inferiore sulla dimensione dei circuiti logici per la classe E^NP.

Secondo The Next Web, il modello ha trovato la dimostrazione il 16 ottobre e il giorno dopo era già verificata in Lean (un linguaggio formale con cui il computer controlla le dimostrazioni). Nella cronologia delle modifiche del repository, OpenAI indica che l’articolo è stato messo online insieme alla formalizzazione in Lean.

Chi sta verificando la dimostrazione?

Il gruppo che deve esaminare e spiegare la dimostrazione è guidato da Russell Impagliazzo, Ramamohan Paturi (UC San Diego) e Ryan Williams (MIT). Secondo la cronologia del repository, è stato proprio su richiesta di questo gruppo che i materiali sono stati pubblicati subito, perché tutti potessero verificarli. Williams ha scritto su X che un modello interno di OpenAI aveva prodotto una “claimed refutation of ETH”, cioè una confutazione dichiarata dell’ETH.

I ricercatori non hanno firmato alcun NDA e non vengono pagati per questo lavoro (secondo The Next Web). Hanno chiesto a OpenAI di rendere pubblici tutti i dati grezzi e di finanziare una conferenza sulle conseguenze del risultato, e l’azienda ha accettato. In una lettera aperta precisano però che la loro partecipazione non è una conferma del risultato (“should not be taken as certification of the claim”), aggiungendo che, se la dimostrazione è corretta, “it will change an important part of theoretical computer science”.

È una novità nel mondo dell’AI?

Non è la prima pubblicazione di questo tipo di OpenAI. Come sappiamo, il 6 ottobre l’azienda ha caricato nello stesso repository oltre 700 articoli matematici generati dal modello. Nel README del repository leggiamo che il modello ha ricevuto circa 4000 problemi aperti e che ogni risultato ha richiesto in media tre ore di “ragionamento” a livello di ChatGPT Pro.

La novità è che il 26 ottobre OpenAI ha annunciato tre risultati in una volta e ha scelto una strada diversa per ciascuno (lo descrive Unite.AI):

1. ETH: l’articolo e la prova in Lean sono pubblici, e li verifica un gruppo aperto guidato da Impagliazzo, Paturi e Williams.
2. La congettura di Sogge sul “local smoothing” in tutte le dimensioni, da cui secondo OpenAI seguono la congettura di Kakeya e la congettura di restrizione di Stein: anch’essa pubblicata con prova in Lean.
3. L’esistenza della teoria di Yang-Mills e della QCD in quattro dimensioni (uno dei Problemi del Millennio del Clay Institute): qui per ora non ci sono materiali. Un gruppo guidato dal premio Nobel David Gross ha deciso di descrivere il risultato in autonomia.

OpenAI dichiara inoltre di non volere il merito scientifico delle scoperte dei suoi modelli. Il riconoscimento deve andare alle persone che le capiranno e le descriveranno. L’azienda ha anche donato 5 milioni di USD alla Simons Foundation per workshop e conferenze sui risultati generati dall’AI.

A cosa fare attenzione?

Primo, allo stato della verifica. Una formalizzazione in Lean è un segnale forte, ma bisogna sempre controllare che il teorema scritto in Lean dica davvero la stessa cosa del testo dell’articolo. La stessa OpenAI scrive nel README che alcuni risultati senza formalizzazione possono contenere errori, e il 7 ottobre ha ritirato tre articoli per un errore di segno in una delle dimostrazioni. Prendiamo quindi il risultato con cautela finché il gruppo non avrà finito il suo lavoro.

Secondo, a ciò che il risultato non significa. Gli autori scrivono chiaramente che da esso non segue che tutti i problemi NP abbiano algoritmi subesponenziali. Quindi non è una soluzione del problema P vs NP, e il tempo di esecuzione cresce comunque più velocemente di qualsiasi polinomio.

Terzo, al ritmo. Un risultato su cui i teorici lavoravano da oltre 20 anni sarebbe stato trovato dal modello nel corso di una valutazione interna. Se verrà confermato, sarà probabilmente l’esempio più forte finora di un’AI che fa scoperte autonome nell’informatica teorica. Nel frattempo torna il tema delle dimostrazioni formali, di cui ho scritto a proposito della verifica formale con Claude.

FAQ

Che cos’è l’ipotesi del tempo esponenziale?

È il presupposto della teoria della complessità secondo cui 3-SAT non può essere risolto in meno di 2^Ω(n) per n variabili. L’hanno formulata Impagliazzo e Paturi con Francis Zane.

OpenAI ha risolto il problema P vs NP?

No. L’algoritmo è subesponenziale ma non polinomiale, e gli autori sottolineano che il risultato non si estende a tutti i problemi NP.

La confutazione dell’ETH è già confermata?

Non ancora. Esiste una formalizzazione in Lean, ma il gruppo indipendente di Impagliazzo, Paturi e Williams la sta appena esaminando e precisa che la sua partecipazione non equivale a una conferma.

Quale modello di OpenAI l’ha fatto?

Un modello interno non rivelato. Nel README del repository OpenAI non ne indica il nome.