Laboratorium Google ujawniło szczegóły AlphaProof

|||Z ostatniej chwili

W przyrodzie kolor wściekle żółty bywa stosowany ku przestrodze (patrz: liściołaz żółty) czy jako kamuflaż (patrz: modliszka storczykowa). W Pulsarze natomiast – to sygnał końca embarga, które prestiżowe czasopisma naukowe nakładają na publikowane przez badaczy artykuły. Tekst z żółtym oznaczeniem dotyczy więc doniesienia, które zostało upublicznione dosłownie przed chwilą.

W lipcu 2024 r. świat obiegła sensacyjna wiadomość: AlphaProof, jako pierwszy system AI, osiągnął poziom srebrnego medalisty Międzynarodowej Olimpiady Matematycznej (IMO). Jest to najstarszy (1959 r.), największy i najbardziej prestiżowy tego rodzaju konkurs. Wprawdzie system nie poradził sobie z dwoma problemami z kombinatoryki, ale m.in. rozwiązał najtrudniejsze zadanie w konkursie.

Najnowsze „Nature” publikuje artykuł naukowców z DeepMind, dokładnie opisujący działanie AlphaProof. Badacze precyzują, że za historyczny wynik AI odpowiadał połączony system algorytmów. Zadania geometryczne rozwiązywał AlphaGeometry 2, natomiast AlphaProof był głównym „silnikiem rozumowania” dla pozostałych problemów. Kluczowa innowacja polegała zaś na odejściu od nieformalnych dowodów zapisanych w języku naturalnym, generowanym przez duże modele językowe (takie jak ChatGPT). AlphaProof tworzy dowody w rygorystyczny, formalny sposób, przeznaczony dla „asystenta” o nazwie Lean (to język programowania służący głównie do sprawdzania, czy skomplikowane dowody matematyczne lub programy komputerowe są poprawne).

Dowodzenie twierdzenia przypomina grę — podobnie jak w innym słynnym modelu AlphaZero, który opanował Go i szachy. System rozpoczyna od otrzymania twierdzenia matematycznego i próbuje dojść do stanu, w którym nie pozostaje już nic do udowodnienia, a asystent Lean sprawdza każdy krok, gwarantując poprawność ostatecznego dowodu.

To jednak nie wystarczało, by rozwiązywać najtrudniejsze zadania. Dlatego DeepMind opracowało nowatorską metodę uczenia przez wzmacnianie – „Test-Time RL” (TTRL). Gdy AlphaProof staje przed wyjątkowo skomplikowanym problemem (takim jak z IMO), zamiast korzystać z ogólnej bazy wiedzy, sam generuje nowy, „szyty na miarę” program uczenia, składający się z wielu wariantów konkretnego problemu (np. jego uproszczeń lub uogólnień), a następnie intensywnie trenuje tylko na nich.

Ograniczenia AlphaProof są jednak równie spektakularne co jego sukcesy. System wymaga 2–3 dni intensywnych obliczeń na rozwiązanie pojedynczego problemu olimpijskiego. Słabo radzi sobie z problemami wymagającymi niestandardowych definicji matematycznych. Wymaga też zasobów dostępnych tylko największym laboratoriom badawczym, gdyż sam trening głównego modelu pochłonął ok. 80 tysięcy TPU-dni (odpowiednik pracy 4 tys. procesorów przez 20 dni).

Dziękujemy, że jesteś z nami. To jest pierwsza wzmianka na ten temat. Pulsar dostarcza najciekawsze informacje naukowe i przybliża najnowsze badania naukowe. Jeśli korzystasz z publikowanych przez Pulsar materiałów, prosimy o powołanie się na nasz portal. Źródło: www.projektpulsar.pl.