Regularization in Spider-Style Strategy Discovery and Schedule Construction
This work addresses the challenge of optimizing automated theorem proving for competition and practical use, though it appears incremental as it builds on existing Spider ideas.
The paper tackled the problem of constructing effective proving strategy schedules for the Vampire theorem prover on the FOF fragment of the TPTP library, based on Spider-style methods, and found that such schedules can generalize well to unseen problems with specific factors influencing performance.
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.