Repository logo
 

Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving

Published version
Peer-reviewed

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>

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

Rights

All rights reserved
Sponsorship
Engineering and Physical Sciences Research Council (1788755)
EPSRC (2119928)