Sztuczna inteligencja na Międzynarodowej Olimpiadzie Matematycznej: jak AlphaProof i AlphaGeometry 2 osiągnęły srebrny medal

Rozumowanie matematyczne jest istotnym aspektem ludzkich zdolności poznawczych, napędzającym postęp odkryć naukowych i rozwój technologiczny. Ponieważ staramy się rozwijać sztuczną inteligencję ogólną odpowiadającą poznaniu człowieka, wyposażenie sztucznej inteligencji w zaawansowane możliwości rozumowania matematycznego jest niezbędne. Chociaż obecne systemy sztucznej inteligencji radzą sobie z podstawowymi problemami matematycznymi, borykają się ze złożonym rozumowaniem niezbędnym w zaawansowanych dyscyplinach matematycznych, takich jak algebra i geometria. Może się to jednak zmienić, jak zrobiło to Google DeepMind znaczące kroki w rozwijaniu możliwości rozumowania matematycznego systemu sztucznej inteligencji. Ten przełom dokonał się w Międzynarodowa Olimpiada Matematyczna (IMO) 2024. Założony w 1959 r. IMO to najstarszy i najbardziej prestiżowy konkurs matematyczny, w którym uczniowie szkół średnich na całym świecie stawiają czoła problemom z algebry, kombinatoryki, geometrii i teorii liczb. Co roku zespoły młodych matematyków rywalizują ze sobą, rozwiązując sześć bardzo trudnych problemów. W tym roku Google DeepMind wprowadziło dwa systemy AI: AlphaProof, który koncentruje się na formalnym rozumowaniu matematycznym, oraz AlphaGeometry 2, który specjalizuje się w rozwiązywaniu problemów geometrycznych. Te systemy AI rozwiązały cztery z sześciu problemów, osiągając poziom srebrnego medalisty. W tym artykule przyjrzymy się, jak te systemy działają przy rozwiązywaniu problemów matematycznych.

AlphaProof: Łączenie sztucznej inteligencji i języka formalnego na potrzeby dowodzenia twierdzeń matematycznych

AlphaProof to system sztucznej inteligencji przeznaczony do udowadniania twierdzeń matematycznych przy użyciu języka formalnego Lean:. To integruje Gemini, wstępnie wytrenowany model języka, z AlfaZero, algorytm uczenia się przez wzmacnianie, znany z opanowania szachów, shogi i Go.

Model Gemini przekłada twierdzenia problemowe języka naturalnego na formalne, tworząc bibliotekę problemów o różnym stopniu trudności. Służy to dwóm celom: przekształceniu nieprecyzyjnego języka naturalnego w precyzyjny język formalny w celu weryfikacji dowodów matematycznych oraz wykorzystaniu zdolności predykcyjnych Bliźniąt do wygenerowania listy możliwych rozwiązań z precyzją języka formalnego.

Gdy AlphaProof napotka problem, generuje potencjalne rozwiązania i wyszukuje kroki dowodowe w Lean, aby je zweryfikować lub obalić. Zasadniczo jest to podejście neurosymboliczne, w którym sieć neuronowa Gemini tłumaczy instrukcje języka naturalnego na symboliczny język formalny Lean, aby udowodnić lub obalić twierdzenie. Podobnie jak mechanizm samodzielnej gry AlphaZero, w którym system uczy się grając przeciwko sobie, AlphaProof ćwiczy się, próbując udowodnić twierdzenia matematyczne. Każda próba sprawdzenia udoskonala model językowy AlphaProof, a udane dowody wzmacniają zdolność modelu do rozwiązywania trudniejszych problemów.

Na potrzeby Międzynarodowej Olimpiady Matematycznej (IMO) AlphaProof został przeszkolony poprzez udowodnienie lub obalenie milionów problemów obejmujących różne poziomy trudności i tematy matematyczne. Szkolenie to było kontynuowane podczas zawodów, podczas których AlphaProof udoskonalał swoje rozwiązania, aż znalazł kompletną odpowiedź na problemy.

AlphaGeometry 2: Integracja LLM i symbolicznej sztucznej inteligencji w celu rozwiązywania problemów z geometrią

AlphaGeometry 2 to najnowsza wersja AlfaGeometria serii, zaprojektowanej do rozwiązywania problemów geometrycznych ze zwiększoną precyzją i wydajnością. Opierając się na swoim poprzedniku, AlphaGeometry 2 wykorzystuje podejście neurosymboliczne, które łączy neuronowe modele dużego języka (LLM) z symboliczną sztuczną inteligencją. Integracja ta łączy logikę opartą na regułach z predykcyjną zdolnością sieci neuronowych do identyfikowania punktów pomocniczych, niezbędnych do rozwiązywania problemów geometrycznych. LLM w AlphaGeometry przewiduje nowe konstrukcje geometryczne, podczas gdy symboliczna sztuczna inteligencja stosuje logikę formalną do generowania dowodów.

