OpenAI dichiara che un modello di intelligenza artificiale ha trovato un modo per confutare l'Ipotesi del Tempo Esponenziale (ETH), una congettura informatica formulata nel 1999. L'affermazione non ha alcun legame con Ethereum, la criptovaluta che viene scambiata con il ticker ETH, né con il cofondatore di Ethereum Vitalik Buterin.

L'annuncio ha tuttavia suscitato battute su tutto Crypto Twitter. "Dannazione, gli algo trader hanno appena massacrato $ETH", ha scritto su X un utente di nome Takumi, mentre Andrew Jiang ha scherzato: "Vitalik è stato molto silenzioso da quando è uscita questa notizia".

L'ETH in questione è stata proposta dagli informatici Russell Impagliazzo, Ramamohan Paturi e Francis Zane. Secondo l'ipotesi, il problema logico noto come 3-SAT non può essere risolto in modo sostanzialmente più rapido rispetto all'esame di ogni possibile combinazione di variabili. Nel 3-SAT, l'obiettivo è determinare se assegnazioni vero/falso possano soddisfare un insieme di regole, ciascuna contenente tre variabili.

Centinaia di articoli accademici si sono basati sull'ipotesi per stabilire che alcuni problemi di teoria dei grafi, biologia computazionale, database e geometria non possono essere risolti rapidamente, secondo OpenAI. L'azienda ha dichiarato che la confutazione dell'ETH potrebbe riaprire interrogativi su quanto più rapidamente tali compiti potrebbero essere risolti e aiutare i ricercatori nella ricerca di algoritmi migliorati.

"La confutazione dell'ETH riapre interrogativi su quanto più rapidamente questi compiti potrebbero diventare", ha scritto OpenAI nel suo post sul blog, "e potrebbe aiutare a orientare la ricerca di algoritmi migliori".

L'articolo di 67 pagine di OpenAI, datato 17 ottobre e revisionato il 25 ottobre, descrive un algoritmo deterministico—che non utilizza casualità—che conta ogni assegnazione soddisfacente per questi enigmi in tempo subesponenziale. Ciò significa che la quantità di lavoro cresce più lentamente di qualsiasi funzione esponenziale del numero di variabili. Poiché contare il numero di soluzioni è più difficile che determinare se esiste almeno una soluzione, il risultato risolve anche il problema decisionale.

OpenAI ha dichiarato che la sua AI ha scoperto la confutazione il 16 ottobre e che il risultato è stato formalizzato in Lean, un software che verifica meccanicamente ogni passaggio logico, il 17 ottobre. L'articolo e la formalizzazione sono disponibili su GitHub. OpenAI ha dichiarato che questo è avvenuto dopo la pubblicazione di 722 manoscritti matematici all'inizio del mese, di cui solo 162 includevano un risultato principale verificato al computer. È proprio quel formato verificabile da macchina a permettere ai ricercatori indipendenti di verificare autonomamente ogni passaggio dell'argomentazione.

Impagliazzo, Paturi e il professore del MIT Ryan Williams stanno guidando un esame indipendente dell'affermazione. In una lettera aperta, hanno avvertito che la loro partecipazione non deve essere interpretata come un'approvazione.

"Il nostro coinvolgimento non deve essere considerato una certificazione dell'affermazione", hanno scritto i tre, aggiungendo che "un risultato di questa importanza richiede un attento esame indipendente e la consapevolezza che altri possano ricostruirlo, metterlo in discussione e construirsi sopra".

OpenAI ha dichiarato che i partecipanti non hanno firmato accordi di riservatezza e lavorano senza compenso. L'azienda ha inoltre accettato di pubblicare tutti i dati grezzi e di finanziare una conferenza dedicata al risultato.

Le implicazioni pratiche restano incerte. "Trovare tali algoritmi e trasformare i progressi teorici in miglioramenti pratici richiederà ulteriori ricerche significative", ha scritto OpenAI. L'articolo precisa inoltre che il risultato non dimostra che ogni problema della classe di complessità NP possa essere risolto in tempo subesponenziale.

Ciò significa che il problema P versus NP resta aperto. P comprende i problemi che i computer possono risolvere in modo efficiente, mentre NP comprende i problemi per i quali le soluzioni proposte possono essere verificate in modo efficiente. La domanda irrisolta è se ogni problema la cui risposta può essere verificata efficientemente possa anche essere risolto efficientemente.

Anthropic è entrata nella discussione il 26 ottobre con un articolo attribuito a Claude e intitolato "A 2^o(n) Time Algorithm for 3-SAT". Il repository, che affronta anch'esso il problema dell'ETH, dichiara che un modello Claude di ricerca interno ha scoperto l'algoritmo. Aggiunge che "il risultato è puramente asintotico e non dice nulla sulla risoluzione pratica delle formule".

Claude ha formalizzato l'Ultimo Teorema di Fermat in Lean a settembre. Il matematico Terence Tao aveva messo in guardia sulla possibilità di sforzi di AI sovrapposti, scrivendo a settembre: "Abbiamo ormai visto che persino la voce che qualcuno stia lavorando a un problema può innescare un'enorme quantità di sforzo alimentato dall'AI per appiattirlo prima che il progetto di ricerca originale abbia il tempo di raggiungere il suo pieno potenziale".

Il recente contributo di 5 milioni di dollari di OpenAI alla Simons Foundation finanzierà workshop, conferenze e programmi speciali destinati ad aiutare i ricercatori a esaminare e sviluppare i risultati prodotti con l'AI.

Fonte: Decrypt