Bayesian Optimisation with Gaussian Processes for Premise Selection

TL;DR

This paper introduces a probabilistic framework using Gaussian processes for optimizing heuristics in theorem provers, demonstrated through premise selection in the AFP case study.

Contribution

It presents a novel Bayesian optimization approach for parameter tuning in theorem provers, improving heuristic performance.

Findings

Effective premise selection heuristic developed

Significant performance improvements in AFP case study

Framework adaptable to other theorem prover heuristics

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.