Stanowiąc duży krok w rozwoju sztucznej inteligencji, zespół badawczy z Uniwersytetu Pekińskiego opracował system sztucznej inteligencji, który może samodzielnie rozwiązywać złożone, nierozwiązane problemy matematyczne. System pomyślnie rozwiązał hipotezę algebraiczną sprzed dziesięciu lat, wyznaczając przejście od wykorzystywania sztucznej inteligencji jako zwykłego asystenta do jej roli autonomicznego badacza.
Rozwiązywanie hipotezy algebraicznej
W centrum tego przełomu leżało założenie algebraiczne zaproponowane po raz pierwszy w 2014 roku przez nieżyjącego już Dana Andersona, byłego profesora Uniwersytetu Iowa. Przez dziesięć lat problem ten pozostawał otwartym wyzwaniem w dziedzinie algebry przemiennej.
W przeciwieństwie do poprzednich modeli sztucznej inteligencji, które wymagały ciągłego nadzoru ze strony człowieka, ten nowy system przetwarzał dziesięciolecia literatury matematycznej, aby rozwiązać hipotezę i – co najważniejsze – autonomicznie weryfikował jej wyniki bez interwencji człowieka. Cały proces zajął zaledwie 80 godzin pracy.
Architektura Autonomii: Rethlas i Archont
Aby przezwyciężyć tradycyjne ograniczenia sztucznej inteligencji w matematyce, badacze odeszli od standardowych modeli dużego języka (LLM), które często są podatne na „halucynacje” lub błędy logiczne. Zamiast tego stworzyli dwuagentową platformę zaprojektowaną tak, aby naśladować rygorystyczny przepływ pracy zawodowych matematyków:
- Reasoning Agent (Rethlas): Ten system działa jak „myśliciel”. Używa wyszukiwarki twierdzeń o nazwie Matlas, aby badać różne strategie i matematyczne sposoby rozwiązywania problemów.
- Agent Formalizacyjny (Archon): Po znalezieniu potencjalnego dowodu kontrola przechodzi na Archonta. Korzystając z narzędzia LeanSearch, przekłada nieformalne rozumowanie na formalny format możliwy do sprawdzenia maszynowego.
- Weryfikator (Lean 4): System wykorzystuje Lean 4 – specjalistyczny język programowania i interaktywnego asystenta dowodzenia twierdzeń – aby mieć pewność, że dowód jest matematycznie rzetelny i wolny od błędów.
Dlaczego to ma znaczenie: od pomocy po automatyzację
Obecne trendy w sztucznej inteligencji wskazują na silny wektor dla modeli szkoleniowych w matematyce, ale większość z nich nadal boryka się z „problemem rygorystyczności”. Chociaż ludzie potrafią pisać dowody, mogą popełniać błędy; chociaż LLM mogą szybko generować tekst, często brakuje im logicznej precyzji wymaganej w wyższej matematyce.
Badania Uniwersytetu w Pekinie wypełniają tę lukę poprzez połączenie rozumowania w języku naturalnym z weryfikacją formalną. To podwójne podejście gwarantuje, że sztuczna inteligencja nie tylko „odgadnie” odpowiedź, ale konstruuje dowód, który można zweryfikować matematycznie pod kątem poprawności.
Co więcej, badacze zauważyli, że sztuczna inteligencja wykazała się wyjątkową zdolnością do wykonywania zadań, które zazwyczaj wymagają współpracy interdyscyplinarnej, zasadniczo działając jako grupa ekspertów pracujących w tandemie.
Przyszłość badań matematycznych
Chociaż system działał autonomicznie, naukowcy zauważyli, że interwencja człowieka nadal może służyć jako akcelerator. Matematyk kierujący agentem Archonta może przyspieszyć proces formalizacji, torując drogę przyszłości, w której ludzie i sztuczna inteligencja będą działać w szybkim cyklu symbiotycznym.
„Ta praca jest konkretnym przykładem tego, jak badania matematyczne można w znacznym stopniu zautomatyzować za pomocą sztucznej inteligencji” – stwierdzili naukowcy.
Wniosek
Łącząc logiczne rozumowanie z rygorystyczną weryfikacją formalną, ta nowa architektura przenosi sztuczną inteligencję poza proste obliczenia w sferę autonomicznych odkryć naukowych. Ten przełom toruje drogę sztucznej inteligencji do rozwiązywania coraz bardziej złożonych problemów w matematyce i innych zaawansowanych technologicznie dziedzinach naukowych.
