| ||||
| ||||
![]() Title:Bayesian Optimisation with Gaussian Processes for Premise Selection Conference:Vampire 2019 Tags:automated theorem proving, bayesian optimisation, gaussian processes, machine learning, premise selection, theorem proving, upper confidence bound and vampire Abstract: Heuristics in theorem provers are often parameterised. Modern theorem provers such as Vampire (Kovács & Voronkov, 2013) 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 integrated with Vampire and The Archive of Formal Proofs (AFP) (Jaskelioff & Merz, 2005) as a case study. Bayesian Optimisation with Gaussian Processes for Premise Selection ![]() Bayesian Optimisation with Gaussian Processes for Premise Selection | ||||
Copyright © 2002 – 2025 EasyChair |