Bardzo dlugo tutaj na forum nie zagladalem, nie wiem czy jest to nadal miejsce spotkan olimpijczykow, ale chcialem naswietlic jeden z tematow ktory moze olimpiade dotykac.
gdzie jak twierdzi, wytrenowany model zwany AlphaGeometry, dowodzi zadanka z planimetrii na poziomie zlotego medalisty IMO. Robi to wraz z pelnymi dowodami. Jest to co najmniej imponujace, rzucam bo byc moze w jakims okresie czasu moze to np zawazyc jak wyglada I etap olmpiady oraz jako ciekawoste do ewentualnej dyskusji. Papier polecam przeczytac
Ostatnio zmieniony 11 mar 2024, o 12:40 przez Jan Kraszewski, łącznie zmieniany 2 razy.
Powód:Poprawa wiadomości.
Ostatnio zmieniony 12 mar 2024, o 06:25 przez admin, łącznie zmieniany 1 raz.
Powód:Usunięto aktywny link do strony zewnętrznej! sunięto cytowany tekst. Nie cytujemy całej treści postu, jeśli odpowiadamy bezpośrednio pod tym postem!
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...
Update https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html
Ai rozwiazalo 4 problemy robiac wynik 28 punktow na 42 z IMO 2024 (2 z algebry, 1 z teorii liczb i to co wyzej wrzucalem ze potrafi jeden problem z geometrii). Wiecej mozna w blogu poczytac
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...
Zgadza sie, pytanie jest co to znaczy rozwiazywac zadanie i jak to robi czlowiek, bo moze na samym koncu to sie sprowadza do tego samego, jesli rozumiesz o czym mowie.
Ostatnio zmieniony 28 lip 2024, o 13:39 przez admin, łącznie zmieniany 1 raz.
Powód:Usunięto aktywny link do strony zewnętrznej!
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.
Ostatnio zmieniony 28 lip 2024, o 13:38 przez admin, łącznie zmieniany 1 raz.
Powód:Usunięto aktywny link do strony zewnętrznej!
Aktualizacja, niepublikowany model robi 5 zadań na 6 na tegorocznej olimpiadzie w Sunshine Coast w Australii, co daję mu złoty medal. Model nie jest dostępny publicznie i pewnie tak jeszcze zostanie przez długi czas. Testowany model był modelem językowym i ogólnym, nie tylko trenowanym pod te olimpiady.
Troszke z innej polki. Dwa modele z czolowych firm ai robia pierwsze i drugie miejsce na tegorocznej ICPC. Model openai rozwiazal wszystkie 12 zadan, z takimi samymi zasadami jak uczestnicy ludzie.
