高效神经子句选择强化学习

子句选择可以说是基于饱和的定理证明中最重要的选择点。将其建模为强化学习(RL)任务，是挑战最先进的证明器中人工设计的启发式方法、并从证明经验出发自动演化其潜在最优替代方案的一种方式。在这项工作中，我们提出了一种用于子句选择打分的神经网络架构，该架构功能强大且求值高效。遵循强化学习原则进行设计决策，我们将该网络集成到Vampire定理证明器中，并从成功的证明尝试中进行训练。在多样化的TPTP基准测试上的实验表明，神经引导的证明器在实践相关的短CPU指令限制下求解训练未见问题的数量上，相比其最初学习的基线策略提升了20%。