迈向逻辑公式的可逆语义保持嵌入

逻辑是执行自动推理的主要形式语言，且至少对小型公式而言也是人类可解释语言。学习与优化逻辑需求与规则一直是人工智能中的重要问题。当前最先进的机器学习（ML）方法多基于连续空间中的梯度下降优化，而逻辑学习被框定在公式的离散语法空间中。利用连续优化学习逻辑属性是具挑战性的问题，需要将公式以有意义的方式（即保持语义）嵌入连续空间。现有方法能通过核方法（针对线性时序逻辑）构建有效的语义保持嵌入，但其定义的映射不可逆。本文解决该问题，借助基于图变分自编码器框架的深度架构学习如何反转此类嵌入。我们提出专为此设定设计的新模型，并通过广泛实验评估论证设计选择。在命题逻辑背景下报告的结果令人鼓舞，且指出并应对了关于公式可逆嵌入学习的若干挑战。