[PYTHON] Aufbau eines neuronalen Netzwerks, das XOR durch Z3 reproduziert
Überblick
Mit Z3 von SAT Solver von Microsoft werden wir ein neuronales Netzwerk aufbauen, das grundlegende logische Elemente reproduziert. Gleichzeitig zeigen wir, dass XOR nicht mit einem Perceptron reproduziert werden kann. Zusätzlich wird die Konfiguration eines neuronalen Netzwerks gezeigt, das XOR reproduzieren kann.
Zum Thema passende Artikel
Globale Allzweckoptimierung mit Z3 http://qiita.com/kotauchisunsun/items/90bce940a1c08ca1b7ae
Neuronales Netz zu implementieren
Ein sehr einfaches neuronales Netzwerk verarbeitet ein Perzeptron mit 2 Eingängen und 1 Ausgang.
Die Ausgabe ist
if w1 * i1 + w2 * i2 + b > 0:
return 1
else:
return 0
Tatsächlicher Code
Führen Sie es mit dem folgenden Code aus.
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)
Im Fall von und
| i1 | i2 | Ausgabe |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 1 | 0 |
| 1 | 0 | 0 |
| 1 | 1 | 1 |
Auszuführender Code
$ 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]
Es stellte sich heraus, dass. Daher das neuronale Netz, das darstellt und ist
w1 = 1
w2 = 1
b = -1
Es wird vertreten durch.
Im Falle von oder
| i1 | i2 | Ausgabe |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 1 |
Auszuführender Code
$ 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]
Es stellte sich heraus, dass. Daher das neuronale Netz, das darstellt oder ist
w1 = 1
w2 = 1
b = 0
Es wird vertreten durch.
Für nand
| i1 | i2 | Ausgabe |
|---|---|---|
| 0 | 0 | 1 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 0 |
Auszuführender Code
$ 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]
Es stellte sich heraus, dass. Daher ist das neuronale Netz, das nand darstellt,
w1 = -1
w2 = -1
b = 2
Es wird vertreten durch. Jetzt, wo wir nand haben, wissen wir, dass jede Logikschaltung durch ein neuronales Netzwerk aufgebaut werden kann.
Für xor
| i1 | i2 | Ausgabe |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 0 |
Auszuführender Code
$ 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
Es wurde als unsat ausgegeben. Daraus wurde herausgefunden, dass die Konstruktion von xor von einem Perzeptron aus unmöglich war. Dies ist ein Problem, das durch die lineare Untrennbarkeit der Ausgabe von xor verursacht wird, was ein bekanntes Problem im Bereich des neuronalen Netzes ist. Es ist ersichtlich, dass dies mit z3 bestätigt wurde.
Aufbau von xor durch ein zweistufiges neuronales Netzwerk
Betrachten Sie das folgende neuronale Netzwerk. Dies ist ein neuronales Netzwerk mit zwei Eingangsschichten und zwei Stufen. Überprüfen Sie, ob xor mithilfe dieses neuronalen Netzwerks erstellt werden kann.
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]
Durch sat wurde festgestellt, dass xor mit dem dargestellten neuronalen Netzwerk reproduziert werden kann. Der Wert zu diesem Zeitpunkt ist
w1 = 1
w2 = 1
w3 = -1
w4 = -1
w5 = 1
w6 = 1
b1 = 0
b2 = 2
b3 = -1
Es stellt sich heraus, dass Betrachtet man das neuronale Netz aus diesem Koeffizienten, Das neuronale Netzwerk oben links ist
w1 = 1
w2 = 1
b1 = 0
Es ist ersichtlich, dass es sich aus den Koeffizienten zusammensetzt. Infolgedessen ist ersichtlich, dass das obere linke neuronale Netzwerk "ODER" ist.
Das untere linke neuronale Netzwerk
w3 = -1
w4 = -1
b2 = 2
Es ist ersichtlich, dass es sich aus den Koeffizienten zusammensetzt. Infolgedessen ist ersichtlich, dass das neuronale Netzwerk unten links "nand" ist.
Das letzte rechte neuronale Netz ist
w5 = 1
w6 = 1
b3 = -1
Es ist ersichtlich, dass es sich aus den Koeffizienten zusammensetzt. Infolgedessen ist ersichtlich, dass das neuronale Netzwerk unten links "und" ist.
Wenn die Ausgabe hier draußen ist
out = (i1 or i2) and not (i1 and i2) Nach dem Gesetz von 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) Hier i1 and not i1 = false i2 and not i2 = false Damit out = (i1 and not i2) or (i2 and not i1) out = i1 xor i2
Daraus ist ersichtlich, dass out der xor-Ausgang von i1 und i2 ist. Daher ist ersichtlich, dass der xor-Ausgang von Z3 mit einem zweistufigen neuronalen Netzwerk reproduziert werden könnte.
Zusammenfassung
Z3 hat gezeigt, dass und oder oder nand konstruiert werden kann und nand nicht mit einem einfachen Perzeptron konstruiert werden kann. Wir haben auch gezeigt, dass xor mit einem zweistufigen neuronalen Netzwerk in Z3 konstruiert werden kann. Wir haben auch bestätigt, dass das Perzeptron in diesem Teil auf die gleiche Weise wie und, oder und und funktioniert, und haben gezeigt, dass xor auch vom logischen Ausdruck ausgegeben wird.
Recommended Posts