论文标题
经过复发的神经网络选择状态前提
Stateful Premise Selection by Recurrent Neural Networks
论文作者
论文摘要
在这项工作中，我们开发了一种基于学习的新方法，用于在大型正式图书馆证明新目标时选择事实（前提）。与以前的方法相互独立地选择事实集的方法不同，新方法使用\ emph {state}的概念，每次选择事实时都会更新。我们的状态体系结构基于经常性的神经网络，这些神经网络最近在语言翻译等状态任务中非常成功。新方法与数据增强技术结合使用，以标准大理论基准进行多种评估，并将其与基于梯度增强树的最新前提方法进行了比较。证明它的性能要好得多，并解决了许多新问题。
In this work, we develop a new learning-based method for selecting facts (premises) when proving new goals over large formal libraries. Unlike previous methods that choose sets of facts independently of each other by their rank, the new method uses the notion of \emph{state} that is updated each time a choice of a fact is made. Our stateful architecture is based on recurrent neural networks which have been recently very successful in stateful tasks such as language translation. The new method is combined with data augmentation techniques, evaluated in several ways on a standard large-theory benchmark, and compared to state-of-the-art premise approach based on gradient boosted trees. It is shown to perform significantly better and to solve many new problems.
