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

Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson

AAAI 2020 pp. 13919-13920

doi:10.1609/AAAI.V34I10.7232 /aaai/2020/slowik2020aaai-bayesian/

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.

PDF AAAI Semantic Scholar

Cite

Text

Slowik et al. "Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract)." AAAI Conference on Artificial Intelligence, 2020. doi:10.1609/AAAI.V34I10.7232

Markdown

[Slowik et al. "Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract)." AAAI Conference on Artificial Intelligence, 2020.](https://mlanthology.org/aaai/2020/slowik2020aaai-bayesian/) doi:10.1609/AAAI.V34I10.7232

BibTeX

@inproceedings{slowik2020aaai-bayesian,
  title     = {{Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract)}},
  author    = {Slowik, Agnieszka and Mangla, Chaitanya and Jamnik, Mateja and Holden, Sean B. and Paulson, Lawrence C.},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2020},
  pages     = {13919-13920},
  doi       = {10.1609/AAAI.V34I10.7232},
  url       = {https://mlanthology.org/aaai/2020/slowik2020aaai-bayesian/}
}