Differentiable Logics

Basics 

Vehicle’s loss function backend allows you to translate logical specifications into differentiable loss functions that can be used to train neural networks. This is achieved by using a Differentiable Logic which maps the Boolean operations such as and, or, not in the specification to real-valued operations.

A differentiable logic has the following type signature:

record DifferentiableTensorLogic where
  { trueElement               : Real
  , falseElement              : Real
  , pointwiseLessThan         : Tensor Real dims -> Tensor Real dims -> Tensor Real dims
  , pointwiseLessEqualThan    : Tensor Real dims -> Tensor Real dims -> Tensor Real dims
  , pointwiseGreaterThan      : Tensor Real dims -> Tensor Real dims -> Tensor Real dims
  , pointwiseGreaterEqualThan : Tensor Real dims -> Tensor Real dims -> Tensor Real dims
  , pointwiseEqual            : Tensor Real dims -> Tensor Real dims -> Tensor Real dims
  , pointwiseNotEqual         : Tensor Real dims -> Tensor Real dims -> Tensor Real dims
  , pointwiseNegation         : Tensor Real dims -> Tensor Real dims
  , pointwiseConjunction      : Tensor Real dims -> Tensor Real dims -> Tensor Real dims
  , pointwiseDisjunction      : Tensor Real dims -> Tensor Real dims -> Tensor Real dims
  , reduceConjunction         : Real -> Tensor Real dims -> Real
  , reduceDisjunction         : Real -> Tensor Real dims -> Real
  }

While Vehicle comes with several built-in differentiable logics, you can also define your own custom differentiable logic by implementing the DifferentiableTensorLogic interface.

For example:

CustomDL : DifferentiableTensorLogic
CustomDL =
  { trueElement                = 0
  , falseElement               = 1000000
  , pointwiseLessThan          = \{dims} x y -> max (const 0 dims) (x - y)
  , pointwiseLessEqualThan     = \{dims} x y -> max (const 0 dims) (x - y)
  , pointwiseGreaterThan       = \{dims} x y -> max (const 0 dims) (y - x)
  , pointwiseGreaterEqualThan  = \{dims} x y -> max (const 0 dims) (y - x)
  , pointwiseEqual             = \{dims} x y -> - (max (const 0 dims) (x - y) + max (const 0 dims) (y - x))
  , pointwiseNotEqual          = \{dims} x y -> (max (const 0 dims) (x - y) + max (const 0 dims) (y - x))
  , pointwiseNegation          = \{dims} x -> (const 1 dims) / x
  , pointwiseConjunction       = \x y -> x + y
  , pointwiseDisjunction       = \x y -> x * y
  , reduceConjunction          = \e xs -> reduceAdd e xs
  , reduceDisjunction          = \e xs -> reduceMul e xs
  }

Notes on the logic above:

Vehicle does not yet currently support infinite values, so we use a large constant to represent falsehood.
Strict and non-strict inequalities are treated the same in this logic, but you could define them differently if desired.

This custom logic can then be used in the loss function backend as described in Training with a specification.

Differentiable Logics

Basics

Basics 