ENIGMA Anonymous：Symbol-Independent Inference Guiding Machine（系统描述）
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
摘要：
我们描述了一个实现的梯度提升和神经指导的饱和式自动定理证明，不依赖于一致的符号名称的问题。对于梯度提升指导，我们通过考虑公式的基于arity的编码来手动创建抽象特征。对于神经指导，我们使用符号无关的图神经网络（GNNs）及其嵌入的条款和条款。这两种方法在E prover及其ENIGMA学习指导框架中得到了有效的实现。为了提供有竞争力的实时性能的GNN，我们已经开发了一种新的基于上下文的方法来评估生成的条款在E。子句在较大的批次中联合评估，并且由GNN相对于大量已经选择的子句（上下文）进行评估，GNN在几轮消息传递中估计它们共同最有用的子集。这意味着GNN完成的近似推理循环与E内部完成的精确符号推理循环有效地交织。的MPTP大型理论基准的方法进行评估，并显示达到可比的实时性能，以最先进的符号为基础的方法。该方法还表现出很高的互补性，解决了大量的硬Mizar问题。
英文摘要：
We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems. For the gradient-boosting guidance, we manually create abstracted features by considering arity-based encodings of formulas. For the neural guidance, we use symbol-independent graph neural networks (GNNs) and their embedding of the terms and clauses. The two methods are efficiently implemented in the E prover and its ENIGMA learning-guided framework. To provide competitive real-time performance of the GNNs, we have developed a new context-based approach to evaluation of generated clauses in E. Clauses are evaluated jointly in larger batches and with respect to a large number of already selected clauses (context) by the GNN that estimates their collectively most useful subset in several rounds of message passing. This means that approximative inference rounds done by the GNN are efficiently interleaved with precise symbolic inference rounds done inside E. The methods are evaluated on the MPTP large-theory benchmark and shown to achieve comparable real-time performance to state-of-the-art symbol-based methods. The methods also show high complementarity, solving a large number of hard Mizar problems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
