AI na Międzynarodowej Olimpiadzie Matematycznej: Jak AlphaProof i AlphaGeometry 2 osiągnęły poziom srebrnego medalu

Rozumowanie matematyczne jest istotnym aspektem ludzkich zdolności poznawczych, napędzając postęp w odkryciach naukowych i rozwoju technologicznym. Podczas gdy obecne systemy AI mogą radzić sobie z podstawowymi problemami matematycznymi, mają trudności z złożonymi rozumowaniami potrzebnymi do zaawansowanych dyscyplin matematycznych, takich jak algebra i geometria. Jednakże, sytuacja ta może ulegać zmianie, ponieważ Google DeepMind dokonał znaczących postępów w rozwoju systemu AI o zaawansowanych zdolnościach rozumowania matematycznego. Przełom ten nastąpił na Międzynarodowej Olimpiadzie Matematycznej (IMO) 2024. Ustanowiona w 1959 roku, IMO jest najstarszą i najbardziej prestiżową konkurencją matematyczną, wyzywającą uczniów szkół średnich na całym świecie do rozwiązywania problemów z algebry, kombinatoryki, geometrii i teorii liczb. Każdego roku zespoły młodych matematyków rywalizują, aby rozwiązać sześć bardzo trudnych problemów. W tym roku, Google DeepMind wprowadził 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 medalu. W tym artykule, będziemy badać, jak te systemy działają, aby rozwiązać problemy matematyczne.

AlphaProof: łącząc AI i język formalny dla dowodzenia twierdzeń matematycznych

AlphaProof to system AI zaprojektowany do dowodzenia twierdzeń matematycznych przy użyciu języka formalnego Lean. Integruje Gemini, wstępnie wytrenowany model językowy, z AlphaZero, algorytmem uczenia wzmocnionego, który jest znany z opanowania szachów, shogi i Go.

Model Gemini tłumaczy naturalne wypowiedzi problemów na formalne, tworząc bibliotekę problemów o różnym poziomie trudności. To służy dwóm celom: przekształceniu nieprecyzyjnego języka naturalnego w precyzyjny język formalny do weryfikacji dowodów matematycznych oraz wykorzystaniu predykcyjnych zdolności Gemini do generowania listy możliwych rozwiązań z precyzyjnym językiem formalnym.

Gdy AlphaProof napotyka problem, generuje potencjalne rozwiązania i wyszukuje kroki dowodowe w Lean, aby zweryfikować lub obalić je. To jest podstawowo neuro-symboliczne podejście, gdzie sieć neuronowa, Gemini, tłumaczy instrukcje języka naturalnego na język formalny symboliczny Lean, aby dowieść lub obalić twierdzenie. Podobnie jak mechanizm samogry AlphaZero, gdzie system uczy się, grając w gry przeciwko sobie, AlphaProof szkoli się, próbując dowieść twierdzeń matematycznych. Każda próba dowodu udoskonala model językowy AlphaProof, z udanymi dowodami wzmacniającymi zdolność modelu do radzenia sobie z bardziej skomplikowanymi problemami.

Dla Międzynarodowej Olimpiady Matematycznej (IMO), AlphaProof został wytrenowany, dowodząc lub obalając miliony problemów, pokrywających różne poziomy trudności i tematy matematyczne. To szkolenie trwało podczas konkursu, gdzie AlphaProof udoskonalił swoje rozwiązania, aż do znalezienia kompletnych odpowiedzi na problemy.

AlphaGeometry 2: integrując LLM i AI symboliczny do rozwiązywania problemów geometrycznych

AlphaGeometry 2 to najnowsza iteracja serii AlphaGeometry, zaprojektowana do rozwiązywania problemów geometrycznych z zwiększoną precyzją i wydajnością. Budując na fundamencie swojego poprzednika, AlphaGeometry 2 wykorzystuje podejście neuro-symboliczne, które łączy duże modele językowe (LLM) z AI symbolicznym. To połączenie łączy logikę opartą na regułach z predykcyjnymi zdolnościami sieci neuronowych, aby zidentyfikować punkty pomocnicze, niezbędne do rozwiązywania problemów geometrycznych. LLM w AlphaGeometry przewiduje nowe konstrukcje geometryczne, podczas gdy AI symboliczny stosuje logikę formalną, aby wygenerować dowody.

