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

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

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

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

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.