Bardzo fajny kanał o tematyce trochę matematycznej, trochę ai, trochę technologie, trochę filozofia - poniżej próbka tłumaczenia po polsku - lepiej czytać po angielsku
http://t.me/axisofordinary/8429
#matematyka
http://t.me/axisofordinary/8429
Jednym z problemów związanych z wykorzystaniem sztucznej inteligencji do wyszukiwania dowodów nie jest brak logiki, ale brak matematycznej intuicji/wyczucia. Sztuczna inteligencja optymalizuje określony cel, a nie "ducha zadania".
...
Przestrzeń możliwych problemów, dowodów i systemów aksjomatów jest praktycznie nieskończona. Większość z nich jest trywialna, zdegenerowana lub mało pouczająca. Prawdziwą umiejętnością jest znalezienie rzadkiego sformułowania, które ujawnia autentyczną strukturę: rozwiązywalną, nietrywialną i wartą przemyślenia.
Dlatego zdolności matematyczne to nie tylko surowa moc logiczna. Na najwyższym poziomie to kwestia gustu: intuicja pozwalająca wyczuć, gdzie kryje się interesujący problem.
One problem with using AI to find proofs is not that it lacks logic, but that it lacks mathematical taste. It optimizes the stated objective, not the spirit of the problem. Given a poorly specified target, it may find a perfectly valid proof that slips through a loophole, dissolving the intended question rather than solving it.
Thought experiments reveal the same failure mode. Some people respond not by engaging the dilemma, but by choosing an interpretation that makes it disappear: “call the police,” “don’t press either button,” “destroy the machine.” But the point of a thought experiment is not to win by escaping the setup. The point is to find the interpretation under which the problem becomes maximally revealing.
The space of possible problems, proofs, and axiom systems is effectively infinite. Most are trivial, degenerate, or unilluminating. The real skill is locating the rare formulation that exposes a genuine structure: solvable, nontrivial, and worth thinking about.
This is why mathematical ability is not merely raw logical power. At the highest level, it is taste: the intuition for where the interesting problem is hiding.
#matematyka
borubar
2
Pomysł na użycie komputera dla znalezienia dowodu matematycznego nie jest nowy - to robiono już pod koniec XX wieku. Między innymi w ten sposób dowodzono twierdzenia o 4 kolorach (że dowolną mapę można pomalować na 4 kolory tak aby sąsiednie obszary miały różne kolory), to z takich bardziej znanych twierdzeń bo jeszcze było sporo mniej znanych udowodnionych w ten sposób. Ale to były wszystko dowody za pomocą brutalnej siły - na zasadzie najpierw wygeneruj a potem sprawdź wszystkie możliwe przypadki.
Tyle że niektóre problemy matematyczne bywają bardzo skomplikowane i ilość obliczeń jest tak duża, że nie ma na świecie wystarczająco wielu komputerów aby rozwiązać je w ten sposób.
Dlatego sięga się po sztuczną inteligencję która ma szybciej eliminować część rozwiązań niewartych sprawdzania albo przeciwnie wskazać przypadki które warto sprawdzić w pierwszej kolejności.
To są algorytmy optymalizacyjne podpatrzone w naturze np programowanie genetyczne (gdzie wprowadza się losowe zmiany i patrzy czy dają poprawę czy pogorszenie, jeśli jest poprawa to takie rozwiązanie się promuje i wprowadza kolejne zmiany), albo poszukiwanie w czegoś w podobny sposób jak mrówki szukają jedzenia i pozostawiają feromony dla oznaczenia drogi którą przebyły.