Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract).
Authors
Slowik, Agnieszka
Mangla, Chaitanya
Holden, Sean B
Paulson, Lawrence C
Change log
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.
Publication Date
2020
Online Publication Date
2020-04-03
Acceptance Date
2019-12-04
Keywords
Journal Title
Proceedings of the AAAI Conference on Artificial Intelligence, 34(10)
Journal ISSN
Volume Title
Publisher
AAAI Press
Rights
Publisher's own licence