摘要

近年来，深度学习与自动定理证明相结合的进展主要集中在将逻辑公式作为输入嵌入深度学习系统。特别是，研究者们日益关注如何将具备结构感知能力的神经方法适配至逻辑表达式的底层图结构表示。尽管相较于字符级和词元级方法更具有效性，基于图的方法在表示上往往存在权衡，限制了其捕捉输入关键结构特性的能力。本文提出一种新颖的逻辑公式嵌入方法，旨在克服以往方法在表示能力上的局限。所提出的架构适用于不同表达能力的逻辑系统，例如一阶逻辑与高阶逻辑。我们在两个标准数据集上对方法进行了评估，结果表明，该架构在前提选择和证明步骤分类任务上均达到了当前最优的性能水平。