Taming Differentiable Logics with Coq Formalisation

Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, Kathrin Stark

Research output: Contribution to conference - NOT published in proceeding or journalPaperResearch


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.
Original languageEnglish
Publication date21 Mar 2024
Publication statusPublished - 21 Mar 2024


  • Machine Learning
  • Differentiable Logics
  • Formal Verification
  • Mathematical Components
  • Coq Proof Assistant


Dive into the research topics of 'Taming Differentiable Logics with Coq Formalisation'. Together they form a unique fingerprint.

Cite this