Matematyka.pl

nie wiem czy jest to nadal miejsce spotkan olimpijczykow,

gdzie jak twierdzi, wytrenowany model zwany AlphaGeometry, dowodzi zadanka z planimetrii na poziomie zlotego medalisty IMO

SekretnyJulek pisze: 15 mar 2024, o 13:27 Z tego co rozumiem jest to de facto klasyczny algorytm brute force (przez angle chasing i podobne metody), któremu AI trochę podpowiada. Jest to na pewno ciekawe osiągnięcie, ale mam wrażenie, że nie tak imponujące jak podają media. Poczekajmy na AI do kombinatoryki i teorii liczb...

https://deepmind-google.translate.goog/discover/blog/ai-solves-imo-problems-at-silver-medal-level/?_x_tr_sl=en&_x_tr_tl=pl&_x_tr_hl=pl&_x_tr_pto=sc

AlphaProof: formalne podejście do rozumowania
AlphaProof to system, który szkoli się w zakresie udowadniania twierdzeń matematycznych w języku formalnym Lean . Łączy wstępnie wytrenowany model języka z algorytmem uczenia się przez wzmacnianie AlphaZero , który wcześniej sam nauczył się opanować partie szachów, shogi i go.

Języki formalne mają tę krytyczną zaletę, że dowody wykorzystujące rozumowanie matematyczne można formalnie zweryfikować pod kątem poprawności. Ich zastosowanie w uczeniu maszynowym było jednak wcześniej ograniczone ze względu na bardzo ograniczoną ilość dostępnych danych pisanych przez ludzi.

W przeciwieństwie do tego, podejścia oparte na języku naturalnym mogą powodować halucynacje wiarygodnych, ale niepoprawnych pośrednich etapów rozumowania i rozwiązań, pomimo dostępu do o rząd wielkości większej ilości danych. Stworzyliśmy pomost pomiędzy tymi dwiema uzupełniającymi się sferami, dostrajając model Gemini , aby automatycznie tłumaczył stwierdzenia problemowe w języku naturalnym na stwierdzenia formalne, tworząc dużą bibliotekę problemów formalnych o różnym stopniu trudności.

Kiedy pojawia się problem, AlphaProof generuje propozycje rozwiązań, a następnie potwierdza je lub obala, przeszukując możliwe kroki sprawdzające w Lean. Każdy znaleziony i zweryfikowany dowód służy wzmocnieniu modelu językowego AlphaProof, zwiększając jego zdolność do rozwiązywania kolejnych, trudniejszych problemów.

Szkoliliśmy AlphaProof dla IMO, udowadniając lub obalając miliony problemów, obejmujących szeroki zakres trudności i obszarów zagadnień matematycznych w ciągu tygodni poprzedzających zawody. Podczas konkursu zastosowano także pętlę szkoleniową, wzmacniając dowody na samodzielnie wygenerowane odmiany problemów konkursowych, aż do znalezienia pełnego rozwiązania.