about
Bayesian Optimisation with Gaussian Processes for Premise Selection (arxiv.org)
2 points by sel1 on Sep 23, 2019 | hide | past | pdf | discuss on HN

In plain words: A smart search tunes prover settings by guessing which combinations work best and testing those next, instead of trying every one. Applied to choosing which earlier proofs to feed a prover, it found strong settings where trying every combination would take far too long.

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.

Agnieszka Słowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson
arXiv:1909.09137 · cs.AI, cs.LG · submitted Sep 18, 2019
abstract · pdf · html

add comment on HN