To właśnie twierdzenie, jakoby system sztucznej inteligencji obalił wspomnianą hipotezę ETH (Exponential Time Hypothesis) wywołało najwięcej emocji. Dlaczego? Powód jest prosty: jej podważenie mogłoby wpłynąć na rozumienie trudności obliczeniowej wielu problemów i skłonić badaczy do ponownego przeanalizowania wyników opartych na tym założeniu.
Czytaj też: Sztuczna inteligencja trafiła na bezludną wyspę. Sprawy błyskawicznie przybrały niespodziewany obrót
Hipoteza ETH zakłada bowiem, iż niektórych problemów obliczeniowych nie da się rozwiązywać znacząco szybciej niż w czasie wykładniczym względem liczby zmiennych. Dotyczy między innymi problemu spełnialności formuł logicznych, znanego jako SAT i jest wykorzystywana w analizach złożoności algorytmów.
Według OpenAI jej model opracował deterministyczny algorytm działający w czasie podwykładniczym dla określonych problemów związanych z formułami boolowskimi. Taki rezultat miałby podważać podstawy wielu wcześniejszych analiz dotyczących granic wydajności obliczeń. W praktyce mógłby utorować drogę do poszukiwania szybszych algorytmów w teorii grafów, bioinformatyce czy geometrii obliczeniowej.
Firma udostępniła opis rozwiązania oraz jego formalizację w Lean, czyli systemie służącym do komputerowego sprawdzania dowodów matematycznych. W niezależnej ocenie wyniku ma wziąć zespół specjalistów złożony między innymi z Russella Impagliazzy, Ramamohana Paturiego i Ryana Williamsa. Dopiero ich analiza pozwoli ustalić, czy przedstawiony dowód rzeczywiście obala ETH w deklarowanym zakresie.
Drugie osiągnięcie dotyczy natomiast hipotezy lokalnego wygładzania, związanej z analizą harmoniczną i zachowaniem fal opisanych równaniami różniczkowymi. Według OpenAI wdrożone modele opracowały dowód obowiązujący we wszystkich wymiarach przestrzennych. Wynik ten ma również konsekwencje dla hipotezy Kakeyi oraz problemów związanych z ograniczeniami transformat Fouriera. Jeśli dowód doczeka się potwierdzenia, może mieć znaczenie dla rozwoju matematyki zajmującej się równaniami falowymi i analizą harmoniczną. Firma opublikowała materiały umożliwiające badaczom zapoznanie się z rozumowaniem modelu i jego formalną weryfikacją.
Czytaj też: Matematyczne wzory zamieniły się w dzieła sztuki. Tak zachwyca nowa technologia
Trzecie odkrycie obejmuje zaś zagadnienia kwantowej chromodynamiki (QCD), czyli teorii opisującej oddziaływania silne między kwarkami i gluonami, oraz matematycznych podstaw modelu standardowego fizyki cząstek. OpenAI deklaruje, że jej model przygotował rygorystyczny dowód istnienia określonych oddziałujących teorii pól kwantowych w czterech wymiarach. Wynik wiąże się z problemem Yang-Millsa, należącym do słynnych problemów milenijnych Instytutu Matematycznego Claya, za rozwiązanie którego pomysłodawcy przewidzieli nagrodę w wysokości miliona dolarów.
W tle powyższych ogłoszeń trwa dyskusja na temat roli sztucznej inteligencji w badaniach naukowych. Pojawiają się bowiem pytania o sposób weryfikowania odkryć i przyznawania autorstwa. Formalne sprawdzenie dowodu w Lean jest ważnym krokiem, jednak nie kończy dyskusji: trzeba będzie upewnić się, czy formalny zapis odpowiada rzeczywistemu problemowi, który badacze zamierzali rozwiązać. Dodatkowe emocje wywołuje konkurencja między laboratoriami AI. Anthropic również ogłosiło wynik podważający ETH, dlatego rywalizacja na tym polu może być nader emocjonująca.
Źródło: New Scientist
