基于循环神经网络的状态预测选择
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
