Mentionsy

No tak pytam o to dlatego, że obecnie mamy do czynienia przede wszystkim ze sztuczną inteligencją i tymi systemami dowodzącymi, różnymi LLM-ami i tak dalej, które wydaje się, że coraz więcej jest głosów, że one mają duży udział w matematyce i jest wręcz taka sugestia, że matematyka może być jedną z takich dziedzin, która pierwsza będzie albo która będzie bardzo mocna.

No więc były próby tego, żeby, to jeszcze przed LLM-ami, próby tego, żeby sformalizować, co to znaczy.

LLM-y mają ten plus, że to, o czym mówiłem poprzednio, to jest brute force, czyli przeszukiwanie wszystkich możliwych dowodów.

LLM-y mają ten plus, że one tworzą zdania, one tworzą zdania w języku naturalnym, ale te zdania mają sens.

Można spokojnie założyć, że możemy zbudować LLM-a i na pewno ktoś to zrobi, który buduje zdania w języku matematyki i one też mają sens i możemy od razu formalnie zweryfikować.

Więc myślę, że moc przeszukiwania tego jakby, wiesz, zbioru wszystkich możliwych stwierdzeń przez LLM-y w celu szukania tych stwierdzeń, które są ciekawe, jest znacznie większa, więc to powinno doprowadzić do lepszych wyników.

I jesteśmy teraz w momencie, kiedy już zaczynają się pojawiać pierwsze dowody napisane naprawdę przez LLM-y.

I w tym LLM są całkiem niezłe.

Mi się wydaje, że kluczowe w tej chwili jest właśnie to, żeby nauczyć LLM-y, co to znaczy, że stwierdzenie jest ciekawe.

Wracając trochę do sedna, nie widzę powodu, żeby LLM miały się nie nauczyć rozpoznawać pięknych stwierdzeń.

Natomiast to, co wydaje mi się z technicznego punktu widzenia najciekawsze w tej chwili, to LLM, czy w ogóle sztuczna inteligencja, w sensie sieci neuronowych, działają w ten sposób, że one w czasie treningu tworzą jakiś output, w sensie coś tworzą i porównują to coś z tym, do czego próbowały dojść.

No i teraz to, czego w matematyce na razie, o tyle ile wiem, nie udało się zrobić, to nikt nie stworzył takiego systemu, który jest w stanie powiedzieć, na ile to, co LLM stworzył, jest dalekie od tego, co próbujemy stworzyć, tak?

Więc LLM jest w stanie wyprodukować kawałek dowodu i sprawdzić go przy pomocy tych weryfikatorów automatycznych, czy ten dowód jest poprawny, ale nie mamy miary niepoprawności.

Wydaje mi się, że gdyby się udało tak zrobić, to wtedy LLM zaczęłyby produkować matematykę w tempie zupełnie niedoścignionym dla człowieka.

Bo moim zdaniem, w sensie ja nie twierdzę, że mózg ludzki jest LLM-em, ale ten proces uczenia się, chociaż wiadomo, że on w inny sposób zachodzi niż w LLM-ach, to jest jednak fundamentalnie taki sam.

Czy może właśnie ta matematyka też potrzebuje pewnego rodzaju procesu, w tym wypadku procesu, nie wiem, czy to umysłowego, czy to realizowanego na przykład na LLM-ach, czy na komputerach, czy na czymkolwiek, który ujawnia dopiero te struktury w jakimś sensie, że one się pojawiają, ale one potrzebują tego procesu, który za nimi stoi.

Mamy mnóstwo tego przy okazji LLM-ów teraz, czy LLM-y są świadome, jaka jest prawdziwa natura LLM-u.