Model, który znalazł nowy wynik w matematyce
Model nie podaje odpowiedzi, tylko pisze programy. Program da się uruchomić i sprawdzić, więc zmyślanie przestaje szkodzić.
Plansza z osiemnastowiecznej encyklopedii ma po lewej figury geometryczne, a po prawej przyrządy pomiarowe. Dowód i sprawdzian na jednym arkuszu.
Metoda, o której tu piszemy, opiera się dokładnie na tym połączeniu.
Problem, który trzeba było obejść
Modele językowe generują tekst prawdopodobny, nie prawdziwy. Przy zadaniach matematycznych objawia się to szczególnie boleśnie: model potrafi napisać rozumowanie, które wygląda poprawnie i zawiera fałszywy krok w środku. Piszemy o mechanizmie osobno przy zmyśleniach.
Dla matematyki to jest dyskwalifikujące. Wynik prawie poprawny nie ma wartości.
Autorzy pracy z 2023 roku nie próbowali tego naprawić. Zmienili zadanie tak, żeby zmyślanie przestało mieć znaczenie.
Na czym polega metoda
Cztery kroki, w pętli:
Model pisze program, a nie odpowiedź. Program jest procedurą wytwarzającą rozwiązanie - na przykład konstruującą pewien zbiór.
Sprawdzian uruchamia program i ocenia wynik według jednoznacznej miary. Nie ma tu miejsca na interpretację: albo konstrukcja jest większa od poprzedniej, albo nie.
Najlepsze programy wracają do modelu jako przykłady, na podstawie których pisze kolejne warianty.
Pętla się kręci, a pula rozwiązań stopniowo się poprawia.
To jest procedura ewolucyjna, w której model językowy pełni rolę generatora sensownych mutacji, a nie źródła prawdy. Sprawdzian pełni rolę doboru.
Co znaleziono
Metodę zastosowano do problemu z kombinatoryki ekstremalnej - pytania o największy zbiór punktów spełniający pewien warunek. Jest to problem badany od dziesięcioleci, a postęp w nim mierzy się w konstrukcjach lepszych od najlepszej dotąd znanej.
Wynik: znaleziono nowe konstrukcje przekraczające dotychczasowe najlepsze, zarówno w wymiarze skończonym, jak i w wersji asymptotycznej.
To jest ważne, bo nie da się tego zbyć jako powtórzenia czegoś z danych uczących. Konstrukcja jest nowa i sprawdzalna - każdy może uruchomić program i policzyć.
Tę samą metodę zastosowano potem do klasycznego problemu algorytmicznego z pakowaniem, uzyskując lepsze heurystyki niż stosowane wcześniej.
Co wiemy
- Model językowy sprzężony z automatycznym sprawdzianem znalazł konstrukcje lepsze od dotąd znanych.
- Wyniki są weryfikowalne przez uruchomienie wygenerowanego programu.
- Metoda wymaga problemu, w którym poprawność i jakość rozwiązania da się ocenić maszynowo.
Czego nie wiemy
- Jak szeroka jest klasa problemów, do których to się stosuje. Warunek automatycznej oceny jest mocny.
- Ile wnosi sam model, a ile procedura przeszukiwania. To jest przedmiot sporu.
- Czy da się w ten sposób dowodzić twierdzeń, a nie tylko szukać konstrukcji. To są dwa różne zadania.
Dlaczego to jest inny rodzaj wyniku
Warto zestawić to z tym, co zwykle trafia do nagłówków.
„Model zdał olimpiadę matematyczną”. Zadania olimpijskie mają znane rozwiązania. Wynik mówi o zdolności odtworzenia znanego typu rozumowania - i zawsze towarzyszy mu pytanie o obecność podobnych zadań w danych uczących. Piszemy o tej pułapce przy testach, które się zużywają.
„Model znalazł konstrukcję lepszą od znanych”. Tu odpowiedzi nie było. Wynik jest nowy i sprawdzalny.
To jest ta sama różnica, która zdecydowała o randze AlphaFold: istniał twardy sprawdzian, którego nie da się przejść zgadywaniem.
Czego to nie oznacza
Nie oznacza, że model rozumie matematykę. W tej metodzie model produkuje warianty programów. Ocena należy do sprawdzianu, a nie do niego.
Nie oznacza automatyzacji matematyki. Warunek jest ostry: potrzebny jest problem, w którym jakość rozwiązania da się policzyć maszynowo. Większość matematyki tego nie spełnia.
Nie oznacza, że problem zmyśleń zniknął. Został obejściem odsunięty na bok. W zadaniach bez sprawdzianu wraca w całości.
Co z tego wynika
Praktycznie: to jest przepis, który działa i daje się powtarzać wszędzie tam, gdzie da się napisać funkcję oceniającą. Sporo problemów inżynierskich tak wygląda.
Dla oceny postępu: ta praca pokazuje, że użyteczność modeli nie zależy tylko od ich własnej niezawodności. Zależy od układu, w który się je wstawi. Model niepewny plus twardy sprawdzian daje wynik pewny - i to jest ważniejsza obserwacja niż jakikolwiek wynik na testach.
Dla tej dziedziny: to jest najbliższe temu, co przy superinteligencji opisuje się jako maszyna wychodząca poza wiedzę ludzką. W wersji rzeczywistej wygląda to tak: pętla, sprawdzian i jeden lepszy przykład w wąskim problemie kombinatorycznym.
Część większego wątku
- AGI i superinteligencjaOd maszyny Gooda po dzisiejsze modele: co zostało wykazane, co jest hipotezą, a co deklaracją firmy zbierającej kapitał.
Źródła (4)
- Bernardino Romera-Paredes i in., Mathematical discoveries from program search with large language models, Nature, t. 625 (2023)
Publikacja zespołu Google DeepMind w piśmie recenzowanym. Wyniki dotyczą wąskiej klasy problemów, w których poprawność da się sprawdzić automatycznie.
- Ziwei Ji i in., Survey of Hallucination in Natural Language Generation, ACM Computing Surveys, t. 55 (2023)
Przywołane dla problemu, który ta metoda obchodzi zamiast rozwiązywać.
- John Jumper i in., Highly accurate protein structure prediction with AlphaFold, Nature, t. 596 (2021)
Przywołane dla porównania: tam też decydował niezależny sprawdzian.
- Meredith Ringel Morris i in., Levels of AGI for Operationalizing Progress on the Path to AGI, arXiv (Google DeepMind) (2023)
Więcej w dziale Sztuczna inteligencja
Cały dział →
Komentarze
Wczytuję komentarze…