DeepMind osiąga kamień milowy w rozwiązaniu problemów matematycznych - kolejne duże wyzwanie dla sztucznej inteligencji
DeepMind osiąga kamień milowy w rozwiązaniu problemów matematycznych - kolejne duże wyzwanie dla sztucznej inteligencji
,
Teraz twierdzi, że jest na skraju pokonania najlepszych uczniów na świecie podczas rozwiązywania zadań matematycznych.
Londyn Learning maszynowy Firma ogłosiła 25 lipca, że jego systemy sztucznej inteligencji (KI) rozwiązały cztery z sześciu zadań, które zostały przekazane studentom Międzynarodowej Olimpiady Matematycznej (IMO) 2024 w Bath, Wielkiej Brytanii. AI dostarczyło rygorystycznych, stopniowych dowodów, które zostały ocenione przez dwie najlepsze matematyki i osiągnęły wynik 28/42 tylko jeden punkt od obszaru złotych medali.
„To oczywiście bardzo ważny postęp”, mówi Joseph Myers, matematyk z Cambridge w Wielkiej Brytanii, który wraz z medalistą Fields Timem Gowersem sprawdził rozwiązania i pomógł wybrać oryginalne problemy na ten rok.
DeepMind i inne firmy są w wyścigu, aby ostatecznie przedstawić dowody maszyn, niezbędne Rozwiąż pytania badawcze w matematyce . Problemy z IMO, wiodącą światową konkurencją dla młodych matematyków, stały się podwórkiem postępu w kierunku tego celu i są postrzegane jako „duże wyzwanie” dla uczenia maszynowego, według firmy.
„Po raz pierwszy system AI był w stanie osiągnąć usługi na poziomie medalu”, powiedział Pushmeet Kohli, wiceprezes AI in Science w Deepmind, w konsultacji prasowej. „To ważny kamień milowy na drodze do budowania postępowych dowodów” - powiedział Kohli.
rozszerzenie
Zaledwie kilka miesięcy temu, w styczniu, system DeepMind Usługi alfageometrii na poziomie medali Podczas rozwiązywania rodzaju problemów IMO, nazwa tych w geometrii euclidean. Pierwsza sztuczna inteligencja, która działa na poziomie złotego medalu dla ogólnych pytań dotyczących testu w algebrze, kombinatoricach i teorii liczb, które są ogólnie uważane za bardziej wymagające niż geometria-jest uprawniona do uzyskania ceny 5 milionów dolarów, nagrody Olimpiady AI Math (AIMO). (Cena ma ścisłe kryteria, takie jak ujawnienie kodu źródłowego i pracy o ograniczonej sile obliczeniowej, co oznacza, że obecne wysiłki DeepMind nie kwalifikowałyby się.)
W swojej najnowszej próbie naukowcy wykorzystali alfageometrię2 do rozwiązania problemu geometrii w mniej niż 20 sekund; AI jest ulepszoną i szybszą wersją systemu rekordu, mówi specjalista z komputera DeepMind, Thang Luong.
W przypadku innych rodzajów pytań zespół opracował zupełnie nowy system o nazwie Alphaproof. Alphaproof rozwiązał dwa problemy z algebry w konkursie i jeden w teorii liczb, dla których zajęło to trzy dni. (Uczestnicy faktycznej IMO mają dwie sesje po 4,5 godziny.) Nie było w stanie rozwiązać dwóch problemów w kombinacji, innego obszaru matematyki.
Tylko w zeszłym tygodniu zespół firm oprogramowania Numina i Huggingface wykorzystał model głosowy, aby wygrać pośrednią „cenę postępu” Amio w oparciu o uproszczone wersje problemów IMO. Firmy stworzyły całe systemy open source i udostępniły je do pobierania innych badaczy. Ale zwycięzcy powiedzieli, że natura że same modele językowe prawdopodobnie nie byłyby wystarczające, aby rozwiązać trudne problemy.
Tylko klasa
Alphaproof łączy model głosowy z technologią uczenia się wzmacniającego, który silnik „Alphazero” dla gier atakujących, takich jak GO, a także niektóre Specyficzne problemy matematyczne . Wraz ze wzrostem nauki sieć neuronowa uczy się poprzez eksperymenty i błędy. Działa to dobrze, jeśli jego odpowiedzi można ocenić za pomocą obiektywnej skali. W tym celu Alphaproof został przeszkolony do czytania i pisania dowodów w formalnym języku o nazwie Lean, który jest używany w pakiecie oprogramowania „Proof Assistant” o tej samej nazwie popularnej wśród matematyków. W tym celu Alphaproof sprawdził, czy jego wydatki były prawidłowe, wykonując je w pakiecie Lean, co pomogło wypełnić niektóre kroki w kodzie.
Szkolenie modelu głosowego wymaga ogromnych ilości danych, ale w Lean dostępnych było tylko kilka dowodów matematycznych. Aby przezwyciężyć ten problem, zespół opracował dodatkową sieć, która próbowała przetłumaczyć istniejące nagranie o milion problemów napisanych w języku naturalnym, ale bez tłumaczenia rozwiązań napisanych w Lean, mówi Thomas Hubert, badacz studiów głębinowych, który przeprowadził rozwój Alphaproofa. „Możemy nauczyć się udowodnić nasze podejście, nawet jeśli pierwotnie nie przeszkoliliśmy dowodów z napisem ludzkim?” (Firma była podobna do Go, gdzie jego sztuczna inteligencja nauczyła się grać w grę, grając przeciwko sobie, zamiast tak, jak ludzie.)
Magical Key
Wiele lean tłumaczeń nie miało sensu, ale wystarczająco było wystarczająco dobre, aby doprowadzić alfaproof do tego stopnia, że mógłby rozpocząć rosnące cykle uczenia się. Wyniki były znacznie lepsze niż oczekiwano, powiedział Gowers podczas konsultacji prasowej. „Wiele problemów z IMO ma tę własność magicznego klucza. Problem najpierw wygląda trudny, dopóki nie znajdziesz magicznego klucza, który go otwiera” - powiedział Gowers, który pracuje w Collège de France w Paryżu.
W niektórych przypadkach Alphaproof wydawał się być w stanie podjąć ten dodatkowy etap kreatywności, nadając mu prawidłowy krok od nieskończenie duże rozwiązanie. Dodała jednak dalsza analiza w celu ustalenia, czy odpowiedzi były mniej zaskakujące niż wyglądały, dodał Gowers. Podobny dyskurs powstał po zaskakującym 'zug 37' , deepMinds Alphago-bot w jego Słynne zwycięstwo w 2016 roku o najlepszym na świecie graczu ludzkim Go -punkt zwrotny dla KI.
Okaże się, czy techniki można udoskonalić do pracy na poziomie badań matematyki, powiedział Myers z recenzji prasowej. „Czy może rozszerzyć się na inne rodzaje matematyki, w których nie można trenować milionów problemów?”
„Dotarliśmy do punktu, w którym możesz nie tylko udowodnić otwarte problemy badawcze, ale także problemy, które są bardzo trudne dla najlepszych młodych matematyków na świecie”-powiedział David Silver, specjalista komputerowy Deepmind, który był wiodącym badaczem w rozwoju Alphago w połowie 2010 roku.