期刊
INTELLIGENT COMPUTER MATHEMATICS (CICM 2021)
卷 12833, 期 -, 页码 107-123出版社
SPRINGER INTERNATIONAL PUBLISHING AG
DOI: 10.1007/978-3-030-81097-9_8
关键词
Theorem proving; Machine learning; Heuristic optimisation; Heuristic selection; Dynamic clustering
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.
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据