Logic is the main formal language to perform automated reasoning, and it is further a human-interpretable language, at least for small formulae. Learning and optimising logic requirements and rules has always been an important problem in Artificial Intelligence. State of the art Machine Learning (ML) approaches are mostly based on gradient descent optimisation in continuous spaces, while learning logic is framed in the discrete syntactic space of formulae. Using continuous optimisation to learn logic properties is a challenging problem, requiring to embed formulae in a continuous space in a meaningful way, i.e. preserving the semantics. Current methods are able to construct effective semantic-preserving embeddings via kernel methods (for linear temporal logic), but the map they define is not invertible. In this work we address this problem, learning how to invert such an embedding leveraging deep architectures based on the Graph Variational Autoencoder framework. We propose a novel model specifically designed for this setting, justifying our design choices through an extensive experimental evaluation. Reported results in the context of propositional logic are promising, and several challenges regarding learning invertible embeddings of formulae are highlighted and addressed.

翻译：逻辑是执行自动推理的主要形式语言，并且（至少对于小型公式而言）它也是一种人类可解释的语言。学习与优化逻辑约束和规则一直是人工智能中的重要问题。最先进的机器学习方法主要基于连续空间中的梯度下降优化，而逻辑学习则被限定在公式的离散句法空间中。利用连续优化学习逻辑性质是一个具有挑战性的问题，要求以有意义的方式将公式嵌入到连续空间中，即保持其语义。现有方法能够通过核方法（用于线性时序逻辑）构建有效的语义保持嵌入，但它们所定义的映射不可逆。本文针对此问题展开研究，利用基于图变分自编码器框架的深度架构学习如何反转此类嵌入。我们提出了一种专门针对该场景设计的新型模型，并通过广泛的实验评估证明了设计选择的合理性。在命题逻辑语境中报告的结果令人鼓舞，同时我们强调并解决了关于学习公式可逆嵌入的数个挑战。