Differentiable Logics
The Theory Behind the Practice
Differentiable logics are the engine that powers this entire project. The idea: take a logical formula expressing a desired property (e.g., “the classifier is robust to small perturbations”) and interpret it as a differentiable function over real numbers. This function can then serve as a loss term during neural network training — the optimizer simultaneously fits the data and satisfies the logical specification.
But the theory is still young. Current differentiable logics have limitations in expressivity, numerical stability, and the guarantees they provide. Extending them is both a mathematical and an engineering challenge.
What You’ll Work On
This theme is for students who enjoy the interplay between theory and implementation. You’ll work on the foundations of differentiable logics and their realization in tools like Vehicle.
Possible thesis directions:
- New operators: Extend existing differentiable logic frameworks with quantifiers, induction principles, or recursion (building on Bacci & Mogelberg’s work on higher-order quantitative logic)
- Formalization: Contribute to the Coq/Rocq formalization of differentiable logics, ensuring mathematical correctness of the framework
- Tool development: Extend the Vehicle specification language to support new property types or improve its compilation to loss functions
- Benchmarking: Systematically compare different differentiable logics (Lukasiewicz, product, Goedel, DL2) on NIDS training tasks
What You’ll Learn
- Differentiable logics and quantitative semantics
- Proof assistants (Coq/Rocq) and formal verification
- The Vehicle specification language
- How theoretical advances translate into practical ML improvements
Project Results
property-driven-ml
A general open-source framework for property-driven machine learning: logical constraints over hyper-rectangle input regions are compiled into training loss terms through differentiable logics (Gödel, Łukasiewicz, Reichenbach, Yager, DL2, and Signal Temporal Logic), combined with PGD and Auto-PGD adversarial training. Gusts Grinbergs is a contributor to the framework, which is described in A General Framework for Property-Driven Machine Learning (Flinkow et al., 2025).
Signal Temporal Logic for Vehicle
An extension of the Vehicle specification language with Signal Temporal Logic operators (globally, finally, until) and closed-loop controller specifications, implemented as a built-in differentiable logic on top of STLCG++. Joint work by Alessandro Bruni, Matthew L. Daggitt, Gusts Gustavs Grīnbergs, and Ekaterina Komendantskaya; a paper on this work is to appear at LOPSTR+PPDP 2026.
Relevant Literature
- Taming Differentiable Logics with Coq Formalisation. Affeldt et al., ITP 2024
- A Foundation for Differentiable Logics using Dependent Type Theory. Affeldt, Bruni, Komendantskaya, Ślusarz, Stark, 2026
- Induction and Recursion Principles in a Higher-Order Quantitative Logic. Bacci & Mogelberg, 2025
- Propositional logics for the Lawvere quantale. Bacci et al.
- Polynomial Lawvere Logic. Bacci et al.
- The Vehicle language tutorial
Supervisors: Giorgio Bacci (AAU), Alessandro Bruni (ITU) – see Team