Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
Automatisiertes Theorembeweisen ist ein bedeutendes und langjähriges Forschungsgebiet der Informatik mit zahlreichen Anwendungen. Ein Großteil der bisher entwickelten Methoden für die Implementierung von automatischen Theorembeweisern (ATPs) ist algorithmisch und hat viel mit der breiteren Untersuchung heuristischer Suchalgorithmen gemeinsam. In den letzten Jahren haben Forscher jedoch damit begonnen, Methoden des maschinellen Lernens (ML) in ATPs einzubauen, um eine bessere Leistung zu erzielen. Das Lösen von Aussagen zur Erfüllbarkeit (SAT) und maschinelles Lernen sind beides große und langjährige Forschungsgebiete, und für beide gibt es eine entsprechend umfangreiche Literatur.
In diesem Buch präsentiert der Autor die Ergebnisse seiner gründlichen und systematischen Untersuchung der Forschung an der Schnittstelle dieser beiden scheinbar nicht miteinander verbundenen Gebiete. Es konzentriert sich auf die Forschung, die bisher erschienen ist, um ML-Methoden in Löser für SAT-Probleme mit propositionaler Erfüllbarkeit einzubauen, und auch in Löser für deren unmittelbare Varianten wie quantifizierter SAT (QSAT). Die Vollständigkeit der Abdeckung bedeutet, dass ML-Forscher ein Verständnis des Stands der Technik bei SAT- und QSAT-Lösern erlangen, das ausreicht, um neue Möglichkeiten für die Anwendung ihrer eigenen ML-Forschung auf diesem Gebiet klar zu erkennen, während ATP-Forscher ein klares Verständnis dafür erlangen, wie modernes maschinelles Lernen ihnen helfen könnte, bessere Löser zu entwerfen.
Bei der Darstellung des Materials konzentriert sich der Autor auf die verwendeten Lernmethoden und die Art und Weise, wie sie in die Löser integriert wurden. Dies ermöglicht es Forschern und Studenten sowohl im Bereich des automatisierten Theorembeweisens als auch des maschinellen Lernens, a) zu wissen, was ausprobiert wurde, und b) die oft komplexe Interaktion zwischen ATP und maschinellem Lernen zu verstehen, die für den Erfolg bei diesen unbestreitbar anspruchsvollen Anwendungen erforderlich ist.
| ISBN: | 9781680838985 |
| Autor: | |
| Verlag: | |
| Sprache: | Englisch |
| Einband: | Taschenbuch |
Derzeit verfügbar, auf Lager.
