Hipoteza Aaronsona-Ambainisa. Dowód z modelem Anthropic

Co ogłosiło PSI

PSI to spółka z siedzibą w Cambridge w stanie Massachusetts, która opisuje się jako laboratorium fizyki oparte na AI. Według firmy jej wewnętrzny system, uruchomiony na własnej infrastrukturze, korzystał z instancji niepublicznego modelu Anthropic. W trzecim dniu pracy miał kompletny dowód, który zaakceptował Lean, czyli program sprawdzający każdy krok rozumowania.

Potem PSI zleciło systemowi pokrewne otwarte problemy i dwukrotnie uzyskało lepszy wynik. Ostateczną wersję Lean także zaakceptował. Rękopis i formalizacja są publicznie dostępne w repozytorium GitHub. Nazwy modelu nie podano, a Anthropic nie odpowiedział na prośbę Business Insidera o komentarz.

Czego dotyczy hipoteza Aaronsona-Ambainisa

Hipoteza odpowiada na pytanie, kiedy komputer kwantowy może być wykładniczo szybszy od zwykłego. Znane wielkie przyspieszenia, jak algorytm Shora z 1994 roku, wykorzystują strukturę. Liczba rozkładana na czynniki kryje powtarzalny wzorzec, a maszyna kwantowa go wykrywa. Scott Aaronson i Andris Ambainis zapytali, co się dzieje, gdy takiego wzorca nie ma, czyli gdy dane są losowym ciągiem zer i jedynek.

Do porównania służy model zapytań. Nie liczy się w nim wszystkich operacji, tylko to, ile razy algorytm sięga do danych. Autorzy sprowadzili problem do hipotezy o wielomianach. Mówi ona, że jeśli wielomian niskiego stopnia o wartościach od 0 do 1 nie jest prawie stały, to przynajmniej jeden bit wejściowy ma na niego zauważalny wpływ. Zwykły komputer może wtedy odczytywać najważniejsze bity po kolei i przewidzieć odpowiedź maszyny kwantowej.

Nowa praca dowodzi tej zależności. Dla pytań typu tak lub nie zwykły komputer przybliża odpowiedź algorytmu kwantowego na prawie wszystkich losowych danych. Potrzebuje przy tym liczby odczytów rosnącej wielomianowo, a nie wykładniczo, względem liczby odczytów maszyny kwantowej.

Co wynik zmienia, a czego nie

Dowód potwierdza to, czego badacze od dawna się spodziewali, i ustawia wyraźniejszą granicę dla poszukiwań algorytmów kwantowych. Łatwo jednak przypisać mu więcej, niż z niego wynika.

• Zmienia - wiadomo, że wykładnicza przewaga w liczbie odczytów na pytaniach tak lub nie wymaga struktury danych.
• Nie zmienia - to nie jest granica całkowitego czasu pracy, bo koszt obróbki odczytanych danych może być ogromny.
• Nie zmienia - nie wynika stąd, że zwykłe komputery sprawnie naśladują każdy algorytm kwantowy.
• Nie zmienia - algorytm Shora nadal działa, bo problem rozkładu na czynniki ma strukturę.
• Nie rozstrzyga - które zastosowania dadzą użyteczne przyspieszenie w praktyce.

Co sprawdzono, a co czeka na ekspertów

Trzeba oddzielić kontrolę maszynową od oceny matematyków. Według repozytorium formalizacja w Lean 4 nie zawiera luk ani dodatkowych założeń, a dwa niezależne programy sprawdzające potwierdziły główne twierdzenia. To mocny sygnał, ale nie koniec weryfikacji.

Czytelnik musi jeszcze ocenić, czy zapis w Lean naprawdę odpowiada hipotezie w jej oryginalnym brzmieniu. Samego tekstu pracy maszyna nie sprawdza. Wariant z lepszą stałą opiera się dodatkowo na twierdzeniu innych autorów, którego nie sformalizowano. Praca nie przeszła recenzji w czasopiśmie, a na blogu Scotta Aaronsona nie znaleźliśmy do 7 listopada rano żadnego wpisu o tym dowodzie.

Najmocniejsza ocena zewnętrzna pochodzi od czworga badaczy ze Stanforda, którzy w sierpniu rozstrzygnęli przypadek szczególny. Guy Blanc, Jordan Docter, Carmen Strassle i Li-Yang Tan nazwali wynik "a huge result" i przygotowują jego krótsze omówienie dla specjalistów. Cytat znamy z komunikatu PSI, a nie z ich osobnej publikacji.

Kto jest autorem dowodu

Repozytorium przyznaje wprost, że dowód, tekst pracy i formalizację wytworzyły modele AI. David Turturean z PSI zbudował system, wybrał problem i uruchomił obliczenia, a potem przejrzał szkic i odpowiada za poprawność pracy. Dowód opiera się na planie Shachara Lovetta i Jiapenga Zhanga. Lukę w tym planie zastępuje nowa nierówność, wyprowadzona z nowego parowania układów bitów.

Tak wygląda coraz więcej takich ogłoszeń. Meta opisywała w październiku prace z Muse Spark, a OpenAI w tym roku pokazało 722 prace matematyczne i dowód dla problemu Naviera-Stokesa, wokół którego matematycy spierają się o rzeczywiste źródło metody. W naszej ocenie to dobra lekcja przed czytaniem podobnych komunikatów. Lean sprawdza poprawność rozumowania, ale nie mówi, skąd wziął się pomysł ani ile pracy wykonał człowiek.

Co to oznacza dla firm w Polsce

Dla działów bezpieczeństwa wniosek jest krótki, bo wynik niczego nie przyspiesza ani nie opóźnia. Plany przejścia na kryptografię odporną na komputery kwantowe pozostają aktualne, ponieważ algorytm Shora nie jest objęty tym ograniczeniem. O stanie starych kluczy więcej mówi opisana przez nas praca Google DeepMind o RSA-1024.

Bardziej praktyczny jest sygnał dla osób oceniających narzędzia badawcze. Przy kolejnym ogłoszeniu tego typu warto zadać cztery pytania.

1. Czy formalny zapis twierdzenia porównał ktoś spoza firmy?
2. Czy opublikowano dowód, kod i ślad pracy modelu?
3. Kto wybrał problem i kto odpowiada za wynik?
4. Czy wypowiedzieli się badacze niezależni od autora ogłoszenia?