Differentiable Logics for Neural Network Training and Verification

TL;DR

This paper explores differentiable logics (DL) as a means to incorporate logical constraints into neural network training, aiming to improve verification by making the process differentiable and more effective.

Contribution

It analyzes the types of differentiable logics possible and evaluates their impact on continuous verification and training effectiveness.

Findings

Different DL choices influence training outcomes and verification success.

Certain DL formulations lead to more effective constraint satisfaction during training.

The paper provides criteria for evaluating desirable differentiable logics.

Abstract

The rising popularity of neural networks (NNs) in recent years and their increasing prevalence in real-world applications have drawn attention to the importance of their verification. While verification is known to be computationally difficult theoretically, many techniques have been proposed for solving it in practice. It has been observed in the literature that by default neural networks rarely satisfy logical constraints that we want to verify. A good course of action is to train the given NN to satisfy said constraint prior to verifying them. This idea is sometimes referred to as continuous verification, referring to the loop between training and verification. Usually training with constraints is implemented by specifying a translation for a given formal logic language into loss functions. These loss functions are then used to train neural networks. Because for training purposes these functions need to be differentiable, these translations are called differentiable logics (DL). This raises several research questions. What kind of differentiable logics are possible? What difference does a specific choice of DL make in the context of continuous verification? What are the desirable criteria for a DL viewed from the point of view of the resulting loss function? In this extended abstract we will discuss and answer these questions.