Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).
View / Open Files
Publication Date
2020Journal Title
Proceedings of the AAAI Conference on Artificial Intelligence, 34(10)
Conference Name
AAAI 2020
ISBN
978-1-57735-823-7
Publisher
AAAI Press
Pages
13919-13920
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Slowik, A., Mangla, C., Jamnik, M., Holden, S. B., & Paulson, L. C. (2020). Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).. Proceedings of the AAAI Conference on Artificial Intelligence, 34(10), 13919-13920. https://doi.org/10.1609/aaai.v34i10.7232
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.
Identifiers
External DOI: https://doi.org/10.1609/aaai.v34i10.7232
This record's URL: https://www.repository.cam.ac.uk/handle/1810/332827
Rights
Publisher's own licence
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.