Repository logo
 

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

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Slowik, Agnieszka 
Mangla, Chaitanya 
Holden, Sean B 
Paulson, Lawrence C 

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.

Description

Keywords

Journal Title

Proceedings of the AAAI Conference on Artificial Intelligence, 34(10)

Conference Name

AAAI 2020

Journal ISSN

Volume Title

Publisher

AAAI Press

Rights

Publisher's own licence