Uczenie maszynowe dla zautomatyzowanego dowodzenia twierdzeń: Nauka rozwiązywania SAT i QSAT

Oryginalny tytuł:

Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT

Zawartość książki:

Zautomatyzowane dowodzenie twierdzeń reprezentuje znaczący i długotrwały obszar badań w informatyce, z licznymi zastosowaniami. Duża część metod opracowanych do tej pory w celu implementacji automatycznego dowodzenia twierdzeń (ATP) ma charakter algorytmiczny, co ma wiele wspólnego z szerszymi badaniami nad heurystycznymi algorytmami wyszukiwania. Jednak w ostatnich latach naukowcy zaczęli włączać metody uczenia maszynowego (ML) do ATP w celu uzyskania lepszej wydajności. Rozwiązywanie zadań satysfakcjonujących (SAT) i uczenie maszynowe to duże i długotrwałe obszary badań, a każdy z nich ma odpowiednio obszerną literaturę.

W tej książce autor przedstawia wyniki swojego gruntownego i systematycznego przeglądu badań na przecięciu tych dwóch pozornie raczej niezwiązanych ze sobą dziedzin. Skupia się on na badaniach, które pojawiły się do tej pory w zakresie włączania metod uczenia maszynowego do rozwiązań problemów SAT związanych ze spełnialnością propozycji, a także rozwiązań ich bezpośrednich wariantów, takich jak i kwantyfikowana SAT (QSAT). Kompleksowość omówienia oznacza, że badacze ML zyskują zrozumienie najnowocześniejszych solverów SAT i QSAT, które jest wystarczające, aby nowe możliwości zastosowania ich własnych badań ML w tej dziedzinie były wyraźnie widoczne, podczas gdy badacze ATP zyskują jasne zrozumienie, w jaki sposób najnowocześniejsze uczenie maszynowe może pomóc im w projektowaniu lepszych solverów.

Prezentując materiał, autor koncentruje się na zastosowanych metodach uczenia się i sposobie, w jaki zostały one włączone do solverów. Dzięki temu badacze i studenci zarówno w dziedzinie automatycznego dowodzenia twierdzeń, jak i uczenia maszynowego mogą a) dowiedzieć się, co zostało wypróbowane i b) zrozumieć często złożoną interakcję między ATP i ML, która jest niezbędna do odniesienia sukcesu w tych niezaprzeczalnie wymagających zastosowaniach.