OpenAI twierdzi, że jego model obalił hipotezę ETH. Wynik czeka na weryfikację ekspertów

W opublikowanym 26 października wpisie o współpracy ze środowiskami akademickimi OpenAI przedstawiło trzy wyniki, które mają pochodzić od jego modeli. Dotyczą obliczeniowej hipotezy ETH, hipotezy lokalnego wygładzania oraz problemów związanych z kwantową teorią pola. Jak opisuje to Chip.pl, najwięcej uwagi przyciąga pierwszy z nich.

ETH: algorytm, który miał nie istnieć

Exponential Time Hypothesis pochodzi z 1999 roku. Zakłada, że niektórych problemów obliczeniowych, w tym spełnialności formuł logicznych (SAT), nie da się rozwiązać znacząco szybciej niż w czasie wykładniczym względem liczby zmiennych. Na tym założeniu opiera się wiele analiz złożoności algorytmów, więc jego podważenie zmusiłoby badaczy do ponownego przyjrzenia się wynikom, które z niego wynikają.

Według OpenAI model opracował deterministyczny algorytm działający w czasie podwykładniczym dla określonych problemów z formułami boolowskimi. Firma podaje daty: dowód w języku naturalnym miał powstać 16 października, a jego formalizacja w systemie Lean, służącym do komputerowego sprawdzania dowodów, 17 października. Opis rozwiązania i zapis w Lean zostały udostępnione.

Nie oznacza to jeszcze, że sprawa jest zamknięta. Ocenić wynik ma zespół specjalistów, wśród których są Russell Impagliazzo, Ramamohan Paturi i Ryan Williams. Dopiero ich analiza pokaże, czy dowód faktycznie obala ETH w deklarowanym zakresie. Sam zapis w Lean też nie rozstrzyga wszystkiego: trzeba jeszcze sprawdzić, czy formalne sformułowanie odpowiada problemowi, który badacze naprawdę mieli na myśli.

Lokalne wygładzanie i Yang-Mills

Drugi wynik dotyczy hipotezy lokalnego wygładzania, związanej z analizą harmoniczną i falami opisywanymi równaniami różniczkowymi. OpenAI deklaruje, że jego modele „produced a proof of the local smoothing conjecture in every dimension”, a tym samym rozstrzygają też hipotezę Kakeyi i hipotezę restrykcyjną Steina we wszystkich wymiarach. Wynik miał pojawić się 18 października, a formalizacja w Lean dzień później. Wolfram MathWorld zaznacza w haśle o tej hipotezie, że według stanu na 27 października niezależne potwierdzenie pełnego argumentu przez specjalistów nie zostało zgłoszone.

Trzeci wynik jest najbardziej odległy od informatyki. OpenAI twierdzi, że jego model przygotował rygorystyczny dowód istnienia określonych oddziałujących teorii pól kwantowych w czterech wymiarach. Wiąże się to z problemem Yang-Millsa, jednym z problemów milenijnych Instytutu Claya z nagrodą miliona dolarów. Źródła nie mówią jednak, że problem został rozwiązany. W podanych datach formalizacje w Lean dotyczą tylko dwóch pierwszych wyników.

Kto sprawdzi sprawdzających

To nie pierwsza taka zapowiedź OpenAI. W maju pisaliśmy o obaleniu hipotezy Paula Erdősa, a w połowie października o wątpliwościach matematyków wobec opisu dowodu OpenAI. Od takich ogłoszeń do przyjęcia wyniku przez środowisko zwykle prowadzi długa droga recenzji. Spór o autorstwo i sposób weryfikacji odkryć dokonanych z udziałem AI dopiero się rozkręca.

Dodatkowy wątek to konkurencja. Według New Scientist Anthropic również ogłosiło wynik podważający ETH. Branżowe komentarze nazywają to „dueling proofs”, jak w tytule tekstu Scientific American. Jeśli oba dowody się obronią, ETH przestanie być punktem odniesienia. Wtedy pozostanie jeszcze ustalić, które z laboratoriów było pierwsze, a obie firmy mają w tym oczywisty interes.