# Regularization in Spider-Style Strategy Discovery and Schedule Construction

arXiv: https://arxiv.org/abs/2403.12869 · HTML: https://mlsanity.com/paper/2403.12869/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 41 references that are in the map.
- First posted on arXiv 19 Mar 2024.

## Builds on (most cited first, 6 of 6)

- [SMAC3: A Versatile Bayesian Optimization Package for Hyperparameter Optimization](https://mlsanity.com/paper/2109.09831/) (2021)
- [ParamILS: An Automatic Algorithm Configuration Framework](https://mlsanity.com/paper/1401.3492/) (2014)
- [A Survey of Methods for Automated Algorithm Configuration](https://mlsanity.com/paper/2202.01651/) (2022)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [BliStrTune: Hierarchical Invention of Theorem Proving Strategies](https://mlsanity.com/paper/1611.08733/) (2016)
- [MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers](https://mlsanity.com/paper/1308.2116/) (2013)

## Built on by (most cited first, 2 of 2)

- [Machine Learning for Quantifier Selection in cvc5](https://mlsanity.com/paper/2408.14338/) (2024)
- [Efficient Neural Clause-Selection Reinforcement](https://mlsanity.com/paper/2503.07792/) (2025)

## Abstract (arXiv)

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.