Quantifiers for Differentiable Logics in Rocq

Jairo Miguel Marulanda-Giraldo; Ekaterina Komendantskaya; Alessandro Bruni; Reynald Affeldt; Matteo Capucci; Enrico Marchioni

doi:10.1007/978-3-031-99991-8_12

Quantifiers for Differentiable Logics in Rocq

Jairo Miguel Marulanda-Giraldo^*
, Ekaterina Komendantskaya
, Alessandro Bruni
, Reynald Affeldt
, Matteo Capucci
, Enrico Marchioni

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The interpretation of logical expressions into loss functions has given rise to so-called differentiable logics. They function as a bridge between formal logic and machine learning, offering a novel approach for property-driven training. The added expressiveness of these logics comes at the price of a more intricate semantics for first-order quantifiers. To ease their integration into machine-learning backends, we explore how to formalize semantics for first-order differentiable logics using the Mathematical Components library in the Rocq proof assistant. We seek to give rigorous semantics for quantifiers, verify their properties with respect to other logical connectives, as well as prove the soundness and completeness of the resulting logics.

Original language	English
Title of host publication	AI Verification. SAIV 2025
Editors	Mirco Giacobbe, Anna Lukina
Publisher	Springer
Pages	227-237
Number of pages	11
ISBN (Electronic)	9783031999918
ISBN (Print)	9783031999901
DOIs	https://doi.org/10.1007/978-3-031-99991-8_12
Publication status	Published - 2026
Event	2nd International Symposium on AI Verification 2025 - Zagreb, Croatia Duration: 21 Jul 2025 → 22 Jul 2025

Publication series

Name	Lecture Notes in Computer Science
Volume	15947
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	2nd International Symposium on AI Verification 2025
Abbreviated title	SAIV 2025
Country/Territory	Croatia
City	Zagreb
Period	21/07/25 → 22/07/25

Keywords

Differentiable Logics
Formal Specifications
Interactive Theorem Proving
Loss Functions
Neural Network Verification

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-031-99991-8_12

Cite this

@inproceedings{e52ec1570e8b428baa3e1b9dc48f1fe7,

title = "Quantifiers for Differentiable Logics in Rocq",

abstract = "The interpretation of logical expressions into loss functions has given rise to so-called differentiable logics. They function as a bridge between formal logic and machine learning, offering a novel approach for property-driven training. The added expressiveness of these logics comes at the price of a more intricate semantics for first-order quantifiers. To ease their integration into machine-learning backends, we explore how to formalize semantics for first-order differentiable logics using the Mathematical Components library in the Rocq proof assistant. We seek to give rigorous semantics for quantifiers, verify their properties with respect to other logical connectives, as well as prove the soundness and completeness of the resulting logics.",

keywords = "Differentiable Logics, Formal Specifications, Interactive Theorem Proving, Loss Functions, Neural Network Verification",

author = "Marulanda-Giraldo, \{Jairo Miguel\} and Ekaterina Komendantskaya and Alessandro Bruni and Reynald Affeldt and Matteo Capucci and Enrico Marchioni",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.; 2nd International Symposium on AI Verification 2025, SAIV 2025 ; Conference date: 21-07-2025 Through 22-07-2025",

year = "2026",

doi = "10.1007/978-3-031-99991-8\_12",

language = "English",

isbn = "9783031999901",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "227--237",

editor = "Mirco Giacobbe and Anna Lukina",

booktitle = "AI Verification. SAIV 2025",

}

Marulanda-Giraldo, JM, Komendantskaya, E, Bruni, A, Affeldt, R, Capucci, M & Marchioni, E 2026, Quantifiers for Differentiable Logics in Rocq. in M Giacobbe & A Lukina (eds), AI Verification. SAIV 2025. Lecture Notes in Computer Science, vol. 15947, Springer, pp. 227-237, 2nd International Symposium on AI Verification 2025, Zagreb, Croatia, 21/07/25. https://doi.org/10.1007/978-3-031-99991-8_12

TY - GEN

T1 - Quantifiers for Differentiable Logics in Rocq

AU - Marulanda-Giraldo, Jairo Miguel

AU - Komendantskaya, Ekaterina

AU - Bruni, Alessandro

AU - Affeldt, Reynald

AU - Capucci, Matteo

AU - Marchioni, Enrico

N1 - Publisher Copyright: © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

PY - 2026

Y1 - 2026

N2 - The interpretation of logical expressions into loss functions has given rise to so-called differentiable logics. They function as a bridge between formal logic and machine learning, offering a novel approach for property-driven training. The added expressiveness of these logics comes at the price of a more intricate semantics for first-order quantifiers. To ease their integration into machine-learning backends, we explore how to formalize semantics for first-order differentiable logics using the Mathematical Components library in the Rocq proof assistant. We seek to give rigorous semantics for quantifiers, verify their properties with respect to other logical connectives, as well as prove the soundness and completeness of the resulting logics.

AB - The interpretation of logical expressions into loss functions has given rise to so-called differentiable logics. They function as a bridge between formal logic and machine learning, offering a novel approach for property-driven training. The added expressiveness of these logics comes at the price of a more intricate semantics for first-order quantifiers. To ease their integration into machine-learning backends, we explore how to formalize semantics for first-order differentiable logics using the Mathematical Components library in the Rocq proof assistant. We seek to give rigorous semantics for quantifiers, verify their properties with respect to other logical connectives, as well as prove the soundness and completeness of the resulting logics.

KW - Differentiable Logics

KW - Formal Specifications

KW - Interactive Theorem Proving

KW - Loss Functions

KW - Neural Network Verification

UR - https://www.scopus.com/pages/publications/105021385538

U2 - 10.1007/978-3-031-99991-8_12

DO - 10.1007/978-3-031-99991-8_12

M3 - Conference contribution

AN - SCOPUS:105021385538

SN - 9783031999901

T3 - Lecture Notes in Computer Science

SP - 227

EP - 237

BT - AI Verification. SAIV 2025

A2 - Giacobbe, Mirco

A2 - Lukina, Anna

PB - Springer

T2 - 2nd International Symposium on AI Verification 2025

Y2 - 21 July 2025 through 22 July 2025

ER -