Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LTNtorch: PyTorch Implementation of Logic Tensor Networks

Tommaso Carraro, Luciano Serafini, Fabio Aiolli

TL;DR

LTNtorch is the fully documented and tested PyTorch implementation of Logic Tensor Networks and how LTNtorch implements it is presented, which provides a basic binary classification example.

Abstract

Logic Tensor Networks (LTN) is a Neuro-Symbolic framework that effectively incorporates deep learning and logical reasoning. In particular, LTN allows defining a logical knowledge base and using it as the objective of a neural model. This makes learning by logical reasoning possible as the parameters of the model are optimized by minimizing a loss function composed of a set of logical formulas expressing facts about the learning task. The framework learns via gradient-descent optimization. Fuzzy logic, a relaxation of classical logic permitting continuous truth values in the interval [0,1], makes this learning possible. Specifically, the training of an LTN consists of three steps. Firstly, (1) the training data is used to ground the formulas. Then, (2) the formulas are evaluated, and the loss function is computed. Lastly, (3) the gradients are back-propagated through the logical computational graph, and the weights of the neural model are changed so the knowledge base is maximally satisfied. LTNtorch is the fully documented and tested PyTorch implementation of Logic Tensor Networks. This paper presents the formalization of LTN and how LTNtorch implements it. Moreover, it provides a basic binary classification example.

LTNtorch: PyTorch Implementation of Logic Tensor Networks

TL;DR

LTNtorch is the fully documented and tested PyTorch implementation of Logic Tensor Networks and how LTNtorch implements it is presented, which provides a basic binary classification example.

Abstract

Logic Tensor Networks (LTN) is a Neuro-Symbolic framework that effectively incorporates deep learning and logical reasoning. In particular, LTN allows defining a logical knowledge base and using it as the objective of a neural model. This makes learning by logical reasoning possible as the parameters of the model are optimized by minimizing a loss function composed of a set of logical formulas expressing facts about the learning task. The framework learns via gradient-descent optimization. Fuzzy logic, a relaxation of classical logic permitting continuous truth values in the interval [0,1], makes this learning possible. Specifically, the training of an LTN consists of three steps. Firstly, (1) the training data is used to ground the formulas. Then, (2) the formulas are evaluated, and the loss function is computed. Lastly, (3) the gradients are back-propagated through the logical computational graph, and the weights of the neural model are changed so the knowledge base is maximally satisfied. LTNtorch is the fully documented and tested PyTorch implementation of Logic Tensor Networks. This paper presents the formalization of LTN and how LTNtorch implements it. Moreover, it provides a basic binary classification example.
Paper Structure (7 sections, 2 equations, 2 figures)

This paper contains 7 sections, 2 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Framework formalization
  3. LTN grounding
  4. LTN learning
  5. Binary classification in LTNtorch
  6. LTNtorch implementation
  7. Conclusions

Figures (2)

  • Figure 1: Step by step computation of $\forall x \exists y \operatorname{P}(x,y) \land \operatorname{Q}(y)$ in LTN. $(a)$ Variables $x$ and $y$ are grounded as sequences of 3 and 2 individuals, respectively. Note each individual (e.g., $x_1$) is a real-valued tensor whose dimensions are determined by the dataset (e.g., image, vector, or scalar). $(b)$ Computation of binary predicate $\operatorname{P}$. Each item in this grid is a truth value in $[0,1]$. Note how LTN organizes the output in two dimensions, one for $x$ and one for $y$. $\operatorname{P}(x_1,y_1)$ is the evaluation of $\operatorname{P}$ on $x_1$ and $y_1$. $(c)$ Computation of unary predicate $\operatorname{Q}$, similar to $\operatorname{P}$. $(d)$ Computation of $\land$ applying $\mathcal{G}(\land)$ element-wise. Note that broadcasting is used to match the dimensions of $\mathcal{G}(\operatorname{P}(x,y))$ and $\mathcal{G}(\operatorname{Q}(y))$ before applying element-wise multiplication. $(e)$ Computation of $\exists$ by aggregating $y$'s dimension using $\mathcal{G}(\exists)$. $(f)$ Computation of $\forall$ by aggregating $x$'s dimension using $\mathcal{G}(\forall)$.
  • Figure 2: Computational graph of the LTN for binary classification. Batch size for $\mathcal{B}_{dog}$ and $\mathcal{B}_{cat}$ is 3. Red arrows indicate how gradients are back-propagated through the logical structure to change the weights of predicate $\operatorname{Dog}$ so $\mathcal{K}$ is maximally satisfied. LTNtorch minimizes $1. - \mathcal{G}(\mathcal{K}) \equiv \mathcal{L}(\boldsymbol{\theta})$.