Apprendimento automatico per la dimostrazione automatica dei teoremi: Imparare a risolvere SAT e QSAT

Titolo originale:

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

Contenuto del libro:

La dimostrazione automatica dei teoremi rappresenta un'area di ricerca significativa e di lunga data nell'informatica, con numerose applicazioni. Gran parte dei metodi sviluppati finora per l'implementazione di teoremi automatici (ATP) sono stati di tipo algoritmico, condividendo molto in comune con il più ampio studio degli algoritmi di ricerca euristica. Tuttavia, negli ultimi anni i ricercatori hanno iniziato a incorporare metodi di apprendimento automatico (ML) negli ATP nel tentativo di ottenere prestazioni migliori. La risoluzione della soddisfacibilità proposizionale (SAT) e l'apprendimento automatico sono entrambe aree di ricerca di ampia portata e di lunga data, con una letteratura altrettanto vasta.

In questo libro, l'autore presenta i risultati di una revisione approfondita e sistematica della ricerca all'intersezione di questi due campi apparentemente non correlati. Si concentra sulla ricerca che è apparsa finora sull'incorporazione dei metodi di ML nei risolutori per i problemi SAT di soddisfacibilità proposizionale, e anche nei risolutori per le sue varianti immediate, come il SAT quantificato (QSAT). La completezza della trattazione consente ai ricercatori di ML di acquisire una comprensione dello stato dell'arte dei risolutori SAT e QSAT sufficiente a rendere chiaramente visibili le nuove opportunità di applicazione della propria ricerca ML a questo dominio, mentre i ricercatori ATP ottengono una chiara valutazione di come l'apprendimento automatico all'avanguardia possa aiutarli a progettare risolutori migliori.

Nel presentare il materiale, l'autore si concentra sui metodi di apprendimento utilizzati e sul modo in cui sono stati incorporati nei risolutori. Ciò consente ai ricercatori e agli studenti di Automated Theorem Proving e Machine Learning di a) sapere cosa è stato provato e b) comprendere l'interazione spesso complessa tra ATP e ML, necessaria per il successo in queste applicazioni innegabilmente impegnative.