OpenAI ujawnia Astrę. Nowy model pomaga rozwiązywać trudne problemy matematyczne

Astra nie jest jeszcze dostępna w ChatGPT ani przez API. OpenAI pokazało na razie wyniki badań. Część problemów model miał rozwiązać, w innych znalazł nowe podejście albo poprawił wcześniejsze wyniki.

Co właściwie zrobiła Astra?

Model pracował nad zagadnieniami z kilku dziedzin matematyki i informatyki. Brzmią one bardzo technicznie, ale ich sens da się wyjaśnić prościej.

Jednym z tematów było upakowanie kul w przestrzeni. W trzech wymiarach można to porównać do układania pomarańczy w skrzynce tak, żeby zmieściło się ich jak najwięcej. Matematycy badają podobne problemy także dla czterech, dziesięciu czy setek wymiarów. Nie da się ich sobie łatwo wyobrazić, ale mają znaczenie dla teorii informacji i przesyłania danych.

Astra zajmowała się też problemem najbliższego wektora. Chodzi o odnalezienie punktu położonego najbliżej wskazanego miejsca w ogromnej, regularnej sieci punktów. Takie problemy wykorzystuje się w kryptografii, między innymi przy projektowaniu zabezpieczeń odpornych na przyszłe komputery kwantowe.

Kolejny wynik dotyczył liczb Ramseya. W dużym uproszczeniu matematycy pytają tu, jak duża musi być grupa elementów, żeby zawsze dało się w niej znaleźć określony układ. Przykładem może być grupa ludzi, w której część osób się zna, a część nie. Po przekroczeniu pewnej liczby uczestników konkretny wzór relacji musi się pojawić.

Czym jest grupa niesoficzna?

Najwięcej uwagi wywołał wynik dotyczący grup soficznych.

W matematyce „grupa” nie oznacza zbioru ludzi. To zestaw obiektów wraz z regułą wykonywania na nich określonego działania. Może chodzić na przykład o obracanie figury, przestawianie elementów albo łączenie kolejnych ruchów.

Grupy soficzne można w pewnym sensie naśladować za pomocą prostszych, skończonych układów. Matematycy przez lata zastanawiali się, czy każda grupa przeliczalna ma tę cechę.

Astra miała skonstruować przykład grupy, której w taki sposób przybliżyć się nie da. Taki obiekt nazywa się grupą niesoficzną. Jeśli dowód zostanie zaakceptowany przez matematyków, oznacza to, że odpowiedź na wieloletnie pytanie brzmi: nie każda grupa jest soficzna.

Model podał też kontrprzykład

Astra przygotowała również kontrprzykład dla jednej z hipotez związanych z algebrami von Neumanna.

Hipoteza to twierdzenie, które wydaje się prawdziwe, ale nie zostało jeszcze udowodnione. Kontrprzykład jest pojedynczym przypadkiem pokazującym, że twierdzenie jednak nie działa zawsze.

Algebry von Neumanna to narzędzia używane między innymi w fizyce kwantowej i matematyce opisującej skomplikowane struktury. Nie trzeba znać ich budowy, żeby zrozumieć znaczenie wyniku: Astra miała znaleźć przykład podważający wcześniejsze przypuszczenie matematyków.

Jak sprawdzono dowody?

OpenAI zapisało dowody w systemie Lean 4. To specjalne oprogramowanie używane do komputerowego sprawdzania matematyki.

Polecana lektura

"Imperium sztucznej inteligencji. Sny i koszmary w OpenAI Sama Altmana"

To jest link afiliacyjny. Kupując za jego pomocą, wspieracie rozwój bloga, a cena dla Was pozostaje bez zmian.

Sprawdź cenę

Lean analizuje kolejne kroki dowodu i sprawdza, czy wynikają one z przyjętych zasad. Nie ocenia, czy problem jest ciekawy ani czy wynik zmienia daną dziedzinę nauki. Pilnuje za to, żeby w samym rozumowaniu nie było ukrytego błędu.

Można porównać go do bardzo rygorystycznego kontrolera. Człowiek zapisuje dowód, a system sprawdza każdą jego część.

OpenAI udostępniło pliki z formalnymi wersjami wszystkich dziesięciu wyników. Matematycy mogą je pobrać, uruchomić i sprawdzić niezależnie.

Czy Astra naprawdę rozwiązała te problemy?

Komputerowa kontrola w Lean nie zamyka sprawy. Naukowcy muszą jeszcze ocenić, czy definicje zostały dobrane prawidłowo, czy wynik rzeczywiście odpowiada na postawione pytanie i jak duże ma znaczenie.

W matematyce zdarza się, że dowód jest formalnie poprawny, ale dotyczy węższej wersji problemu, niż sugeruje nagłówek. Dlatego wyniki Astry wymagają teraz niezależnej analizy.

Skąd wzięła się kwota 2000 dolarów?

OpenAI podało, że liczba tokenów zużytych podczas szukania dziesięciu wyników kosztowałaby około 2000 dolarów według cennika API modelu Sol.

Token to mały fragment tekstu przetwarzany przez model. Może nim być całe słowo, jego część albo znak interpunkcyjny. Firmy rozliczają korzystanie z modeli AI właśnie na podstawie liczby tokenów.

Kwota 2000 dolarów nie oznacza więc, że tyle kosztowało stworzenie Astry. Nie obejmuje treningu modelu, serwerów ani pracy badaczy. To wyłącznie szacunek ceny obliczeń wykonanych podczas tego konkretnego eksperymentu.

Wielu agentów pracujących razem

Według serwisu „The Information” Astra ma działać jako zespół wielu agentów AI.

Agent AI to program oparty na modelu językowym, który może otrzymać zadanie, wykonać serię kroków, korzystać z narzędzi i poprawiać własne wyniki. Kilku agentów może podzielić między siebie pracę. Jeden szuka pomysłu, drugi sprawdza obliczenia, kolejny próbuje znaleźć błąd.

Taki system może pracować nad jednym problemem przez wiele godzin, a nawet dni. Różni się więc od zwykłego chatbota, który odpowiada po kilku lub kilkudziesięciu sekundach.

OpenAI nie podało jeszcze daty premiery Astry. Nie wiadomo również, czy model trafi do ChatGPT, API czy do osobnej usługi.