PSI informuje o sprawdzonym maszynowo dowodzie hipotezy Aaronsona–Ambainisa

Physical Superintelligence ogłosiła 6 listopada 2026 r., że wewnętrzny system badawczy, uruchamiający instancje niepublicznego modelu Anthropic, znalazł dowód hipotezy Aaronsona–Ambainisa — problemu z dziedziny obliczeń kwantowych, który pozostawał nierozwiązany od 2008 r.

System wygenerował kompletny dowód trzeciego dnia działania w infrastrukturze należącej do PSI, a asystent dowodzenia Lean zaakceptował go. Następnie PSI zleciła systemowi rozwiązanie pokrewnych otwartych problemów. System dwukrotnie ulepszył wynik, zanim Lean zaakceptował ostateczną wersję. Manuskrypt i formalizacja w Lean 4 są publicznie dostępne.

Co hipoteza mówi o przyspieszeniu obliczeń kwantowych

Pytanie dotyczy tego, kiedy komputery kwantowe mogą działać wykładniczo szybciej niż maszyny klasyczne. Algorytm Shora z 1994 r. służący do faktoryzacji zależy od struktury: jego dane wejściowe zawierają powtarzający się wzorzec, który algorytm może wykorzystać. Wynik PSI dotyczy odmiennego przypadku danych losowych lub pozbawionych struktury, w których zazwyczaj nie ma takiego wzorca.

W modelu zapytań algorytm klasyczny odczytuje jeden bit na zapytanie, natomiast zapytanie kwantowe może obejmować w superpozycji wiele pozycji danych wejściowych. Wyjaśnienie PSI łączy ten model z wielomianami: po T zapytaniach kwantowych prawdopodobieństwo, że algorytm odpowie „tak”, jest wielomianem ograniczonym wartościami, zależnym od bitów wejściowych i mającym stopień nie większy niż 2T. Symulacja algorytmu kwantowego sprowadza się więc do oszacowania tego wielomianu bez odczytywania wykładniczo dużej liczby bitów wejściowych.

W swojej pierwotnej pracy Scott Aaronson i Andris Ambainis wysunęli hipotezę, że każdy ograniczony wielomian niskiego stopnia ma zmienną o dużym wpływie. Dowiedli, że przy założeniu prawdziwości tej hipotezy każdy algorytm kwantowy wykonujący T zapytań można zasymulować dla większości danych wejściowych za pomocą algorytmu klasycznego, który wykonuje wielomianowo wiele zapytań w T. Oznacza to wielomianowy, a nie wykładniczy wzrost liczby zapytań klasycznych przy każdym ustalonym błędzie przybliżenia i odsetku wykluczonych danych wejściowych; nie wyklucza to wykładniczej przewagi kwantowej w problemach o odpowiedniej strukturze.

Formalnie repozytorium rozpatruje wielomian rzeczywisty p stopnia co najwyżej d, którego wartości na kostce dyskretnej mieszczą się w przedziale od 0 do 1. Jeśli jego wariancja względem jednostajnie losowanych danych wejściowych wynosi co najmniej ε, to pewna współrzędna ma wpływ co najmniej (8√15 / (125π⁴)) · ε^(5/2) / d⁶, a w konsekwencji co najmniej (ε/d)⁷. Wpływ to oczekiwana wartość kwadratu zmiany p po odwróceniu bitu w tej współrzędnej.

Jak skonstruowano i sprawdzono dowód

Dowód opiera się na planie Shachara Lovetta i Jiapenga Zhanga, wykorzystującym certyfikaty ułamkowe i zbiory poziomicowe, ale zastępuje nierówność, którą w tym planie pozostawiono jako hipotezę, nową nierównością obejmującą wszystkie pary. Wyznacznik tworzy bijekcję parującą ustawienia danych wejściowych. Według PSI parowanie to wykracza poza słabsze parowanie z lematu motylkowego Davida Reimera, ponieważ ogranicza również częstość, z jaką sparowane ustawienia są zgodne na każdej współrzędnej — a takie ograniczenie jest potrzebne do nowej nierówności.

Repozytorium dzieli elementarny dowód na cztery części: wyprowadzenie nierówności dla wszystkich par z wyznacznika i bijekcji, całkowanie po zbiorach poziomicowych, uśrednianie względem współrzędnych oraz wykazanie ograniczenia dla wiersza za pomocą punktowego ograniczenia czułości. Łącznie kroki te prowadzą do jawnego ograniczenia wpływu.

Zgodnie z audytem odnotowanym w repozytorium formalizacja nie zawiera żadnych nieuzupełnionych fragmentów dowodu ani dodatkowych aksjomatów. Jej deklaracje ponownie sprawdzono za pomocą jądra Lean oraz lean4lean, niezależnej implementacji sprawdzarki typów Lean. W odizolowanym środowisku program porównujący, korzystający z jąder nanoda i Lean, zaakceptował cztery końcowe twierdzenia; na drugim komputerze zaakceptował jedno poprawne, niewielkie rozwiązanie i odrzucił cztery celowo błędne.

Kontrole te mają wyraźne ograniczenia. Czytelnik nadal musi potwierdzić, że sformalizowane twierdzenie odpowiada hipotezie przedstawionej w publikacji. Artykuł w formie czytelnej dla człowieka nie został sam w sobie sprawdzony maszynowo, a jądro i kompilator Lean, definicje Mathlib oraz komputery użyte do weryfikacji nadal należą do zaufanej podstawy.

Rola ludzi i weryfikacja ekspercka

David Turturean, członek zespołu technicznego PSI, opracował i uruchomił system badawczy, wybrał zakres problemu, skłonił model do przygotowania pierwszej wersji projektu, zrecenzował ją i odpowiada za poprawność artykułu. W repozytorium ujawniono, że modele AI wygenerowały twierdzenia matematyczne, pierwszy projekt oraz formalizację w Lean. Jim Halverson przeprowadził audyt dowodu, a Phiala Shanahan zgłosiła uwagi do formalizacji.

Ogłoszenie następuje po pracy zgłoszonej 19 sierpnia 2026 r. przez Guya Blanca, Jordana Doctera, Carmen Strassle i Li-Yang Tana. Autorzy ci rozstrzygnęli konsekwencję dotyczącą klasycznej symulacji równoległych algorytmów kwantowych, dowodząc, że algorytm wykonujący t zapytań w d rundach można zasymulować dla większości danych wejściowych przy użyciu t^(O(d²)) zapytań klasycznych. PSI informuje, że cała czwórka zapoznała się z pełnym dowodem, przekazała uwagi i przygotowuje krótsze omówienie dla ekspertów.

W ocenie opublikowanej przez PSI badacze napisali: „To ogromny wynik. Rozstrzyga hipotezę, która od dziesięcioleci pozostawała nierozwiązana, i ma istotne konsekwencje dla zrozumienia natury problemów, w których można uzyskać przyspieszenie kwantowe. Dowód wykorzystuje i rozwija kilka nurtów badań nad analizą funkcji boolowskich i kombinatoryką probabilistyczną. Wszystko łączy się w dość magiczny sposób”.

Bezpośredni test jest wyjątkowo konkretny: niezależne jądra mogą odtworzyć zakodowany argument, ale eksperci muszą jeszcze potwierdzić, że zakodowane twierdzenie odpowiada hipotezie Aaronsona i Ambainisa, oraz ocenić te części artykułu, które nie zostały sformalizowane w Lean. Ten podział wyznacza, co potwierdzają kontrole maszynowe, a co nadal wymaga matematycznej weryfikacji przez człowieka.