Differentiable logics (DL) have recently been proposed as a method of training neural networks to satisfy logical specifications. A DL consists of a syntax in which specifications are stated and an interpretation function that translates expressions in the syntax into loss functions. These loss functions can then be used during training with standard gradient descent algorithms. The variety of existing DLs and the differing levels of formality with which they are treated makes a systematic comparative study of their properties and implementations difficult. This paper remedies this problem by suggesting a meta-language for defining DLs that we call the Logic of Differentiable Logics, or LDL. Syntactically, it generalises the syntax of existing DLs to FOL, and for the first time introduces the formalism for reasoning about vectors and learners. Semantically, it introduces a general interpretation function that can be instantiated to define loss functions arising from different existing DLs. We use LDL to establish several theoretical properties of existing DLs, and to conduct their empirical study in neural network verification.

翻译：可微逻辑（DL）近年来被提出作为一种训练神经网络以满足逻辑规约的方法。DL包含一个用于陈述规约的语法体系，以及一个将语法表达式转化为损失函数的解释函数。这些损失函数随后可配合标准梯度下降算法用于训练过程。现有DL的多样性及其处理形式化程度的差异，导致难以系统性地比较研究它们的性质与实现。本文通过提出一种用于定义DL的元语言——称之为"可微逻辑的逻辑"（LDL）——来解决这一问题。在句法层面，它将现有DL的语法推广至一阶逻辑，并首次引入用于推理向量和学习者的形式化方法。在语义层面，它引入一个通用解释函数，该函数可通过实例化来定义源自不同现有DL的损失函数。我们利用LDL建立了若干现有DL的理论性质，并在神经网络验证中对其进行了实证研究。