Titre original :
Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
Contenu du livre :
La preuve automatique de théorèmes représente un domaine de recherche important et ancien en informatique, avec de nombreuses applications. Une grande partie des méthodes développées à ce jour pour la mise en œuvre de prouveurs de théorèmes automatisés (PTA) ont été algorithmiques, partageant beaucoup de points communs avec l'étude plus large des algorithmes de recherche heuristique. Cependant, ces dernières années, les chercheurs ont commencé à incorporer des méthodes d'apprentissage automatique dans les ATP afin d'obtenir de meilleures performances. La résolution de la satisfaisabilité propositionnelle (SAT) et l'apprentissage automatique sont deux domaines de recherche importants et de longue date, et chacun d'eux fait l'objet d'une littérature abondante.
Dans ce livre, l'auteur présente les résultats de son examen approfondi et systématique de la recherche à l'intersection de ces deux domaines apparemment sans rapport. Il se concentre sur la recherche qui est apparue à ce jour sur l'incorporation des méthodes de ML dans les solveurs pour les problèmes SAT de satisfiabilité propositionnelle, ainsi que les solveurs pour ses variantes immédiates telles que le SAT quantifié (QSAT). L'exhaustivité de la couverture signifie que les chercheurs en ML acquièrent une compréhension des solveurs SAT et QSAT de pointe suffisante pour que de nouvelles opportunités d'application de leur propre recherche en ML à ce domaine soient clairement visibles, tandis que les chercheurs en ATP acquièrent une appréciation claire de la manière dont l'apprentissage automatique de pointe peut les aider à concevoir de meilleurs solveurs.
Dans sa présentation, l'auteur se concentre sur les méthodes d'apprentissage utilisées et sur la manière dont elles ont été incorporées dans les solveurs. Cela permet aux chercheurs et aux étudiants, tant dans le domaine de la résolution automatique de théorèmes que dans celui de l'apprentissage automatique, a) de savoir ce qui a été essayé et b) de comprendre l'interaction souvent complexe entre la résolution automatique de théorèmes et l'apprentissage automatique, qui est nécessaire pour réussir dans ces applications indéniablement difficiles.
Autres informations sur le livre :
| ISBN : | 9781680838985 |
| Auteur : | |
| Éditeur : | |
| Langue : | anglais |
| Reliure : | Broché |
Achat:
Actuellement disponible, en stock.
