Differentiable Logics are deployed in neuro-symbolic learning tasks as a way of embedding logical constraints in the training objective of neural networks. A differentiable logic consists of a syntax to write logical properties and a semantics to interpret them as real-valued functions to be folded in the loss function. A defining trade-off of the field is that between logical properties of the connectives, and analytic concerns for the semantics, with both aspects being relevant in applications. At one extreme we find fuzzy logics, that have well-established algebraic and proof-theoretic foundations, and at the other ad-hoc differentiable logics like Fischer's DL2, conceived for deep learning applications. However, no satisfactory foundation has emerged yet. We propose a resolution to this long-standing tension via a novel logic, Quantitative Linear Logic (QLL), with foundational ambitions. Our design is driven by naturality -- the idea that, since logical constraints are translated to losses, the semantics of the connectives should be pertinent operations used in ML practice (that is, sum and log-sum-exp) on additive quantities (like logits). We then judge the result on two aspects: logical adequacy -- that they satisfy most of the standard logical laws of Linear Logic; and empirical effectiveness -- test-time performance (as measured by adversarial attacks) is well-correlated to the actual verification of the logical constraints (as measured by off-the-shelf neural network verifiers), which makes QLL stand out among SoTA techniques.

翻译：可微逻辑被部署在神经符号学习任务中，作为将逻辑约束嵌入神经网络训练目标的一种方法。可微逻辑包含用于编写逻辑属性的语法，以及将其解释为实值函数（用于折叠到损失函数中）的语义。该领域的一个关键权衡在于逻辑连接词的逻辑属性与语义的分析问题之间，而这两个方面在实际应用中均具相关性。一极端是模糊逻辑，它具有完善的代数与证明理论基础；另一极端则是为深度学习应用而设计的专用可微逻辑（如Fischer的DL2）。然而，目前尚未出现令人满意的基础理论。我们提出通过一种具有基础性目标的新型逻辑——定量线性逻辑（QLL）——来解决这一长期存在的张力。我们的设计以自然性为驱动：由于逻辑约束被转化为损失，连接词的语义应成为机器学习实践中使用的相关运算（即对加性量如logits执行的求和与log-sum-exp操作）。随后，我们从两个维度评判结果：逻辑充分性——它们满足线性逻辑的大多数标准逻辑定律；以及经验有效性——测试时间性能（通过对抗攻击衡量）与实际逻辑约束的验证（通过现成神经网络验证器衡量）高度相关，这使得QLL在现有最先进技术中脱颖而出。