Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving


Loading...
Thumbnail Image
Type
Conference Object
Change log
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>

Publication Date
2020-03-11
Online Publication Date
Acceptance Date
2019-06-27
Keywords
46 Information and Computing Sciences, 49 Mathematical Sciences, 4602 Artificial Intelligence
Journal Title
EPiC Series in Computing
Journal ISSN
2398-7340
Volume Title
Publisher
EasyChair
Rights
All rights reserved
Sponsorship
Engineering and Physical Sciences Research Council (1788755)
EPSRC (2119928)