[PYTHON] Construction d'un réseau neuronal qui reproduit XOR par Z3
Aperçu
En utilisant Z3 de SAT Solver fabriqué par Microsoft, nous allons construire un réseau neuronal qui reproduit les éléments logiques de base. Parallèlement à cela, nous montrons que XOR ne peut pas être reproduit avec un seul Perceptron. De plus, la configuration d'un réseau neuronal capable de reproduire XOR est présentée.
Articles Liés
Optimisation globale à usage général avec Z3 http://qiita.com/kotauchisunsun/items/90bce940a1c08ca1b7ae
Réseau de neurones à mettre en œuvre
Un réseau de neurones très simple gère un perceptron à 2 entrées et 1 sortie.
La sortie est
if w1 * i1 + w2 * i2 + b > 0:
return 1
else:
return 0
Code réel
Exécutez-le en utilisant le code suivant.
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)
Dans le cas de et
| i1 | i2 | production |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 1 | 0 |
| 1 | 0 | 0 |
| 1 | 1 | 1 |
Code à exécuter
$ 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]
Il s'est avéré que. Par conséquent, le réseau neuronal qui représente et est
w1 = 1
w2 = 1
b = -1
Il est représenté par.
En cas de ou
| i1 | i2 | production |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 1 |
Code à exécuter
$ 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]
Il s'est avéré que. Par conséquent, le réseau neuronal qui représente ou est
w1 = 1
w2 = 1
b = 0
Il est représenté par.
Pour nand
| i1 | i2 | production |
|---|---|---|
| 0 | 0 | 1 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 0 |
Code à exécuter
$ 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]
Il s'est avéré que. Par conséquent, le réseau neuronal qui représente nand est
w1 = -1
w2 = -1
b = 2
Il est représenté par. Maintenant que nous avons nand, nous savons que tout circuit logique peut être construit par un réseau neuronal.
Pour xor
| i1 | i2 | production |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 0 |
Code à exécuter
$ 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
Il était sorti comme insatisfait. A partir de là, il a été constaté que la construction de xor était impossible à partir d'un perceptron. C'est un problème causé par l'inséparabilité linéaire de la sortie de xor, qui est un problème bien connu dans la zone du réseau neuronal. On peut voir que cela a été confirmé en utilisant z3.
Construction de xor par un réseau de neurones à 2 étages
Considérez le réseau neuronal suivant. Il s'agit d'un réseau neuronal avec deux couches d'entrée et deux étages. Vérifiez si xor peut être construit en utilisant ce réseau neuronal.
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]
Par sat, il a été constaté que xor peut être reproduit avec le réseau neuronal illustré. La valeur à ce moment-là est
w1 = 1
w2 = 1
w3 = -1
w4 = -1
w5 = 1
w6 = 1
b1 = 0
b2 = 2
b3 = -1
Il se trouve que Considérant le réseau de neurones à partir de ce coefficient, Le réseau neuronal en haut à gauche est
w1 = 1
w2 = 1
b1 = 0
On voit qu'il est composé des coefficients. En conséquence, on peut voir que le réseau neuronal supérieur gauche est "OU".
Le réseau neuronal inférieur gauche
w3 = -1
w4 = -1
b2 = 2
On voit qu'il est composé des coefficients. En conséquence, on peut voir que le réseau neuronal en bas à gauche est "nand".
Le dernier bon réseau neuronal est
w5 = 1
w6 = 1
b3 = -1
On voit qu'il est composé des coefficients. En conséquence, on peut voir que le réseau neuronal en bas à gauche est "et".
Si la sortie est ici
out = (i1 or i2) and not (i1 and i2) Selon la loi de Domorgan 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) ici i1 and not i1 = false i2 and not i2 = false Alors out = (i1 and not i2) or (i2 and not i1) out = i1 xor i2
On peut voir à partir de cela que out est la sortie xor de i1 et i2. Par conséquent, on peut voir que la sortie xor pourrait être reproduite par Z3 avec un réseau neuronal à deux étages.
Résumé
Il a été montré par Z3 que et, ou, nand peut être construit et nand ne peut pas être construit avec un simple perceptron. Nous avons également montré que xor peut être construit avec un réseau de neurones à deux étages dans Z3. Nous avons également confirmé que le perceptron dans cette partie fonctionne de la même manière que et, ou, et nand, et montré que xor est également sorti de l'expression logique.
Recommended Posts