教吸血鬼新把戏：神经子句选择的实验研究
Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
浏览论文内容
中文总结 AI 辅助
本文实验研究Vampire定理证明器中神经子句选择引导方法，发现跨基准应用效果不佳，但通过多数据集联合训练单一模型可弥补差距，且组合策略下收益递减。
中文摘要 AI 辅助
最近研究表明，在Vampire定理证明器中采用神经子句选择引导方法，能显著提高证明器在TPTP基准上默认策略的成功率。我们通过实验研究了该方法在多个ITP衍生基准集上的影响及其与定理证明策略的交互作用。我们发现，虽然神经引导在单个基准域内持续提升性能，但跨基准应用引导模型时，其表现不如简单的默认策略。这个问题可以通过在所有数据集上同时训练单一模型来解决。这样的模型虽然获取成本更高，但能帮助Vampire在几乎所有数据集上几乎追平性能。当考虑组合策略时，情况则不那么明确，表明神经引导仍有持续价值，但收益递减。
英文摘要
A neural clause-selection guidance approach in the Vampire theorem prover was recently shown to substantially improve the success rate of the prover's default strategy on the TPTP benchmark. We experimentally study the impact of the approach across several ITP-derived benchmark sets and its interaction with theorem proving strategies. We find that while the neural guidance consistently improves performance within individual benchmark domains, cross-benchmark application of guiding models underperforms the plain default strategy. This can be remedied by training a single model on all datasets at once. Such a model, although more expensive to obtain, helps Vampire almost catch up in performance across all datasets. The picture when considering combined strategies is less clear-cut, indicating persisting value of neural guidance but under diminishing returns.
发表机构
- Czech Technical University in Prague（布拉格捷克理工大学）
- University of Gothenburg（哥德堡大学）
机构由 AI 辅助整理，请以论文原文为准。
