Regularization in Spider-Style Strategy Discovery and Schedule Construction
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要