Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
Az automatizált tételbizonyítás a számítástechnika jelentős és régóta tartó kutatási területe, számos alkalmazással. Az automatizált tételbizonyítók (ATP-k) megvalósítására eddig kifejlesztett módszerek nagy része algoritmikus, és sok közös vonásuk van a heurisztikus keresési algoritmusok szélesebb körű vizsgálatával. Az utóbbi években azonban a kutatók a jobb teljesítmény elérése érdekében elkezdték a gépi tanulási (ML) módszereket beépíteni az ATP-kbe. A feltételes kielégíthetőség (SAT) megoldása és a gépi tanulás egyaránt nagy és régóta fennálló kutatási területek, és mindegyiknek megfelelően nagy irodalma van.
Ebben a könyvben a szerző e két, látszólag egymástól meglehetősen független terület metszéspontjában végzett kutatások alapos és szisztematikus áttekintésének eredményeit mutatja be. Azokra a kutatásokra összpontosít, amelyek eddig az ML-módszerek beépítésével kapcsolatban jelentek meg a proposicionális kielégíthetőségi SAT-problémák megoldóiban, valamint a közvetlen változatainak, például a kvantált SAT-nak (QSAT) a megoldóiban. A lefedettség átfogó jellege azt jelenti, hogy az ML-kutatók olyan ismereteket szereznek a legkorszerűbb SAT- és QSAT-megoldókról, amelyek elegendőek ahhoz, hogy világosan láthatóvá váljanak a saját ML-kutatásaik e területen való alkalmazásának új lehetőségei, míg az ATP-kutatók világos képet kapnak arról, hogy a legkorszerűbb gépi tanulás hogyan segíthet nekik jobb megoldók tervezésében.
Az anyag bemutatásakor a szerző az alkalmazott tanulási módszerekre és arra koncentrál, hogy ezeket hogyan építették be a megoldókba. Ez lehetővé teszi, hogy mind az automatizált tételbizonyítás, mind a gépi tanulás kutatói és hallgatói a) tudják, hogy mit próbáltak ki, és b) megértsék az ATP és az ML közötti gyakran összetett kölcsönhatást, amely szükséges a sikerhez ezekben a kétségtelenül nagy kihívást jelentő alkalmazásokban.