[PYTHON] Construction of a neural network that reproduces XOR by Z3

Overview

Using Z3 of SAT Solver made by Microsoft, we will build a neural network that reproduces basic logic elements. Therefore, we show that XOR cannot be reproduced with one perceptron. In addition, the configuration of a neural network that can reproduce XOR is shown.

Related articles

General-purpose global optimization with Z3 http://qiita.com/kotauchisunsun/items/90bce940a1c08ca1b7ae

Neural network to implement

A very simple neural network handles perceptrons with 2 inputs and 1 output.

The output is

if w1 * i1 + w2 * i2 + b > 0:
    return 1
else:
    return 0

Actual code

Execute it using the following code.

nn_test.py:

#coding:utf-8
import sys
from z3 import *

def and_def(w1,w2,b,s):
    for i in [0,1]:
        for j in [0,1]:
            if i*j==1:
                ex = w1 * i + w2 * j + b > 0
            else:
                ex = w1 * i + w2 * j + b <= 0
            print ex
            s.add(ex)
            print s.check()
            print s.model()

def or_def(w1,w2,b,s):
    for i in [0,1]:
        for j in [0,1]:
            if i+j>0:
                ex = w1 * i + w2 * j + b > 0
            else:
                ex = w1 * i + w2 * j + b <= 0
            print ex
            s.add(ex)
            print s.check()
            print s.model()

def nand_def(w1,w2,b,s):
    for i in [0,1]:
        for j in [0,1]:
            if not i*j==1:
                ex = w1 * i + w2 * j + b > 0
            else:
                ex = w1 * i + w2 * j + b <= 0
            print ex
            s.add(ex)
            print s.check()
            print s.model()

def xor_def(w1,w2,b,s):
    for i in [0,1]:
        for j in [0,1]:
            if i+j==1:
                ex = w1 * i + w2 * j + b > 0.0
            else:
                ex = w1 * i + w2 * j + b <= 0.0
            print ex
            s.add(ex)
            print s.check()
            print s.model()

if __name__ == "__main__":
    i1 = Real('i1')
    i2 = Real('i2')

    w1 = Real('w1')
    w2 = Real('w2')
    b  = Real('b')

    out = Real('out')

    s = Solver()

    table = {
        "and"  : and_def,
        "or"   : or_def, 
        "nand" : nand_def,
        "xor"  : xor_def,
    }

    table[sys.argv[1]](w1,w2,b,s)

In the case of and

Code to execute

$ python nn_test.py and
> w1*0 + w2*0 + b <= 0
> sat
> [b = 0]
> w1*0 + w2*1 + b <= 0
> sat
> [w2 = 0, b = 0]
> w1*1 + w2*0 + b <= 0
> sat
> [w2 = 0, b = 0, w1 = 0]
> w1*1 + w2*1 + b > 0
> sat
> [w2 = 1, b = -1, w1 = 1]

It turned out that. Therefore, the neural network that represents and is

w1 = 1
w2 = 1
b = -1

It is represented by.

In case of or

Code to execute

$ python nn_test.py or
> w1*0 + w2*0 + b <= 0
> sat
> [b = 0]
> w1*0 + w2*1 + b > 0
> sat
> [w2 = 1, b = 0]
> w1*1 + w2*0 + b > 0
> sat
> [w2 = 1, b = 0, w1 = 1]
> w1*1 + w2*1 + b > 0
> sat
> [w2 = 1, b = 0, w1 = 1]

It turned out that. Therefore, the neural network that represents or is

w1 = 1
w2 = 1
b  = 0

It is represented by.

For nand

Code to execute

$ python nn_test.py nand
> w1*0 + w2*0 + b > 0
> sat
> [b = 1]
> w1*0 + w2*1 + b > 0
> sat
> [w2 = 0, b = 1]
> w1*1 + w2*0 + b > 0
> sat
> [w2 = 0, b = 1, w1 = 0]
> w1*1 + w2*1 + b <= 0
> sat
> [w2 = -1, b = 2, w1 = -1]

It turned out that. Therefore, the neural network that represents nand is

w1 = -1
w2 = -1
b  = 2

It is represented by. Now that we have nand, we know that any logic circuit can be constructed by a neural network.

For xor

Code to execute

$ python nn_test.py xor
w1*0 + w2*0 + b <= 0
sat
[b = 0]
w1*0 + w2*1 + b > 0
sat
[w2 = 1, b = 0]
w1*1 + w2*0 + b > 0
sat
[w2 = 1, b = 0, w1 = 1]
w1*1 + w2*1 + b <= 0
unsat
Traceback (most recent call last):
  File "nn_test.py", line 73, in <module>
    table[sys.argv[1]](w1,w2,b,s)
  File "nn_test.py", line 51, in xor_def
    print s.model()
  File "/usr/lib/python2.7/dist-packages/z3.py", line 6100, in model
    raise Z3Exception("model is not available")
z3types.Z3Exception: model is not available

