Logic Tensor Networks (LTN)

Logic Tensor Network (LTN) is a neurosymbolic framework that supports querying, learning and reasoning with both rich data and rich abstract knowledge about the world. LTN uses a differentiable first-order logic language, called Real Logic, to incorporate data and logic. The figure below describes features of Real Logic.

LTN converts Real Logic formulas (e.g. ∀x(cat(x) → ∃y(partOf(x,y)∧tail(y)))) into TensorFlow computational graphs. Such formulas can express complex queries about the data, prior knowledge to satisfy during learning, statements to prove ... The next two figures describe how Real Logic sentences can represent computational graphs (inputs are on the left, outputs are on the right).

One can represent and effectively compute the most important tasks of deep learning. Examples of such tasks are classification, regression, clustering, or link prediction. The "Getting Started" section of the README links to tutorials and examples of LTN code.

[Paper] -- [Preprint]

Cite as:

@article{badreddine2022logic,
title = {Logic Tensor Networks},
journal = {Artificial Intelligence},
volume = {303},
pages = {103649},
year = {2022},
issn = {0004-3702},
doi = {https://doi.org/10.1016/j.artint.2021.103649},
author = {Samy Badreddine and Artur {d'Avila Garcez} and Luciano Serafini and Michael Spranger},
keywords = {Neurosymbolic AI, Deep learning and reasoning, Many-valued logics}
}

Installation

For the latest release version, install via pip. To install the core dependencies, run:

pip install ltn

If you need the dependencies used in the examples, run:

pip install ltn[examples]

For the latest development version, clone the github repository and install it locally (with or without dependency modifier).

pip install -e <local project path>

Repository structure

• ltn/core.py -- core system for defining constants, variables, predicates, functions and formulas,
• ltn/fuzzy_ops.py -- a collection of fuzzy logic operators defined using Tensorflow primitives,
• ltn/utils.py -- a collection of useful functions,
• tutorials/ -- tutorials to start with LTN,
• examples/ -- various problems approached using LTN,
• tests/ -- tests.

Getting Started

Tutorials

tutorials/ contains a walk-through of LTN. In order, the tutorials cover the following topics:

1. Grounding in LTN part 1: Real Logic, constants, predicates, functions, variables,
2. Grounding in LTN part 2: connectives and quantifiers (+ complement: choosing appropriate operators for learning),
3. Learning in LTN: using satisfiability of LTN formulas as a training objective,
4. Reasoning in LTN: measuring if a formula is the logical consequence of a knowledgebase.

The tutorials are implemented using jupyter notebooks.

Examples

examples/ contains a series of experiments. Their objective is to show how the language of Real Logic can be used to specify a number of tasks that involve learning from data and reasoning about logical knowledge. Examples of such tasks are: classification, regression, clustering, link prediction.

• The binary classification example illustrates in the simplest setting how to ground a binary classifier as a predicate in LTN, and how to feed batches of data during training,
• The multiclass classification examples (single-label, multi-label) illustrate how to ground predicates that can classify samples in several classes,
• The MNIST digit addition example showcases the power of a neurosymbolic approach in a classification task that only provides groundtruth for some final labels (result of the addition), where LTN is used to provide prior knowledge about intermediate labels (possible digits used in the addition),
• The regression example illustrates how to ground a regressor as a function symbol in LTN,
• The clustering example illustrates how LTN can solve a task using first-order constraints only, without any label being given through supervision,
• The Smokes Friends Cancer example is a classical link prediction problem of Statistical Relational Learning where LTN learns embeddings for individuals based on fuzzy groundtruths and first-order constraints.

The examples are presented with both jupyter notebooks and Python scripts.

License

This project is licensed under the MIT License - see the LICENSE file for details.

Acknowledgements

LTN has been developed thanks to active contributions and discussions with the following people (in alphabetical order):

• Alessandro Daniele (FBK)
• Artur d’Avila Garcez (City)
• Benedikt Wagner (City)
• Emile van Krieken (VU Amsterdam)
• Francesco Giannini (UniSiena)
• Giuseppe Marra (UniSiena)
• Ivan Donadello (FBK)
• Lucas Bechberger (UniOsnabruck)
• Luciano Serafini (FBK)
• Marco Gori (UniSiena)
• Michael Spranger (Sony AI)
• Michelangelo Diligenti (UniSiena)
• Samy Badreddine (Sony AI)