Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Taming Differentiable Logics with Coq Formalisation

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

TL;DR

This work formalises differentiable logics (DLs) in Coq using the MathComp libraries to provide a uniform semantics and rigorous proofs of key DL properties. It encodes a generic LDL syntax and interpreters capable of supporting DLs such as Gödel, Łukasiewicz, Yager, product, DL2, and STL, and addresses core requirements like soundness, compositionality, and differentiability. The development yields new results (e.g., STL soundness under restricted conditions and complete shadow-lifting proofs for STL via L'Hôpital's rule) and uncovers concrete errors in prior literature, establishing a solid foundation for verified translation of logical properties into differentiable loss for property-guided training. By delivering a extensible, formally verified framework, the work enables certified compilation and verification workflows for neural-network properties and paves the way for future programming-language support in ML verification. The approach demonstrates the practicality of using Coq and MathComp for formalising state-of-the-art AI verification concepts and supports broader adoption of formal methods in ML tooling.

Abstract

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.

Taming Differentiable Logics with Coq Formalisation

TL;DR

This work formalises differentiable logics (DLs) in Coq using the MathComp libraries to provide a uniform semantics and rigorous proofs of key DL properties. It encodes a generic LDL syntax and interpreters capable of supporting DLs such as Gödel, Łukasiewicz, Yager, product, DL2, and STL, and addresses core requirements like soundness, compositionality, and differentiability. The development yields new results (e.g., STL soundness under restricted conditions and complete shadow-lifting proofs for STL via L'Hôpital's rule) and uncovers concrete errors in prior literature, establishing a solid foundation for verified translation of logical properties into differentiable loss for property-guided training. By delivering a extensible, formally verified framework, the work enables certified compilation and verification workflows for neural-network properties and paves the way for future programming-language support in ML verification. The approach demonstrates the practicality of using Coq and MathComp for formalising state-of-the-art AI verification concepts and supports broader adoption of formal methods in ML tooling.

Abstract

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.
Paper Structure (17 sections, 1 theorem, 9 equations, 4 figures, 3 tables)

This paper contains 17 sections, 1 theorem, 9 equations, 4 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Property-guided training, by means of an example
  4. Differentiable logics
  5. Properties of DLs
  6. An encoding of DLs in Coq
  7. Encoding of the syntax of types and expressions
  8. Encoding of the interpretation function
  9. Logical properties and soundness of DLs
  10. Logical properties of DLs
  11. Soundness of DLs
  12. Differentiability: shadow-lifting
  13. formalisation of shadow-lifting
  14. Shadow-lifting for DL2 and product
  15. formalisation of L'Hôpital's rule using MathComp-Analysis
  16. ...and 2 more sections

Key Result

Theorem 9

Let $f, g: {\mathbb R} \to {\mathbb R}$ be functions differentiable on an open interval $U$ except possibly at one point $a$. Suppose that $\forall x \in U$, $x\neq a$, we have $g'(x) \neq 0$. If it holds that $f(a)=g(a)=0$, then if $\lim\limits_{x \rightarrow a^+} \frac{f'(x)}{g'(x)} = l$ for some

Figures (4)

  • Figure 1: Types and expressions of LDL.
  • Figure 2: LDL syntax in Coq.
  • Figure 3: Excerpt of the semantics of STL: conjunction, negation, and comparison. (See Fig. \ref{['fig:semantics-lt0-gt0']} for intermediate definitions ssrstl_and_lt0 and ssrstl_and_gt0.)
  • Figure 4: Intermediate definitions to define the conjunction of STL. (The right subfigure reproduces part of Table \ref{['tab:semantics-math']} for reading convenience.)

Theorems & Definitions (9)

  • Example 1: Properties of neural networks
  • Example 2: Generating a loss function from a logical property fischer2019dl2
  • Example 3: Loss functions from properties in a fuzzy logic
  • Definition 4: Soundness
  • Definition 5: Commutativity, idempotence, and associativity of $\bigwedge\nolimits_M$
  • Definition 6: Shadow-lifting property varnai
  • Example 7: Discrepancies in pen and paper proofs
  • Example 8
  • Theorem 9: L'Hôpital's rule