It was output as unsat. From this, it was found that the construction of xor is impossible from one perceptron. This is a problem caused by the linear inseparability of the output of xor, which is a well-known problem in the neural network area. It can be seen that this was also confirmed using z3.

Construction of xor by 2-stage neural network

Consider the following neural network. This is a neural network with two input layers and two stages. Check if xor can be constructed by using this neural network.

xor_nn_test.py:

#coding:utf-8

from z3 import *

if __name__ == "__main__":

    w1 = Real('w1')
    w2 = Real('w2')
    w3 = Real('w3')
    w4 = Real('w4')
    w5 = Real('w5')
    w6 = Real('w6')
    
    b1  = Real('b1')
    b2  = Real('b2')
    b3  = Real('b3')

    s = Solver()

    for i in [0.0,1.0]:
        for j in [0.0,1.0]:

            print "-*-" * 10
            o1 = Real('o1%d%d'%(i,j))
            o2 = Real('o2%d%d'%(i,j))
            o3 = Real('o3%d%d'%(i,j))

            s.add(o1 == If(w1 * i + w2 * j + b1 > 0.0 , 1.0, 0.0))
            s.add(o2 == If(w3 * i + w4 * j + b2 > 0.0 , 1.0, 0.0))
            s.add(o3 == w5 * o1 + w6 * o2 + b3)
            
            if i+j==1:
                s.add(o3 > 0.0)
            else:
                s.add(o3 <= 0.0)
            print s.check()
            print s.model()

$ python xor_nn_test.py
> -*--*--*--*--*--*--*--*--*--*-
> sat
> [w5 = 0,
>  w6 = 0,
>  b3 = 0,
>  b2 = 1,
>  b1 = 1,
>  o300 = 0,
>  o200 = 1,
>  o100 = 1]
> -*--*--*--*--*--*--*--*--*--*-
> sat
> [o301 = 1,
>  w4 = 0,
>  o300 = 0,
>  o201 = 0,
>  o101 = 0,
>  b3 = 1,
>  b2 = 0,
>  o200 = 0,
>  w5 = -1,
>  w2 = -1,
>  o100 = 1,
>  w6 = 0,
>  b1 = 1]
> -*--*--*--*--*--*--*--*--*--*-
> sat
> [o301 = 1,
>  w3 = -1,
>  o300 = 0,
>  o101 = 1,
>  b2 = 1,
>  o200 = 1,
>  w5 = 1,
>  o310 = 1,
>  w6 = -1,
>  b1 = 0,
>  w4 = 0,
>  o201 = 1,
>  b3 = 1,
>  w2 = 1,
>  o110 = 0,
>  o100 = 0,
>  o210 = 0,
>  w1 = 0]
> -*--*--*--*--*--*--*--*--*--*-
> sat
> [o301 = 1,
>  w3 = -1,
>  o300 = 0,
>  o101 = 1,
>  b2 = 2,
>  o200 = 1,
>  w5 = 1,
>  o310 = 1,
>  w6 = 1,
>  b1 = 0,
>  w4 = -1,
>  o201 = 1,
>  o111 = 1,
>  b3 = -1,
>  w2 = 1,
>  o110 = 1,
>  o211 = 0,
>  o311 = 0,
>  o100 = 0,
>  o210 = 1,
>  w1 = 1]

By sat, it was found that xor can be reproduced with the illustrated neural network. The value at that time is

w1 = 1
w2 = 1
w3 = -1
w4 = -1
w5 = 1
w6 = 1
b1 = 0
b2 = 2
b3 = -1

It turns out that Considering the neural network from this coefficient, The neural network on the upper left is

w1 = 1
w2 = 1
b1 = 0

It can be seen that it is composed of the coefficients. As a result, it can be seen that the neural network on the upper left is "OR".

The neural network at the bottom left is

w3 = -1
w4 = -1
b2 = 2

It can be seen that it is composed of the coefficients. As a result, it can be seen that the neural network in the lower left is "nand".

The last neural network on the right

w5 = 1
w6 = 1
b3 = -1

It can be seen that it is composed of the coefficients. As a result, it can be seen that the neural network in the lower left is "and".

If the output is out here

out = (i1 or i2) and not (i1 and i2) According to De Morgan's laws out = (i1 or i2) and (not i1 or not i2) out = (i1 and not i1) or (i1 and not i2) or (i2 and not i1) or (i2 and not i2) here i1 and not i1 = false i2 and not i2 = false So out = (i1 and not i2) or (i2 and not i1) out = i1 xor i2

It can be seen from this that out is the xor output of i1 and i2. Therefore, it can be seen that the xor output could be reproduced by Z3 with a two-stage neural network.

Summary

It is shown that and, or, nand can be constructed by Z3 and nand cannot be constructed by a simple perceptron. We also showed that xor can be constructed with a two-stage neural network in Z3. We also confirmed that the perceptron in that part operates in the same way as and, or, and nand, and showed that xor is also output from the logical formula.