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

image

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

i1 i2 output
0 0 0
0 1 0
1 0 0
1 1 1

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

i1 i2 output
0 0 0
0 1 1
1 0 1
1 1 1

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

i1 i2 output
0 0 1
0 1 1
1 0 1
1 1 0

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

i1 i2 output
0 0 0
0 1 1
1 0 1
1 1 0

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.

image

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.

Recommended Posts

Construction of a neural network that reproduces XOR by Z3
Let's summarize the basic functions of TensorFlow by creating a neural network that learns XOR gates
Implementation of a two-layer neural network 2
Do Neural Networks Dream of Electric Rats?
Guidelines for Output Layer Design of Neural Networks
Notes on neural networks
That of / etc / shadow
[PyTorch Tutorial ③] NEURAL NETWORKS
Construction of a neural network that reproduces XOR by Z3
A set of integers that satisfies ax + by = 1.
Visualize the inner layer of a neural network
Recognition of handwritten numbers by multi-layer neural network
The story of making a music generation neural network
Basics of PyTorch (2) -How to make a neural network-
Implementation of a convolutional neural network using only Numpy
Implement a 3-layer neural network
Create a web application that recognizes numbers with a neural network
Rank learning using neural network (Implementation of RankNet by Chainer)
I made a neural network generator that runs on FPGA
Understand the number of input / output parameters of a convolutional neural network
A story and its implementation that arbitrary a1 * a2 data can be represented by a 3-layer ReLU neural network with a1 and a2 intermediate neurons with an error of 0.
What is a Convolutional Neural Network?
[TensorFlow] [Keras] Neural network construction with Keras
Touch the object of the neural network
Build a classifier with a handwriting recognition rate of 99.2% with a TensorFlow convolutional neural network
Compose with a neural network! Run Magenta
Implementation of 3-layer neural network (no learning)
Implementation of "blurred" neural network using Chainer
[Chainer] Document classification by convolutional neural network
Implementation of a model that predicts the exchange rate (dollar-yen rate) by machine learning
A program that sends a fixed amount of mail at a specified time by Python