Suche
Mein Konto
Po tym, jak Google DeepMind pokonał ludzi we wszystkim, od Zagraj Przejdź do strategicznych gier planszowych,
obecnie twierdzi, że jest o krok od pokonania najlepszych uczniów na świecie w rozwiązywaniu problemów matematycznych.
Z siedzibą w Londynie Uczenie maszynowe 25 lipca firma ogłosiła, że jej systemy sztucznej inteligencji (AI) rozwiązały cztery z sześciu problemów postawionych uczniom podczas Międzynarodowej Olimpiady Matematycznej (IMO) 2024 w Bath w Wielkiej Brytanii. Sztuczna inteligencja zapewniła rygorystyczne dowody krok po kroku oceniane przez dwóch czołowych matematyków i uzyskała wynik 28/42 – zaledwie jeden punkt do złotego medalu.
„To oczywiście bardzo znaczący postęp” – mówi Joseph Myers, matematyk z Cambridge w Wielkiej Brytanii, który wraz z medalistą Fields Timem Gowersem dokonał przeglądu rozwiązań i pomógł wybrać oryginalne problemy na tegoroczną IMO.
DeepMind i inne firmy ścigają się, aby ostatecznie dostarczyć maszynom istotne dowody Rozwiązuj problemy badawcze z matematyki. Firma stwierdziła, że problemy prezentowane na IMO, wiodącym na świecie konkursie dla młodych matematyków, stały się punktem odniesienia dla postępu w realizacji tego celu i są uważane za „wielkie wyzwanie” dla uczenia maszynowego.
„To pierwszy raz, kiedy system sztucznej inteligencji osiągnął medalowy poziom wydajności” – powiedział na konferencji prasowej Pushmeet Kohli, wiceprezes ds. sztucznej inteligencji w nauce w DeepMind. „To ważny kamień milowy w tworzeniu zaawansowanych narzędzi dochodzeniowych” – powiedział Kohli.
Rozszerzenie
Zaledwie kilka miesięcy temu, w styczniu, pojawił się system DeepMind Osiągnięcia na poziomie medalowym AlphaGeometry osiągnąć w rozwiązywaniu jednego rodzaju problemów IMO, a mianowicie problemów z geometrią euklidesową. Pierwsza sztuczna inteligencja, która uzyska złoty medal w teście ogólnym, obejmującym pytania z algebry, kombinatoryki i teorii liczb, ogólnie uważane za trudniejsze niż geometria, będzie kwalifikować się do otrzymania nagrody o wartości 5 milionów dolarów – nagrody AIMO Olimpiady Matematycznej (AIMO). (Nagroda opiera się na rygorystycznych kryteriach, takich jak ujawnienie kodu źródłowego i praca z ograniczoną mocą obliczeniową, co oznacza, że obecne wysiłki DeepMind nie będą się kwalifikować.)
W swojej ostatniej próbie badacze wykorzystali AlphaGeometry2 do rozwiązania problemu geometrii w czasie krótszym niż 20 sekund; sztuczna inteligencja jest ulepszoną i szybszą wersją ich systemu nagrywania, mówi Thang Luong, specjalista komputerowy DeepMind.
W przypadku pozostałych typów pytań zespół opracował zupełnie nowy system o nazwie AlphaProof. AlphaProof rozwiązał dwa problemy z algebry w konkursie i jedno z teorii liczb, co zajęło trzy dni. (Uczestnicy rzeczywistego IMO mają dwie sesje po 4,5 godziny każda.) Nie udało się rozwiązać tych dwóch problemów w kombinatoryce, innej dziedzinie matematyki.
Badacze uzyskali mieszane wyniki, odpowiadając na pytania matematyczne przy użyciu modeli językowych — tego rodzaju systemów, które obsługują chatboty takie jak ChatGPT. Czasami modele dają właściwą odpowiedź, ale nie potrafią racjonalnie wyjaśnić swojego rozumowania, a czasami wygadują bzdury.
Nie dalej jak w zeszłym tygodniu zespół badaczy z firm zajmujących się oprogramowaniem Numina i HuggingFace wykorzystał model językowy, aby zdobyć pośrednią „nagrodę za postęp” AMIO opartą na uproszczonych wersjach problemów IMO. Firmy udostępniły całe swoje systemy jako open source i udostępniły je innym badaczom do pobrania. Ale zwycięzcy powiedzieliNatura, że same modele językowe prawdopodobnie nie wystarczą do rozwiązania trudniejszych problemów.
Tylko klasa
AlphaProof łączy model językowy z technologią uczenia się przez wzmacnianie, która wykorzystuje silnik „AlphaZero”, który firma z powodzeniem wykorzystała w grach atakujących, takich jak Go i niektórych specyficzne problemy matematyczne używany. W uczeniu się przez wzmacnianie sieć neuronowa uczy się metodą prób i błędów. Działa to dobrze, gdy jego odpowiedzi można ocenić za pomocą obiektywnego standardu. W tym celu AlphaProof został przeszkolony w zakresie czytania i pisania dowodów w formalnym języku zwanym Lean, który jest używany w popularnym wśród matematyków pakiecie oprogramowania „Proof Assistant” o tej samej nazwie. W tym celu AlphaProof przetestował poprawność wyników, uruchamiając je w pakiecie Lean, co pomogło wypełnić niektóre kroki w kodzie.
Uczenie modelu językowego wymaga ogromnych ilości danych, a mimo to w Lean dostępnych było niewiele dowodów matematycznych. Aby przezwyciężyć ten problem, zespół opracował dodatkową sieć, która próbowała przetłumaczyć istniejący zapis miliona problemów napisanych w języku naturalnym, ale bez rozwiązań napisanych przez ludzi, na Lean, mówi Thomas Hubert, badacz uczenia maszynowego DeepMind, który współkierował rozwojem AlphaProof. „Nasze podejście było następujące: czy możemy nauczyć się udowadniać, nawet jeśli początkowo nie ćwiczyliśmy na dowodach pisanych przez ludzi?” (Firma przyjęła podobne podejście do Go, gdzie sztuczna inteligencja nauczyła się grać, grając przeciwko sobie, a nie na podstawie sposobu, w jaki robią to ludzie).
Magiczne klucze
Wiele tłumaczeń Lean nie miało sensu, ale były wystarczająco dobre, aby doprowadzić AlphaProof do punktu, w którym mógł rozpocząć cykle uczenia się przez wzmacnianie. Gowers powiedział na konferencji prasowej, że wyniki były znacznie lepsze niż oczekiwano. „Wiele problemów w IMO ma tę właściwość magicznego klucza. Na początku problem wydaje się trudny, dopóki nie znajdziesz magicznego klucza, który go otworzy” – powiedział Gowers, który pracuje w Collège de France w Paryżu.
W niektórych przypadkach wydawało się, że AlphaProof jest w stanie zapewnić dodatkowy krok kreatywności, zapewniając jeden poprawny krok z nieskończenie dużego możliwego rozwiązania. Jednak konieczna jest dalsza analiza, aby ustalić, czy odpowiedzi były mniej zaskakujące, niż się wydawało, dodał Gowers. Podobny dyskurs pojawił się po zaskakującym „Pociąg 37”, bot DeepMinds AlphaGo u niego słynne zwycięstwo w 2016 roku nad najlepszym na świecie człowiekiem w Go wykonane – punkt zwrotny dla sztucznej inteligencji.
Czas pokaże, czy techniki można udoskonalić do pracy na poziomie badawczym w matematyce, Myers powiedział na konferencji prasowej. „Czy można go rozszerzyć na inne rodzaje matematyki, które mogą nie obejmować milionów problemów?”
„Jesteśmy w punkcie, w którym mogą udowodnić nie tylko otwarte problemy badawcze, ale także problemy, które stanowią duże wyzwanie dla najlepszych młodych matematyków na świecie” – powiedział David Silver, specjalista komputerowy DeepMind, który był głównym badaczem rozwijającym AlphaGo w połowie 2010 roku.