Zdjęcie: © Vitaly Gariev / Unsplash
Źródło: unsplash.com/photos/XeHplGPXZ_E
Sztuczna inteligencja coraz sprawniej rozwiązuje trudne problemy matematyczne. Dla matematyków sama odpowiedź nie jest jednak jedyną wartością dowodu. Równie ważne może być to, co sposób rozumowania mówi o problemie i czy pozwala budować kolejne wyniki. Najnowsze badanie Google DeepMind pokazuje, że system AI może skutecznie pracować nad otwartymi problemami, ale jednocześnie uwidacznia ograniczenia automatycznej weryfikacji oraz ryzyko utraty współpracy między badaczami.
W recenzowanej publikacji, która stała się publiczna 8 października w czasopiśmie Science, badacze opisali działanie systemu AlphaProof Nexus. System rozwiązał dziewięć problemów z kolekcji zadań związanych z węgierskim matematykiem Paulem Erdősem i dokonał także innych postępów matematycznych. Zespół testował go na zbiorze 353 otwartych problemów. W pracy przedstawiono nie tylko uzyskane wyniki, lecz także sposób ich otrzymania, a wiele dowodów ocenili niezależni matematycy.
Agenci pracujący w pełnej konfiguracji wymieniali się próbami dowodów. Zachowywali obiecujące rozwiązania i odrzucali te, które nie prowadziły do celu. Ich rozumowanie było sprawdzane przez Lean, program służący do weryfikowania formalnych zapisów matematycznych. Dzięki temu system mógł wykrywać kroki, których nie uzasadniono w kodzie. Prostszy wariant, w którym niezależne agenty Gemini korzystały z informacji zwrotnej od Lean, ale nie wymieniały się próbami i nie korzystały z AlphaProof, również rozwiązał wszystkie dziewięć zadań. Na łatwych problemach zużywał mniej zasobów obliczeniowych, a na dwóch najtrudniejszych więcej.
Słownik artykułu
Krótkie objaśnienia terminów występujących w tekście. Każde hasło prowadzi do szerszej definicji i przykładów użycia.
Pytanie matematyczne, którego rozwiązanie nie zostało znalezione albo nie jest szerzej znane społeczności matematyków.
Model sztucznej inteligencji wyspecjalizowany w analizowaniu i tworzeniu tekstu na podstawie zależności poznanych podczas treningu na danych językowych.
Autorzy badania nie ustalili jednak, czy prostszy wariant rozwiązałby którykolwiek z problemów, których nie udało się zamknąć pełnemu systemowi. Sam fakt, że oba warianty poradziły sobie z tym samym zestawem dziewięciu zadań, zaskoczył badaczy. Wynik sugeruje, że coraz sprawniejsze modele językowe mogą pracować nad matematyką badawczą przy użyciu stosunkowo prostych narzędzi kontrolnych. Nie oznacza to jednak, że kontrola programu zastępuje analizę matematyczną.
Lean sprawdza twierdzenie dokładnie w takiej postaci, w jakiej zostało zapisane w kodzie. Problem może pojawić się wcześniej, podczas przełożenia zwykłego zapisu matematycznego na język formalny albo podczas odczytywania wyniku. W preprincie opublikowanym 6 października badacze wskazali rozbieżności między fragmentami tekstowego dowodu równań Naviera i Stokesa przygotowanego przez OpenAI a jego odpowiednikiem w Lean. Nie dowodzi to, że tekstowy dowód jest błędny, ale pokazuje, że poprawny zapis w programie nie potwierdza automatycznie poprawności całej pracy wygenerowanej przez AI.
Z tego powodu istotną częścią publikacji DeepMind była praca matematyków, którzy ocenili wiele uzyskanych dowodów. Swarat Chaudhuri, współautor badania, podkreślał, że człowiek musi naprawdę przeanalizować problem i wyznaczyć cele dla systemu. Nawet gdy AI nie kończy dowodu, sprawdzone kroki mogą pomóc badaczom znaleźć miejsce, w którym pozostała luka. W takim modelu człowiek dostarcza pomysłów i kierunku pracy, a system pomaga przeszukiwać możliwe rozwiązania. Chaudhuri ujął to wprost: „Matematyka jest ostatecznie ludzką sztuką”.
Thomas Bloom z University of Manchester, który nie uczestniczył w badaniu, ocenił, że wyniki AlphaProof Nexus nie należą do najważniejszych osiągnięć matematycznych. To zastrzeżenie nie podważa samego rezultatu, lecz pomaga określić jego znaczenie. Badanie pokazuje możliwości konkretnej konfiguracji AI i opisuje proces weryfikacji, ale nie dowodzi, że systemy tego typu samodzielnie przejęły matematykę badawczą. Zdaniem Blooma podejście DeepMind jest bardziej odpowiedzialne naukowo niż prezentowanie matematyki przede wszystkim jako demonstracji możliwości oprogramowania.
Dyskusja zaostrzyła się po tym, jak OpenAI opublikowało 722 rękopisy matematyczne przygotowane przez niewprowadzony wcześniej model AI. Firmy rozwijające takie systemy często nie ujawniają metod i danych, ponieważ konkurują o przełomowe wyniki. Według materiału OpenAI opublikowane prace i towarzyszące im dowody w Lean zostały w całości wygenerowane przez AI, a społeczność matematyczna musiała sama ocenić, które elementy są użyteczne. OpenAI informowało o współpracy z niezależną grupą doradczą przy tworzeniu zasad udostępniania wyników. Grupa ta miała jednak zalecać, aby nie testować niewprowadzonych modeli na zaawansowanej matematyce. Autor materiału ocenia, że firma postąpiła wbrew tej wskazówce.
Bryna Kra z Northwestern University mówiła, że szybkie i konkurencyjne podejście firm osłabia kulturę dzielenia się pomysłami. Jej zdaniem poprawiło się cytowanie wcześniejszej literatury przez OpenAI, a potencjał AI do rozwiązywania ważnych problemów jest ekscytujący. Jednocześnie wśród matematyków istnieje obawa, że modele mogły uzyskać dostęp do nieopublikowanych prac. Kra mówiła o niszczeniu zdrowej, opartej na współpracy kultury, w której badacze chętnie dzielili się pomysłami. Jeśli autorzy obawiają się, że ich nieukończone wyniki zostaną wykorzystane bez ich wiedzy, współpraca staje się trudniejsza.
Nie wszyscy matematycy postrzegają ten kierunek negatywnie. Andrew Turner, który studiował matematykę i fizykę oraz jest dyrektorem technicznym firmy Plasma AI, uważa, że AI zwiększa dostępność matematyki. Jego zdaniem nie powinno się zakładać, że tylko niewielka grupa matematyków ma decydować, jak rozwiązywać problemy. Turner porównuje pracę z maszynami do inżynierii i uważa, że dzięki nim można zadawać pytania wcześniej uznawane za nieosiągalne. Kilka dni po zamknięciu przez Blooma komentarzy na stronie śledzącej problemy Erdősa Plasma AI ogłosiła uruchomienie nowej witryny, która będzie przyjmować także wyniki uzyskane przez AI.
Badanie AlphaProof Nexus nie rozstrzyga tego sporu. Pokazuje natomiast, że skuteczne wykorzystanie AI w matematyce wymaga połączenia generowania rozwiązań, formalnego sprawdzania i oceny ludzi. Równie ważne pozostają zasady udostępniania wyników oraz ochrona nieopublikowanych pomysłów. Na stronie Blooma końcowe przesłanie brzmi: „Bądź zagubiony, utknij, zainspiruj się. Znajdź nieporządny dowód, a potem lepszy. Zmęcz się, zgłodniej, skup się. Dyskutuj, śmiej się, poddaj się, napij się kawy i spróbuj ponownie. Bądź człowiekiem”. W świetle opisanego badania AI może przyspieszać taką pracę, ale nie zastępuje jej ludzkiego sensu.
Brak komentarzy. Bądź pierwszy!