Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
View / Open Files
Conference Name
International Joint Conference on Automated Reasoning 2022
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Mangla, C., Holden, s., & Paulson, L. Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers. International Joint Conference on Automated Reasoning 2022. https://doi.org/10.17863/CAM.84911
Abstract
A strategy schedule 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.
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)
Embargo Lift Date
2023-05-26
Identifiers
External DOI: https://doi.org/10.17863/CAM.84911
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.