Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving
Published version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Słowik, Agnieszka https://orcid.org/0000-0001-7113-4098
Mangla, Chaitanya https://orcid.org/0000-0001-7600-1681
Jamnik, Mateja https://orcid.org/0000-0003-2772-2532
Holden, Sean https://orcid.org/0000-0001-7979-1148
Paulson, Lawrence https://orcid.org/0000-0003-0288-4279
Abstract
jats:pModern theorem provers such as Vampire utilise premise selection algorithms to control the proof search explosion. Premise selection heuristics often employ an array of continuous and discrete parameters. The quality of recommended premises varies depending on the parameter assignment. In this work, we introduce a principled probabilistic framework for optimisation of a premise selection algorithm. We present results using Sumo Inference Engine (SInE) and the Archive of Formal Proofs (AFP) as a case study. Our approach can be used to optimise heuristics on large theories in minimum number of steps.</jats:p>
Description
Keywords
46 Information and Computing Sciences, 49 Mathematical Sciences, 4602 Artificial Intelligence
Journal Title
EPiC Series in Computing
Conference Name
Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
Journal ISSN
2398-7340
Volume Title
Publisher
EasyChair
Publisher DOI
Rights
All rights reserved
Sponsorship
Engineering and Physical Sciences Research Council (1788755)
EPSRC (2119928)
EPSRC (2119928)