Gdy AlphaGeometry napotyka problem geometryczny, LLM ocenia wiele możliwości, przewidując konstrukcje niezbędne do rozwiązania problemu. Te przewidywania służą jako cenne wskazówki, kierując silnik symboliczny w stronę dokładnych wnioskowań i zbliżając się do rozwiązania. To innowacyjne podejście umożliwia AlphaGeometry rozwiązywać złożone wyzwania geometryczne, które wykraczają poza konwencjonalne scenariusze.

Jednym z kluczowych usprawnień w AlphaGeometry 2 jest integracja modelu LLM Gemini. Ten model został wytrenowany od podstaw na znacznie większych danych syntetycznych niż jego poprzednik. To obszerne szkolenie pozwala mu radzić sobie z trudniejszymi problemami geometrycznymi, w tym tymi, które obejmują ruchy obiektów i równania kątów, stosunków lub odległości. Dodatkowo, AlphaGeometry 2 posiada silnik symboliczny, który działa dwa rzędy wielkości szybciej, umożliwiając mu eksplorować alternatywne rozwiązania z bezprecedensową szybkością. Te postępy czynią AlphaGeometry 2 potężnym narzędziem do rozwiązywania skomplikowanych problemów geometrycznych, ustanawiając nowy standard w tej dziedzinie.

AlphaProof i AlphaGeometry 2 na IMO

W tym roku na Międzynarodowej Olimpiadzie Matematycznej (IMO), uczestnicy zostali poddani sześciu różnorodnym problemom: dwóm z algebry, jednej z teorii liczb, jednej z geometrii i dwóm z kombinatoryki. Naukowcy z Google przetłumaczyli te problemy na język matematyczny formalny dla AlphaProof i AlphaGeometry 2. AlphaProof rozwiązał dwa problemy algebryczne i jeden problem z teorii liczb, w tym najtrudniejszy problem konkursu, rozwiązany tylko przez pięciu uczestników w tym roku. Tymczasem, AlphaGeometry 2 pomyślnie rozwiązał problem geometryczny, choć nie rozwiązał dwóch wyzwań kombinatorycznych.

Każdy problem na IMO jest wart siedem punktów, co daje maksymalnie 42 punkty. AlphaProof i AlphaGeometry 2 zdobyli 28 punktów, osiągając idealne wyniki w problemach, które rozwiązały. To umieściło ich na wysokim poziomie kategorii srebrnego medalu. Progiem złotego medalu w tym roku było 29 punktów, osiągnięte przez 58 z 609 uczestników.

Następny skok: język naturalny dla wyzwań matematycznych

AlphaProof i AlphaGeometry 2 pokazały imponujące postępy w zdolnościach systemów AI do rozwiązywania problemów matematycznych. Jednakże, te systemy nadal polegają na ekspertach, aby przetłumaczyć problemy matematyczne na język formalny do przetwarzania. Dodatkowo, nie jest jasne, jak te specjalistyczne umiejętności matematyczne mogą być włączone do innych systemów AI, takich jak eksploracja hipotez, testowanie innowacyjnych rozwiązań długotrwałych problemów i efektywne zarządzanie czasochłonnymi aspektami dowodów.

Aby pokonać te ograniczenia, naukowcy z Google rozwijają system rozumnienia języka naturalnego oparty na Gemini i ich najnowszych badaniach. Ten nowy system ma na celu udoskonalenie zdolności rozwiązywania problemów bez wymogu tłumaczenia języka formalnego i jest zaprojektowany, aby zintegrować się płynnie z innymi systemami AI.

Podsumowanie

Wynik AlphaProof i AlphaGeometry 2 na Międzynarodowej Olimpiadzie Matematycznej jest znaczącym skokiem w zdolnościach AI do rozwiązywania złożonych problemów matematycznych. Obie systemy wykazały wyniki na poziomie srebrnego medalu, rozwiązując cztery z sześciu wyzwań, demonstrując znaczące postępy w dowodzeniu twierdzeń formalnych i rozwiązywaniu problemów geometrycznych. Pomimo ich osiągnięć, te systemy AI nadal zależą od danych wejściowych od ludzi do tłumaczenia problemów na język formalny i stają w obliczu wyzwań integracji z innymi systemami AI. Przyszłe badania mają na celu dalsze udoskonalenie tych systemów, potencjalnie integrując rozumnienie języka naturalnego, aby rozszerzyć ich zdolności na szerszy zakres wyzwań matematycznych.