Machine Learning for Automated Theorem Proving: Învățarea rezolvării SAT și QSAT

Titlul original:

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

Conținutul cărții:

Demonstrarea automată a teoremelor reprezintă un domeniu de cercetare semnificativ și de lungă durată în informatică, cu numeroase aplicații. O mare parte a metodelor dezvoltate până în prezent pentru punerea în aplicare a demonstratoarelor automate de teoreme (ATP) au fost algoritmice, având multe în comun cu studiul mai larg al algoritmilor euristici de căutare. Cu toate acestea, în ultimii ani, cercetătorii au început să încorporeze metode de învățare automată (ML) în ATP în încercarea de a obține performanțe mai bune. Rezolvarea satisfiabilității propoziționale (SAT) și învățarea automată sunt ambele domenii de cercetare vaste și de lungă durată, fiecare având o literatură de specialitate corespunzătoare.

În această carte, autorul prezintă rezultatele revizuirii sale aprofundate și sistematice a cercetării la intersecția acestor două domenii aparent fără legătură. Acesta se concentrează pe cercetările care au apărut până în prezent cu privire la încorporarea metodelor ML în soluțiile pentru problemele SAT de satisfiabilitate propozițională, precum și în soluțiile pentru variantele sale imediate, cum ar fi și SAT cuantificat (QSAT). Caracterul cuprinzător al acoperirii înseamnă că cercetătorii ML dobândesc o înțelegere a soluțiilor SAT și QSAT de ultimă generație care este suficientă pentru a face clar vizibile noile oportunități de aplicare a propriilor cercetări ML în acest domeniu, în timp ce cercetătorii ATP dobândesc o apreciere clară a modului în care învățarea automată de ultimă generație îi poate ajuta să conceapă soluții mai bune.

În prezentarea materialului, autorul se concentrează pe metodele de învățare utilizate și pe modul în care acestea au fost încorporate în rezolvatoare. Acest lucru permite cercetătorilor și studenților atât în domeniul demonstrației automate de teoreme, cât și în cel al învățării automate a) să știe ce s-a încercat și b) să înțeleagă interacțiunea adesea complexă dintre ATP și ML, necesară pentru succesul în aceste aplicații incontestabil dificile.