Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Slowik, Agnieszka
Mangla, Chaitanya
Jamnik, Mateja https://orcid.org/0000-0003-2772-2532
Holden, Sean B
Paulson, Lawrence C
Abstract
Modern theorem provers utilise a wide array of heuristics to control the search space explosion, thereby requiring optimisation of a large set of parameters. An exhaustive search in this multi-dimensional parameter space is intractable in most cases, yet the performance of the provers is highly dependent on the parameter assignment. In this work, we introduce a principled probabilistic framework for heuristic optimisation in theorem provers. We present results using a heuristic for premise selection and the Archive of Formal Proofs (AFP) as a case study.
Description
Keywords
Journal Title
Proceedings of the AAAI Conference on Artificial Intelligence, 34(10)
Conference Name
AAAI 2020
Journal ISSN
Volume Title
Publisher
AAAI Press
Publisher DOI
Rights
Publisher's own licence