Taming Differentiable Logics with Coq Formalisation
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要