Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Chaitanya Mangla, Sean B. Holden, Lawrence Charles Paulson · Lecture notes in computer science · 2022
Abstract Astrategy scheduleallocates 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.