Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract)

Authors

  • Agnieszka Słowik University of Cambridge
  • Chaitanya Mangla University of Cambridge
  • Mateja Jamnik University of Cambridge
  • Sean B. Holden University of Cambridge
  • Lawrence C. Paulson University of Cambridge

DOI:

https://doi.org/10.1609/aaai.v34i10.7232

Abstract

Modern theorem provers 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 probabilistic framework for heuristic optimisation in theorem provers. We present results using a heuristic for premise selection and the Archive of Formal Proofs (AFP) as a case study.

AAAI-20 Proceedings Cover

Downloads

Published

2020-04-03

How to Cite

Słowik, A., Mangla, C., Jamnik, M., Holden, S. B., & Paulson, L. C. (2020). Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). Proceedings of the AAAI Conference on Artificial Intelligence, 34(10), 13919-13920. https://doi.org/10.1609/aaai.v34i10.7232

Issue

Vol. 34 No. 10: Issue 10: AAAI-20 Student Tracks

Section

Student Abstract Track