For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among these methods, differentiable logics (DLs) are used to translate propositional or first-order formulae into loss functions deployed for optimisation in machine learning. At the same time, recent attempts to give programming language support for verification of neural networks showed that DLs can be used to compile verification properties to machine-learning backends. This situation is calling for stronger guarantees about the soundness of such compilers, the soundness and compositionality of DLs, and the differentiability and performance of the resulting loss functions. In this paper, we propose an approach to formalise existing DLs using the Mathematical Components library in the Coq proof assistant. Thanks to this formalisation, we are able to give uniform semantics to otherwise disparate DLs, give formal proofs to existing informal arguments, find errors in previous work, and provide formal proofs to missing conjectured properties. This work is meant as a stepping stone for the development of programming language support for verification of machine learning.

翻译：在机器学习性能与验证领域，近期涌现出优化学习系统以使其满足形式化逻辑属性的新方法。其中，可微逻辑（DLs）被用于将命题或一阶逻辑公式转化为优化过程中部署的损失函数。与此同时，近期为神经网络验证提供编程语言支持的尝试表明，可微逻辑可用于将验证属性编译至机器学习后端。这一现状要求我们为以下方面提供更强保障：此类编译器的可靠性、可微逻辑的可靠性与组合性，以及所生成损失函数的可微性与性能。本文提出一种方法，利用Coq证明助手中的数学组件库对现有可微逻辑进行形式化。借助该形式化，我们能够为原本分散的可微逻辑赋予统一语义，为现有非正式论证提供形式化证明，发现前人工作中的错误，并为缺失的猜想属性补全形式化证明。本工作旨在为机器学习验证的编程语言支持发展奠定基础。