Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

8 Downloads (Pure)

Abstract

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.

Original languageEnglish
Title of host publicationInternational Conference on Intelligent Computer Mathematics 2021
Subtitle of host publication Intelligent Computer Mathematics
PublisherSpringer Cham
Pages107-123
ISBN (Electronic)978-3-030-81097-9
ISBN (Print)978-3-030-81096-2
DOIs
Publication statusPublished - 20 Jul 2021

Publication series

NameIntelligent Computer Mathematics
Volume12833
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Theorem proving
  • Machine learning
  • Heuristic optimisation
  • Heuristic selection
  • Dynamic clustering

Fingerprint

Dive into the research topics of 'Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving'. Together they form a unique fingerprint.

Cite this