Strojové učenie pre automatizované dokazovanie tvrdení: Učenie sa riešiť SAT a QSAT

Pôvodný názov:

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

Obsah knihy:

Automatizované dokazovanie tvrdení predstavuje významnú a dlhodobú oblasť výskumu v informatike s mnohými aplikáciami. Veľká časť doteraz vyvinutých metód na implementáciu automatizovaného dokazovania tvrdení (ATP) bola algoritmická a má veľa spoločného so širším štúdiom heuristických vyhľadávacích algoritmov. V posledných rokoch však výskumníci začali do ATP začleňovať metódy strojového učenia (ML) v snahe dosiahnuť lepší výkon. Riešenie splniteľnosti výrokov (SAT) a strojové učenie sú rozsiahle a dlhodobé oblasti výskumu a každá z nich má zodpovedajúcu rozsiahlu literatúru.

V tejto knihe autor predstavuje výsledky svojho dôkladného a systematického prehľadu výskumu na pomedzí týchto dvoch zdanlivo nesúvisiacich oblastí. Zameriava sa na výskum, ktorý sa doteraz objavil v oblasti začlenenia metód ML do riešiteľov výrokovej splniteľnosti úloh SAT a tiež riešiteľov jej bezprostredných variantov, ako je kvantifikovaný SAT (QSAT). Komplexnosť pokrytia znamená, že výskumníci v oblasti ML získajú prehľad o najnovších riešiteľoch SAT a QSAT, ktorý je dostatočný na to, aby sa jasne ukázali nové možnosti uplatnenia ich vlastného výskumu v tejto oblasti, zatiaľ čo výskumníci v oblasti ATP získajú jasnú predstavu o tom, ako by im mohlo najmodernejšie strojové učenie pomôcť pri navrhovaní lepších riešiteľov.

Pri prezentácii materiálu sa autor sústreďuje na použité metódy učenia a spôsob ich začlenenia do riešiteľov. To umožňuje výskumníkom a študentom v oblasti automatizovaného dokazovania tvrdení aj strojového učenia a) vedieť, čo bolo vyskúšané, a b) pochopiť často zložitú interakciu medzi ATP a ML, ktorá je potrebná na úspech v týchto nesporne náročných aplikáciách.