Hipoteza czasu wykładniczego obalona przez model OpenAI?

26 października OpenAI opublikowało w repozytorium openai/math pracę „The Exponential Time Hypothesis is False”. Według niej nieujawniony wewnętrzny model OpenAI obalił hipotezę czasu wykładniczego (ETH), jedno z podstawowych założeń teorii złożoności obliczeniowej. Pracę razem z formalizacją w Lean bada niezależna grupa informatyków, wśród nich dwaj współautorzy samej hipotezy.

Czym jest hipoteza czasu wykładniczego?

ETH (Exponential Time Hypothesis) zakłada, że problemu 3-SAT, czyli sprawdzenia, czy da się spełnić formułę logiczną z klauzulami po trzy zmienne, nie da się rozstrzygnąć szybciej niż w czasie 2^Ω(n) dla n zmiennych. Mówiąc prościej: przy każdej dodatkowej zmiennej czas rośnie wykładniczo i żaden sprytny algorytm tego nie zmieni.

Hipotezę sformułowali Russell Impagliazzo i Ramamohan Paturi (z Francisem Zane). Na ETH opierają się setki prac, które dowodzą, że jakiś problem w grafach, bazach danych czy biologii obliczeniowej „nie może” być rozwiązany szybciej (jak przypomina The Next Web).

Co dokładnie udowodnił model OpenAI?

Praca podaje deterministyczny algorytm, który dokładnie liczy wszystkie spełniające przypisania formuły k-CNF dla każdego ustalonego k ≥ 2. Działa w pamięci wielomianowej i w czasie (n + m)^O(1) · 2^(n/(log n)^(1/2+o(1))), czyli subwykładniczym. Przypadek 3-SAT wystarcza, żeby obalić ETH.

Co ciekawe, algorytm nie tylko odpowiada „tak” lub „nie”, ale liczy rozwiązania. Z tego w pracy wyprowadzone są kolejne wnioski:

1. subwykładnicze algorytmy do liczenia kolorowań grafów, zbiorów niezależnych i doskonałych skojarzeń,
2. dowolnie dokładne przybliżenia dla Max-k-SAT w czasie subwykładniczym,
3. nowe dolne ograniczenie na rozmiar obwodów logicznych dla klasy E^NP.

Według The Next Web model znalazł dowód 16 października, a dzień później był on już zweryfikowany w Lean (formalnym języku do sprawdzania dowodów przez komputer). W historii zmian repozytorium OpenAI podaje, że praca trafiła do sieci z formalizacją w Lean.

Kto sprawdza dowód?

Grupą, która ma zbadać i wytłumaczyć dowód, kierują Russell Impagliazzo, Ramamohan Paturi (UC San Diego) i Ryan Williams (MIT). Według historii zmian repozytorium to właśnie na prośbę tej grupy materiały opublikowano od razu, żeby mogli je sprawdzać wszyscy. Williams napisał na X, że wewnętrzny model OpenAI wyprodukował „claimed refutation of ETH”, czyli deklarowane obalenie ETH.

Badacze nie podpisali żadnych NDA i nie biorą za to pieniędzy (według The Next Web). Poprosili OpenAI o upublicznienie wszystkich surowych danych i sfinansowanie konferencji o skutkach wyniku, a firma się zgodziła. W liście otwartym zastrzegają jednak, że ich udział nie jest potwierdzeniem wyniku (cytując „should not be taken as certification of the claim”), dodając, że jeśli dowód jest poprawny, „it will change an important part of theoretical computer science”.

Czy to coś nowego w świecie AI?

To nie pierwsza taka publikacja OpenAI. Jak wiemy, 6 października firma wrzuciła do tego samego repozytorium ponad 700 prac matematycznych wygenerowanych przez model. W README repozytorium czytamy, że model dostał ok. 4000 otwartych problemów, a na każdy wynik przypadało średnio trzy godziny „myślenia” na poziomie ChatGPT Pro.

Nowe jest to, że 26 października OpenAI ogłosiło od razu trzy wyniki i dla każdego wybrało inną drogę (opisuje to Unite.AI):

1. ETH – praca i dowód w Lean są publiczne, a sprawdza je otwarta grupa Impagliazzo, Paturiego i Williamsa.
2. Hipoteza Sogge’a o „local smoothing” we wszystkich wymiarach, z której według OpenAI wynikają hipoteza Kakeyi i hipoteza restrykcji Steina – też opublikowana z dowodem w Lean.
3. Istnienie teorii Yanga-Millsa i QCD w czterech wymiarach (jeden z problemów milenijnych Instytutu Claya) – tu materiałów na razie nie ma. Grupa pod kierunkiem noblisty Davida Grossa postanowiła sama opisać wynik.

OpenAI deklaruje przy tym, że nie chce zasług naukowych za odkrycia swoich modeli. Uznanie mają dostać ludzie, którzy je zrozumieją i opiszą. Firma przekazała też 5 mln USD Fundacji Simonsa na warsztaty i konferencje o wynikach wygenerowanych przez AI.

Na co zwrócić uwagę?

Po pierwsze, na stan weryfikacji. Formalizacja w Lean to mocny sygnał, ale zawsze trzeba sprawdzić, czy twierdzenie zapisane w Lean naprawdę mówi to samo, co tekst pracy. Samo OpenAI pisze w README, że część wyników bez formalizacji może mieć błędy, a 7 października wycofało trzy prace przez błąd znaku w jednym z dowodów. Traktujmy więc wynik z dystansem, dopóki grupa nie skończy pracy.

Po drugie, na to, czego wynik nie oznacza. Autorzy piszą wprost, że nie wynika z niego, że wszystkie problemy NP mają algorytmy subwykładnicze. To więc nie jest rozstrzygnięcie problemu P vs NP, a czas działania nadal rośnie szybciej niż jakikolwiek wielomian.

Po trzecie, na tempo. Wynik, nad którym teoretycy pracowali od ponad 20 lat, model miał znaleźć w ramach wewnętrznej ewaluacji. Jeśli się potwierdzi, będzie to chyba najmocniejszy jak dotąd przykład, że AI robi samodzielne odkrycia w informatyce teoretycznej. Przy okazji wraca temat formalnych dowodów, o którym pisałem przy weryfikacji formalnej z Claude.

FAQ

Co to jest hipoteza czasu wykładniczego?

To założenie z teorii złożoności, że problemu 3-SAT nie da się rozwiązać w czasie krótszym niż 2^Ω(n) dla n zmiennych. Sformułowali je Impagliazzo i Paturi z Francisem Zane.

Czy OpenAI rozwiązało problem P vs NP?

Nie. Algorytm jest subwykładniczy, ale nie wielomianowy, a autorzy zaznaczają, że wynik nie przenosi się na wszystkie problemy NP.

Czy dowód obalenia ETH jest już potwierdzony?

Na razie nie. Istnieje formalizacja w Lean, ale niezależna grupa Impagliazzo, Paturiego i Williamsa dopiero go bada i zastrzega, że jej udział nie oznacza potwierdzenia.

Który model OpenAI to zrobił?

Nieujawniony wewnętrzny model. W README repozytorium OpenAI nie podaje jego nazwy.