Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
View / Open Files
Publication Date
2022Journal Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference Name
International Joint Conference on Automated Reasoning 2022
ISSN
0302-9743
ISBN
9783031107689
Publisher
Springer International Publishing
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Mangla, C., Holden, S., & Paulson, L. (2022). Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) https://doi.org/10.1007/978-3-031-10769-6_33
Abstract
<jats:title>Abstract</jats:title><jats:p>A<jats:italic>strategy schedule</jats:italic>allocates time to proof strategies that are used in sequence in a theorem prover. We employ Bayesian statistics to propose alternative sequences for the strategy schedule in each proof attempt. Tested on the TPTP problem library, our method yields a time saving of more than 50%. By extending this method to optimize the fixed time allocations to each strategy, we obtain a notable increase in the number of theorems proved.</jats:p>
Keywords
Bayesian machine learning, Strategy scheduling, Automated theorem proving
Sponsorship
This work was supported by the UK Engineering and Physical Sciences Research Council (EPSRC) through a Doctoral Training studentship, award reference 1788755.
Funder references
Engineering and Physical Sciences Research Council (1788755)
European Research Council (742178)
Engineering and Physical Sciences Research Council (EP/P020259/1)
Identifiers
External DOI: https://doi.org/10.1007/978-3-031-10769-6_33
This record's URL: https://www.repository.cam.ac.uk/handle/1810/337497
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.
Recommended or similar items
The current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk