Regularization in Spider-Style Strategy Discovery and Schedule Construction
arXiv:2403.12869 · doi:10.1007/978-3-031-63498-7_12
Abstract
To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In this paper, we report on a large-scale experiment with discovering strategies for the Vampire prover, targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Andrei Voronkov's system Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, and establish how well a schedule can be expected to generalize to unseen problems and what factors influence this property.
25 pages, 8 figures; updated cosmetically for publication in IJCAR 2024 proceedings