W obliczu problemu geometrycznego, program LLM firmy AlphaGeometry analizuje liczne możliwości, prognozując konstrukcje kluczowe dla rozwiązania problemu. Te przewidywania stanowią cenne wskazówki, kierując silnik symboliczny w stronę trafnych wniosków i zbliżając go do rozwiązania. To innowacyjne podejście pozwala firmie AlphaGeometry rozwiązywać złożone problemy geometryczne, wykraczające poza konwencjonalne scenariusze.

Jednym z kluczowych usprawnień w AlphaGeometry 2 jest integracja Gemini LLM. Model ten jest szkolony od podstaw na znacznie większej liczbie syntetycznych danych niż jego poprzednik. To obszerne szkolenie przygotowuje go do rozwiązywania trudniejszych problemów z geometrią, w tym związanych z ruchami obiektów i równaniami kątów, stosunków lub odległości. Dodatkowo AlphaGeometry 2 zawiera silnik symboliczny, który działa o dwa rzędy wielkości szybciej, umożliwiając eksplorację alternatywnych rozwiązań z niespotykaną dotąd szybkością. Te udoskonalenia sprawiają, że AlphaGeometry 2 jest potężnym narzędziem do rozwiązywania skomplikowanych problemów geometrycznych, ustanawiając nowy standard w tej dziedzinie.

AlphaProof i AlphaGeometry 2 w IMO

W tym roku uczestnicy Międzynarodowej Olimpiady Matematycznej (IMO) byli testowani z sześcioma różnymi problemami: dwoma z algebry, jednym z teorii liczb, jednym z geometrii i dwoma z kombinatoryki. Badacze Google’a przetłumaczony te problemy na formalny język matematyczny dla programów AlphaProof i AlphaGeometry 2. AlphaProof rozwiązał dwa problemy z algebry i jeden problem z teorii liczb, w tym najtrudniejsze zadanie konkursu, rozwiązane w tym roku przez zaledwie pięciu uczestników. Tymczasem w ramach projektu AlphaGeometry 2 pomyślnie rozwiązano problem geometrii, choć nie rozwiązano dwóch problemów kombinatoryki

Każdy problem w IMO jest wart siedem punktów, co daje maksymalnie 42 punkty. AlphaProof i AlphaGeometry 2 zdobyły 28 punktów, osiągając doskonałe wyniki w rozwiązanych problemach. Dało im to miejsce w górnej części kategorii srebrnych medali. Próg złotego medalu w tym roku wynosił 29 punktów i osiągnęło go 58 z 609 zawodników.

Następny skok: język naturalny w wyzwaniach matematycznych

AlphaProof i AlphaGeometry 2 wykazały imponujący postęp w zakresie zdolności sztucznej inteligencji do rozwiązywania problemów matematycznych. Jednak systemy te nadal polegają na ekspertach, którzy tłumaczą problemy matematyczne na język formalny w celu ich przetwarzania. Ponadto nie jest jasne, w jaki sposób te specjalistyczne umiejętności matematyczne mogłyby zostać włączone do innych systemów sztucznej inteligencji, na przykład do analizy hipotez, testowania innowacyjnych rozwiązań długotrwałych problemów i efektywnego zarządzania czasochłonnymi aspektami dowodzenia.

Aby pokonać te ograniczenia, badacze Google opracowują system rozumowania w języku naturalnym w oparciu o Gemini i swoje najnowsze badania. Celem tego nowego systemu jest zwiększenie możliwości rozwiązywania problemów bez konieczności formalnego tłumaczenia na język i zaprojektowano go tak, aby umożliwiał płynną integrację z innymi systemami sztucznej inteligencji.

Bottom Line

Wyniki AlphaProof i AlphaGeometry 2 na Międzynarodowej Olimpiadzie Matematycznej stanowią znaczący krok naprzód w zakresie możliwości sztucznej inteligencji w zakresie rozwiązywania złożonych zagadnień matematycznych. Oba systemy uzyskały srebrny medal, rozwiązując cztery z sześciu trudnych zadań, co stanowi znaczący postęp w zakresie formalnego dowodzenia i rozwiązywania problemów geometrycznych. Pomimo osiągnięć, te systemy sztucznej inteligencji nadal polegają na wnioskach człowieka w zakresie tłumaczenia problemów na język formalny i borykają się z problemami integracji z innymi systemami sztucznej inteligencji. Przyszłe badania mają na celu dalsze udoskonalenie tych systemów, potencjalnie integrując rozumowanie w języku naturalnym, aby rozszerzyć ich możliwości w szerszym zakresie zagadnień matematycznych.