Bayesian Optimisation with Gaussian Processes for Premise Selection
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Bayesian OptimisationGaussian ProcessesSimilar Papers 제목 키워드 기반
GAUCHE: A Library for Gaussian Processes in Chemistry
We introduce GAUCHE, a library for GAUssian processes in CHEmistry. Gaussian processes have long been a cornerstone of probabilistic machine learning, affording particular advantages for uncertainty quantification and Ba…
Bayesian OptimisationGaussian ProcessesUncertainty QuantificationInducing Point Allocation for Sparse Gaussian Processes in High-Throughput Bayesian Optimisation
Sparse Gaussian Processes are a key component of high-throughput Bayesian Optimisation (BO) loops; however, we show that existing methods for allocating their inducing points severely hamper optimisation performance. By …
Bayesian OptimisationDecision MakingDiversityGaussian Processes+2Theoretical Analysis of Bayesian Optimisation with Unknown Gaussian Process Hyper-Parameters
Bayesian optimisation has gained great popularity as a tool for optimising the parameters of machine learning algorithms and models. Somewhat ironically, setting up the hyper-parameters of Bayesian optimisation methods i…
Bayesian OptimisationGaussian Processesparameter estimationBayesian Image Classification with Deep Convolutional Gaussian Processes
In decision-making systems, it is important to have classifiers that have calibrated uncertainties, with an optimisation objective that can be used for automated model selection and training. Gaussian processes (GPs) pro…
ClassificationDecision MakingGaussian ProcessesGeneral Classification+4Multi-view Bayesian optimisation in reduced dimension for engineering design
Bayesian optimisation is an adaptive sampling strategy for constructing a Gaussian process surrogate to emulate a black-box computational model with the aim of efficiently searching for the global minimum. However, Gauss…
Bayesian OptimisationGaussian ProcessesMULTI-VIEW LEARNING