DROPS

Artifact

Software

Formalisation of Differentiable Logics in Coq

Authors: Natalia Ślusarz, Reynald Affeldt, and Alessandro Bruni

Abstract

Cite as

Natalia Ślusarz, Reynald Affeldt, Alessandro Bruni. Formalisation of Differentiable Logics in Coq (Software, Source). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22503,
   title = {{Formalisation of Differentiable Logics in Coq}}, 
   author = {\'{S}lusarz, Natalia and Affeldt, Reynald and Bruni, Alessandro},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:bd213b761dfc453ccfe8e785a38cffe583c98f04;origin=https://github.com/ndslusarz/formal_LDL;visit=swh:1:snp:b2cb2b91dfa180cde7ca3a5ee8e013e02c3cbd5a;anchor=swh:1:rev:bd0e5eddeae0d264b736fdd1bbb9edd4e8fe1a99}{\texttt{swh:1:dir:bd213b761dfc453ccfe8e785a38cffe583c98f04}} (visited on 2024-11-28)},
   url = {https://github.com/ndslusarz/formal_LDL},
   doi = {10.4230/artifacts.22503},
}

Document

DOI: 10.4230/LIPIcs.ITP.2024.4

Taming Differentiable Logics with Coq Formalisation

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

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

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.

Cite as

Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, and Kathrin Stark. Taming Differentiable Logics with Coq Formalisation. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.4,
  author =	{Affeldt, Reynald and Bruni, Alessandro and Komendantskaya, Ekaterina and \'{S}lusarz, Natalia and Stark, Kathrin},
  title =	{{Taming Differentiable Logics with Coq Formalisation}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.4},
  URN =		{urn:nbn:de:0030-drops-207325},
  doi =		{10.4230/LIPIcs.ITP.2024.4},
  annote =	{Keywords: Machine Learning, Loss Functions, Differentiable Logics, Logic and Semantics, Interactive Theorem Proving}
}

Search Results

Documents authored by Ślusarz, Natalia

Formalisation of Differentiable Logics in Coq

Abstract

Cite as

Taming Differentiable Logics with Coq Formalisation

Abstract

Cite as

Thanks for your feedback!

Could not send message