Extensive research on formal verification of machine learning (ML) systems indicates that learning from data alone often fails to capture underlying background knowledge. A variety of verifiers have been developed to ensure that a machine-learnt model satisfies correctness and safety properties, however, these verifiers typically assume a trained network with fixed weights. ML-enabled autonomous systems are required to not only detect incorrect predictions, but should also possess the ability to self-correct, continuously improving and adapting. A promising approach for creating ML models that inherently satisfy constraints is to encode background knowledge as logical constraints that guide the learning process via so-called differentiable logics. In this research preview, we compare and evaluate various logics from the literature in weakly-supervised contexts, presenting our findings and highlighting open problems for future work. Our experimental results are broadly consistent with results reported previously in literature; however, learning with differentiable logics introduces a new hyperparameter that is difficult to tune and has significant influence on the effectiveness of the logics.

翻译：关于机器学习系统形式化验证的大量研究表明，仅从数据中学习往往无法捕捉潜在的背景知识。为确保机器学习模型满足正确性和安全性属性，研究者已开发出多种验证器，但这些验证器通常假设训练好的网络具有固定权重。具备机器学习能力的自主系统不仅需要检测错误的预测，还应具备自我修正、持续改进和适应的能力。一种有望创建固有满足约束的机器学习模型的方法是将背景知识编码为逻辑约束，通过所谓的可微逻辑指导学习过程。在这项研究预览中，我们比较和评估了文献中在弱监督上下文中的多种逻辑，展示了我们的发现，并指出了未来研究中尚待解决的关键问题。我们的实验结果与先前文献报道的结果基本一致；然而，使用可微逻辑进行学习引入了一个难以调节的新超参数，该参数对逻辑的有效性有显著影响。