Bayesian Optimisation with Gaussian Processes for Premise Selection
This work addresses the challenge of parameter tuning for theorem provers, which is crucial for enhancing automated reasoning efficiency, though it appears incremental as it applies an existing optimization method to a specific domain.
The paper tackled the problem of optimizing heuristic parameters in theorem provers, which is intractable via exhaustive search, by introducing a Bayesian optimization framework with Gaussian processes, achieving improved performance as demonstrated in a case study on premise selection using the Archive of Formal Proofs.
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.