Regularization in Spider-Style Strategy Discovery and Schedule Construction
<|reference_start|>Regularization in Spider-Style Strategy Discovery and Schedule Construction: 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.<|reference_end|>
@article{bártek2024regularization,
    title={Regularization in Spider-Style Strategy Discovery and Schedule
  Construction},
    author={Filip B'artek, Karel Chvalovsk'y, Martin Suda},
    journal={Automated Reasoning. IJCAR 2024. 194-213},
    year={2024},
    doi={10.1007/978-3-031-63498-7_12},
    archivePrefix={arXiv},
    eprint={2403.12869},
    primaryClass={cs.AI cs.LO}
}