Open AccessBayesian Optimisation for Heuristic Configuration in Automated Theorem Proving
Author(s) -
Agnieszka Słowik,
Chaitanya Mangla,
Mateja Jamnik,
Sean B. Holden,
Lawrence C. Paulson
Publication year - 2020
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/q91g
Subject(s) - heuristics , premise , mathematical proof , computer science , selection (genetic algorithm) , heuristic , inference , vampire , formal proof , probabilistic logic , automated theorem proving , theoretical computer science , mathematical optimization , algorithm , mathematics , artificial intelligence , philosophy , linguistics , geometry
Modern 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.