Bayesian Optimisation with Gaussian Processes for Premise Selection
Artificial Intelligence
2019-09-23 v1 Machine Learning
Abstract
Heuristics in theorem provers are often parameterised. Modern theorem provers such as Vampire 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 probablistic framework for heuristics optimisation in theorem provers. We present results using a heuristic for premise selection and The Archive of Formal Proofs (AFP) as a case study.
Keywords
Cite
@article{arxiv.1909.09137,
title = {Bayesian Optimisation with Gaussian Processes for Premise Selection},
author = {Agnieszka Słowik and Chaitanya Mangla and Mateja Jamnik and Sean B. Holden and Lawrence C. Paulson},
journal= {arXiv preprint arXiv:1909.09137},
year = {2019}
}