Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Comparing differentiable logics for learning with logical constraints

Thomas Flinkow, Barak A. Pearlmutter, Rosemary Monahan

TL;DR

This work investigates learning with background knowledge by comparing differentiable logics (DL2 and fuzzy logics) for enforcing logical constraints during neural network training. It advances the experimental methodology by incorporating counterexample generation via Projected Gradient Descent and adaptive loss balancing with GradNorm, enabling fairer comparisons and stronger constraint satisfaction. The study analyzes theoretical properties (shadow-lifting, Modus Ponens/Tollens, consistency) and empirically assesses how different operators affect learning and subsequent verification outcomes using Vehicle and Marabou. Results show that incorporating logical constraints generally improves constraint satisfaction and verifiable properties, though trade-offs with prediction accuracy and task-specific biases remain; the work highlights practical directions toward verifiable, constraint-guided learning and outlines paths to certified training and probabilistic extensions. Overall, the paper contributes a thorough framework for evaluating differentiable logics in learning with constraints and demonstrates their potential to support safer, corrective learning in autonomous and safety-critical systems.

Abstract

Extensive research on formal verification of machine learning systems indicates that learning from data alone often fails to capture underlying background knowledge, such as specifications implicitly available in the data. Various neural network verifiers have been developed to ensure that a machine-learnt model satisfies correctness and safety properties; however, they typically assume a trained network with fixed weights. A promising approach for creating machine learning models that inherently satisfy constraints after training is to encode background knowledge as explicit logical constraints that guide the learning process via so-called differentiable logics. In this paper, we experimentally compare and evaluate various logics from the literature, present our findings, and highlight open problems for future work. We evaluate differentiable logics with respect to their suitability in training, and use a neural network verifier to check their ability to establish formal guarantees. The complete source code for our experiments is available as an easy-to-use framework for training with differentiable logics at https://github.com/tflinkow/comparing-differentiable-logics.

Comparing differentiable logics for learning with logical constraints

TL;DR

This work investigates learning with background knowledge by comparing differentiable logics (DL2 and fuzzy logics) for enforcing logical constraints during neural network training. It advances the experimental methodology by incorporating counterexample generation via Projected Gradient Descent and adaptive loss balancing with GradNorm, enabling fairer comparisons and stronger constraint satisfaction. The study analyzes theoretical properties (shadow-lifting, Modus Ponens/Tollens, consistency) and empirically assesses how different operators affect learning and subsequent verification outcomes using Vehicle and Marabou. Results show that incorporating logical constraints generally improves constraint satisfaction and verifiable properties, though trade-offs with prediction accuracy and task-specific biases remain; the work highlights practical directions toward verifiable, constraint-guided learning and outlines paths to certified training and probabilistic extensions. Overall, the paper contributes a thorough framework for evaluating differentiable logics in learning with constraints and demonstrates their potential to support safer, corrective learning in autonomous and safety-critical systems.

Abstract

Extensive research on formal verification of machine learning systems indicates that learning from data alone often fails to capture underlying background knowledge, such as specifications implicitly available in the data. Various neural network verifiers have been developed to ensure that a machine-learnt model satisfies correctness and safety properties; however, they typically assume a trained network with fixed weights. A promising approach for creating machine learning models that inherently satisfy constraints after training is to encode background knowledge as explicit logical constraints that guide the learning process via so-called differentiable logics. In this paper, we experimentally compare and evaluate various logics from the literature, present our findings, and highlight open problems for future work. We evaluate differentiable logics with respect to their suitability in training, and use a neural network verifier to check their ability to establish formal guarantees. The complete source code for our experiments is available as an easy-to-use framework for training with differentiable logics at https://github.com/tflinkow/comparing-differentiable-logics.
Paper Structure (40 sections, 39 equations, 5 figures, 5 tables)

This paper contains 40 sections, 39 equations, 5 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Formal verification of neural networks
  3. Loss-based methods for guiding network training
  4. Our contributions
  5. Notation & definitions
  6. Background: DL2 and Fuzzy Logics
  7. Atomic terms
  8. Conjunction and disjunction
  9. Negation
  10. Implication
  11. Universal quantification
  12. Other operators
  13. Theoretical Comparison
  14. Shadow-lifting (derivatives of conjunction)
  15. Modus Ponens and Modus Tollens reasoning (derivatives of implication)
  16. ...and 25 more sections

Figures (5)

  • Figure 1: Example images from training with the $\mathsf{StandardRobustness}(\epsilon=0.4, \delta=0.1)$ constraint on MNIST showing an original image in \ref{['fig:img_input']}, a random sample from $\mathbb{B}(\boldsymbol{x};0.4)$ in \ref{['fig:img_random']}, and a constraint counterexample in \ref{['fig:img_pgd']}.
  • Figure 2: Results of training with the $\mathsf{StandardRobustness}$ constraint on MNIST in \ref{['fig:robustness_mnist']} and on Fashion-MNIST in \ref{['fig:robustness_fmnist']}.
  • Figure 3: The traffic sign groups for the Groups constraint on GTSRB stallkampGermanTrafficSign2011.
  • Figure 4: Results of training with the $\mathsf{Groups}(\epsilon=16/255, \delta=0.02)$ constraint on gtsrb.
  • Figure 5: Results of training with the $\mathsf{EvenOdd}$ constraint on MNIST in \ref{['fig:even-odd-mnist']} and of training with the $\mathsf{ClassSimilarity}$ on CIFAR-10 in \ref{['fig:class-similarity_cifar10']}.