Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving

Good heuristics are essential for successful proof search in first-order automated theorem proving. As a result, state-of-the-art theorem provers offer a range of options for tuning the proof search process to specific problems. However, the vast configuration space makes it exceedingly challenging to construct effective heuristics. In this paper we present a new approach called HOS-ML, for automatically discovering new heuristics and mapping problems into optimised local schedules comprising of these heuristics. Our approach is based on interleaving Bayesian hyper-parameter optimisation for discovering promising heuristics and dynamic clustering to make optimisation efficient on heterogeneous problems. HOS-ML also use constraint programming to devise locally optimal schedules and machine learning for mapping unseen problems into such schedules. We evaluated HOS-ML on the theorem prover iProver and demonstrated that it can discover new heuristics that considerably improve performance and can solve problems that have not been solved previously by any other system.

Automated summary

This paper introduces a new approach called HOS-ML for automatically discovering new heuristics and mapping problems into optimised local schedules. The approach combines Bayesian hyper-parameter optimisation and dynamic clustering to improve the effectiveness of heuristics, and utilizes constraint programming and machine learning for optimal scheduling and problem mapping. Evaluation on the iProver theorem prover shows that HOS-ML can discover new heuristics that significantly enhance performance and solve previously unsolved problems.