一阶逻辑自动定理证明中公式嵌入的实验研究

一阶逻辑中的自动定理证明是一个活跃的研究领域，并成功地得到机器学习的支持。尽管已有各种将逻辑公式编码为数值向量的方案——从简单字符串到更复杂的基于图的嵌入——但人们对这些不同编码方式的比较知之甚少。本文中，我们研究并实验比较了当前系统中应用的基于模式的嵌入与流行的基于图的编码，其中大多数基于图的编码此前未在定理证明语境中被考虑过。我们的实验表明，更简单编码方案在运行时间上的优势被更复杂的基于图嵌入所超越，后者产生了更高效的搜索策略和更简单的证明。为支持这一点，我们跨多个定理证明器性能维度（不仅限于证明完成率）给出了详细分析，从而提供经验证据以帮助将神经引导定理证明的未来研究导向最有前景的方向。