Skip to content
GitLab
Commit 56f7612e authored by Pedot Nicola's avatar Pedot Nicola
Browse files

adds introduction notebook

parent a7a82f38
Expand all Hide whitespace changes
Inline Side-by-side
notebooks/.ipynb_checkpoints/db-reaparing-checkpoint.ipynb deleted 100644 → 0
View file @ a7a82f38
%% Cell type:markdown id: tags:
## Database Repair with Logic Tensor Networks
%% Cell type:markdown id: tags:
This is a basic example in which we use LTN for unsupervised in bringing out database population problems. We define a theory that encodes the following facts
* every person in the sample set should be assigned to a profile
* every person may be
* if two points are close, they should belong to the same cluster
We start setting loggin and importing required modules.
%% Cell type:code id: tags:
``` python
import logging; logging.basicConfig(level=logging.INFO)
import numpy as np
import tensorflow as tf
import logictensornetworks_wrapper as ltnw
```
%% Cell type:markdown id: tags:
One notably successful use of deep learning is embedding, a method used to represent discrete variables as continuous vectors.
Per each person, six people, we define a constant with embedding.
%% Cell type:code id: tags:
``` python
EMBEDDING_SIZE = 2
constants = list('abcdef')
print(constants)
for c in constants:
ltnw.constant(c,min_value=[0.]*EMBEDDING_SIZE,max_value=[1.]*EMBEDDING_SIZE)
```
%% Cell type:markdown id: tags:
We define a simple net as a sigmoid function of belonging.
%% Cell type:code id: tags:
``` python
def simple_net():
N = tf.Variable(tf.random_normal((EMBEDDING_SIZE, EMBEDDING_SIZE), stddev=0.1))
def net(x):
return tf.sigmoid(tf.reduce_sum(tf.multiply(tf.matmul(x,N),x),axis=1))
return net
```
%% Cell type:markdown id: tags:
We define a double net as a sigmoid over a variable with double embedding.
%% Cell type:code id: tags:
``` python
def double_net():
N = tf.Variable(tf.random_normal((EMBEDDING_SIZE*2, EMBEDDING_SIZE*2), stddev=0.1))
def net(x,y):
return tf.sigmoid(tf.reduce_sum(tf.multiply(tf.matmul(tf.concat([x,y],axis=1),N),tf.concat([x,y],axis=1)),axis=1))
return net
```
%% Cell type:markdown id: tags:
We define the theory using a number of predicates and variables.
* M for male people.
* S for married people.
* L for workers.
* P for our query predicate.
%% Cell type:code id: tags:
``` python
ltnw.predicate("M",EMBEDDING_SIZE,pred_definition=simple_net())
ltnw.predicate("S",EMBEDDING_SIZE,pred_definition=simple_net())
ltnw.predicate("L",EMBEDDING_SIZE,pred_definition=simple_net())
ltnw.predicate("P",EMBEDDING_SIZE*2,pred_definition=double_net())
```
%% Cell type:markdown id: tags:
We define our population.
%% Cell type:code id: tags:
``` python
ltnw.axiom('M(a)')
ltnw.axiom('~L(a)')
ltnw.axiom('S(a)')
ltnw.axiom('M(b)')
ltnw.axiom('L(b)')
ltnw.axiom('~S(b)')
ltnw.axiom('M(c)')
ltnw.axiom('L(c)')
ltnw.axiom('S(c)')
ltnw.axiom('M(d)')
ltnw.axiom('L(d)')
ltnw.axiom('~S(d)')
ltnw.axiom('~M(e)')
ltnw.axiom('~L(e)')
ltnw.axiom('~S(e)')
ltnw.axiom('~M(f)')
ltnw.axiom('~L(f)')
ltnw.axiom('S(f)')
```
%% Cell type:markdown id: tags:
Next we can define the theory using three variables.
%% Cell type:code id: tags:
``` python
ltnw.variable('x',tf.concat([ltnw.CONSTANTS[c] for c in constants],axis=0))
ltnw.variable('y',tf.concat([ltnw.CONSTANTS[c] for c in constants],axis=0))
ltnw.variable('z',tf.concat([ltnw.CONSTANTS[c] for c in constants],axis=0))
```
%% Cell type:markdown id: tags:
We define the equality for two individuals.
%% Cell type:code id: tags:
``` python
def smooth_eq(x,y):
return 1 - tf.truediv(tf.reduce_sum(tf.square(x - y), axis=1),
np.float32(EMBEDDING_SIZE)*tf.square(8.))
ltnw.predicate('eq',EMBEDDING_SIZE*2,
pred_definition=smooth_eq)
```
%% Cell type:markdown id: tags:
The relationships:
* married requires male.
* worker required male.
%% Cell type:code id: tags:
``` python
ltnw.axiom('forall x:(S(x) -> M(x))')
ltnw.axiom('forall x:(L(x) -> M(x))')
```
%% Cell type:markdown id: tags:
We define our query predicate:
* P is married.
* P is not married with his self.
* P is reflexive.
* P is intransitive.
%% Cell type:code id: tags:
``` python
ltnw.axiom('forall x:(S(x) % exists y:P(x,y))')
ltnw.axiom('forall x:~P(x,x)')
ltnw.axiom('forall x,y:(P(x,y) -> P(y,x))')
ltnw.axiom('forall x,y,z:(P(x,y) & P(x,z) -> eq(y,z))')
```
%% Cell type:markdown id: tags:
We train our knowledgbase model:
%% Cell type:code id: tags:
``` python
ltnw.initialize_knowledgebase(optimizer=tf.train.RMSPropOptimizer(learning_rate=.01),
initial_sat_level_threshold=.1)
sat_level=ltnw.train(track_sat_levels=100,sat_level_epsilon=.99,max_epochs=4000)
```
%% Cell type:markdown id: tags:
We ask our model if there are people not satisfing constrains:
%% Cell type:code id: tags:
``` python
print('L(x) -> M(x)',constants[np.where(ltnw.ask('L(x) -> M(x)') < .95)[0].squeeze()])
print('S(x) -> M(x)',constants[np.where(ltnw.ask('S(x) -> M(x)') < .95)[0].squeeze()])
```
%% Cell type:markdown id: tags:
L(x) -> M(x) []
S(x) -> M(x) f
%% Cell type:markdown id: tags:
We ask our model what the computed populations looks like:
%% Cell type:code id: tags:
``` python
for c in constants:
for p in ['L','S','M']:
print("{}({})".format(p,c),ltnw.ask("{}({})".format(p,c)))
print('L({}) -> M({})'.format(c,c),ltnw.ask('L({}) -> M({})'.format(c,c)))
print('S({}) -> M({})'.format(c,c),ltnw.ask('S({}) -> M({})'.format(c,c)))
```
%% Cell type:markdown id: tags:
L(a) [1.0207855e-06]
S(a) [1.]
M(a) [0.9999863]
L(a) -> M(a) [1.]
S(a) -> M(a) [0.9999863]
L(b) [1.]
S(b) [6.727357e-13]
M(b) [1.]
L(b) -> M(b) [1.]
S(b) -> M(b) [1.]
L(c) [0.99999976]
S(c) [1.]
M(c) [1.]
L(c) -> M(c) [1.]
S(c) -> M(c) [1.]
L(d) [1.]
S(d) [6.5612733e-13]
M(d) [1.]
L(d) -> M(d) [1.]
S(d) -> M(d) [1.]