论文标题
一项用于自动定理的公式嵌入的实验研究，以一阶逻辑证明
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
论文作者
论文摘要
在一阶逻辑中证明的自动定理是一个活跃的研究领域，它得到了机器学习的成功支持。尽管有各种建议将逻辑公式编码为数值向量（从简单的字符串到更多涉及的基于图的嵌入），但对这些不同的编码如何比较知之甚少。在本文中，我们研究并在实验上比较了基于模式的嵌入，这些嵌入在具有流行的基于图的编码的当前系统中，其中大多数以前尚未在定理中得到证明的环境。我们的实验表明，基于图形的嵌入更加复杂，从运行时进行更简单的编码方案的优势会超过，从而产生更有效的搜索策略和更简单的证明。为了支持这一点，我们对定理私人绩效的几个维度进行了详细的分析，而不仅仅是证明完成率，从而提供了经验证据，以帮助指导未来的对神经引导定理的研究，以证明朝着最有前途的方向证明。
Automated theorem proving in first-order logic is an active research area which is successfully supported by machine learning. While there have been various proposals for encoding logical formulas into numerical vectors -- from simple strings to more involved graph-based embeddings -- little is known about how these different encodings compare. In this paper, we study and experimentally compare pattern-based embeddings that are applied in current systems with popular graph-based encodings, most of which have not been considered in the theorem proving context before. Our experiments show that the advantages of simpler encoding schemes in terms of runtime are outdone by more complex graph-based embeddings, which yield more efficient search strategies and simpler proofs. To support this, we present a detailed analysis across several dimensions of theorem prover performance beyond just proof completion rate, thus providing empirical evidence to help guide future research on neural-guided theorem proving towards the most promising directions.
