Überblick

Eine "numerische" globale Optimierungsmethode mit Z3 Prover wird gezeigt.

Was ist Z3 Prover?

In etwa handelt es sich um einen MIT-lizenzierten Theorem-Zertifizierer von Microsoft Research.

https://github.com/Z3Prover/z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.

If you are not familiar with Z3, you can start here.

Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.

See the release notes for notes on various stable releases of Z3.

Der Charme von Z3

Selbst wenn ich bisher schreibe, glaube ich nicht, dass ich die Bedeutung von Z3 verstehen kann, deshalb möchte ich ein Beispiel geben.

Code

from z3 import *

x = Real("x")
y = Real("y")
c = Real("c")

s = Solver()

s.add(
    x > 0,
    y > 0,
    c > 0,
    c * c == 2.0,
    x*x + y*y == 1,
    y == -x + c
)

print s.check()
print s.model()

Ausgabeergebnis

$ python z3_test.py 
> sat
> [x = 0.7071067811?, c = 1.4142135623?, y = 0.7071067811?]

Das Wort "saß" kam heraus. Daraus ist ersichtlich, dass dieser logische Ausdruck der Einschränkung erfüllt werden kann. Dann wird die Kombination von Variablen ausgegeben, die diese Einschränkung erfüllt.

Das einfachste Beispiel ist c. c ist

c > 0
c * c == 2.0

Lösen Sie die Einschränkung von. ist was es liest. Von hier aus können Sie sehen, dass c = √2. Der Wert von s.model () ist ebenfalls 1.4142 ..., was zeigt, dass es korrekt ist. Es ist schneller, die Zahl für die Beziehung zwischen x und y zu sehen.

Dies ist das Problem, den Schnittpunkt des Einheitskreises und y = -x + c zu finden. Die Antwort ist sehr einfach und Sie können die Antwort als x = y = √2 / 2 sehen. (Sie können dem Ausgabeergebnis entnehmen, dass es auch numerisch korrekt ist.) Im Allgemeinen ist es für Menschen notwendig, über die Lösung nachzudenken, indem sie x * x + y * y = 1 durch y = -x + c ersetzen ... Es ist nicht nötig.

Aus dem Obigen können wir sehen, dass dieser Z3 drei wundervolle Punkte hat.

Kann Brüche handhaben
Kann Multiplikation und Division zwischen Variablen handhaben
Sie müssen die Formel nicht lösen, sondern nur die Randbedingungen schreiben.

Mit genau dem können Sie die meisten Dinge tun.

Globales Optimierungsverfahren mit Z3

Grundidee

Z3 selbst kann keine Werte optimieren. Gibt an, ob der angegebene logische Ausdruck erfüllt ist. Welchen Wert hat es, wenn es zufrieden ist? Das weiß ich nur. Achten Sie daher auf den Fehler zwischen dem Modell und den Daten. Wie weit kann der Fehler minimiert werden? Ich werde den Vorschlag lösen. Infolgedessen kann der maximale Fehler, dass der Satz nicht gelöst werden kann. Finden Sie den Wert des minimalen Fehlers, der den Satz durch Dichotomie lösen kann. Dies ermöglicht eine globale Optimierung mit Z3. Im folgenden Beispiel wird die Verwendung eines Modells erläutert, das 2x + 3 mit Rauschen von ax + b zurückgibt.

Testdatengenerierungsskript (data.py)

import sys
from random import gauss,seed

seed(0)
n = int(sys.argv[1])

for i in range(n):
    print i,gauss(2.0 * i + 3.0, 0.1)

Ausführungsverfahren

$python data.py 50 > data.csv

Globale Optimierung durch Residuum

Bereiten Sie die Daten vor
Definieren Sie Modellformel und Datenreste
Definieren Sie die Summe der Quadrate der Residuen (Delta)
Überprüfen Sie das Modell
Sei max_delta das in 4 erhaltene Delta.
Setzen Sie min_delta = 0.0
tmp_delta = (max_delta + min_delta) / 2
Definieren Sie Delta <max_delta
Wenn das Modell überprüft werden kann, setzen Sie max_delta = tmp_delta.
Wenn das Modell nicht überprüft werden kann, brechen Sie die Definition in 8. ab und setzen Sie min_delta = tmp_delta.
max_delta --min_delta <Beenden, wenn die gewünschte Genauigkeit erreicht ist. Wenn nicht, springen Sie zu 8.

from z3 import *

if __name__ == "__main__":
    data = map(lambda x:map(float,x.split()),open("data.csv")) # 1.

    s = Solver()
    a = Real("a")
    b = Real("b")
    delta = Real("delta")

    deltas = []
    for i,(x,y) in enumerate(data):
        d = Real("d%d"%i)
        deltas.append(d)
        s.add(
            d == y - ( a * x + b )  # 2.
        )
        s.check()

    s.add(delta == sum(d * d for d in deltas)) # 3.
    
    print s.check() # 4.
    print s.model()

    max_delta = float(s.model()[delta].as_decimal(15)[:-1]) # 5.
    min_delta = 0                                           # 6.

    while 1:
        tmp_delta = (max_delta + min_delta) / 2.0           #7.
        s.push()

        s.add( delta < tmp_delta )   # 8.

        if s.check() == sat: # 9.
            print "sat:",tmp_delta,min_delta,max_delta
            s.push()
            max_delta = tmp_delta
        else: # 10.
            print "unsat:",tmp_delta,min_delta,max_delta
            s.pop()
            min_delta = tmp_delta

        if max_delta - min_delta < 1.0e-6: # 11.
            break

    print s.check()
    model = s.model()
    
    print delta,model[delta].as_decimal(15)
    print a,model[a].as_decimal(15)
    print b,model[b].as_decimal(15)

Ergebnis

delta 0.604337347396090?
a 2.001667022705078?
b 2.963314133483435?

Sie können sehen, dass Zahlen nahe a = 2,0 und b = 3,0 erforderlich sind.

Globale Optimierung für den Umfangsbereich von Einzelfällen

Bereiten Sie die Daten vor
Definieren Sie epsilon> 0
Definieren Sie y --epsilon <= f (x) <= y + epsilon, wobei die Steuervariable (x), die Zielvariable (y) und das Modell je nach Fall der einzelnen Daten y = f (x) sind. ..
Überprüfen Sie das Modell
Sei max_epsilon das in 4 erhaltene Epsilon.
Setzen Sie min_epsilon = 0.0
tmp_epsilon = (max_epsilon + min_epsilon) / 2
Definieren Sie epsilon <max_epsilon
Wenn das Modell überprüft werden kann, setzen Sie max_epsilon = tmp_epsilon.
Wenn das Modell nicht überprüft werden kann, brechen Sie die Definition in 8. ab und setzen Sie min_epsilon = tmp_epsilon.
max_epsilon --min_epsilon <Beenden, wenn die gewünschte Genauigkeit erreicht ist. Wenn nicht, springen Sie zu 8.

from z3 import *

if __name__ == "__main__":
    data = map(lambda x:map(float,x.split()),open("data.csv")) # 1.

    s = Solver()
    a = Real("a")
    b = Real("b")
    epsilon = Real("epsilon")

    s.add(epsilon >= 0.0) # 2.

    for i,(x,y) in enumerate(data):
        s.add(
            y - epsilon <=  ( a * x + b ) , (a*x+b) <= y + epsilon # 3.
        )
        s.check() 

    print s.check() # 4.
    print s.model()

    max_epsilon = float(s.model()[epsilon].as_decimal(15)[:-1]) # 5.
    min_epsilon = 0 # 6.

    while 1:
        tmp_epsilon = (max_epsilon + min_epsilon) / 2.0 # 7.
        s.push()

        s.add( epsilon < tmp_epsilon ) # 8.

        if s.check() == sat: # 9.
            print "sat:",tmp_epsilon,min_epsilon,max_epsilon
            s.push()
            max_epsilon = tmp_epsilon
        else: # 10.
            print "unsat:",tmp_epsilon,min_epsilon,max_epsilon
            s.pop()
            min_epsilon = tmp_epsilon

        if max_epsilon - min_epsilon < 1.0e-6: # 11.
            break

    print s.check()
    model = s.model()
    
    print epsilon,model[epsilon].as_decimal(15)
    print a,model[a].as_decimal(15)
    print b,model[b].as_decimal(15)

Ergebnis

epsilon 0.223683885406060?
a 2.000628752115151?
b 3.006668013951515?

Sie können sehen, dass hier auch Zahlen nahe a = 2,0 und b = 3,0 erforderlich sind.

Welche Methode sollte verwendet werden

Letzteres ist "globale Optimierung für den Grenzbereich von Einzelfällen". Eins ist Geschwindigkeit. Ersteres dauert lange, um es einmal zu überprüfen. Dies ist wahrscheinlich eine interne Implementierung von Z3, daher kenne ich die Details nicht, aber es scheint, dass es einige Zeit dauert, da die Beziehung zwischen Delta und x, y eine starke Nichtlinearität aufweist. Andererseits haben epsilon und x, y eine schwache Nichtlinearität, so dass es nicht lange dauern wird. Das zweite ist die Leichtigkeit, die Rationalität des Modells zu beurteilen. Dies liegt daran, dass durch Hinzufügen einer Einschränkung wie "epsilon <spezifizierte Genauigkeit", wenn das Modell die spezifizierte Genauigkeit nicht erfüllt, es unsat wird, sodass die Erkennung eines fehlerhaften Modells schneller wird. Darüber hinaus gibt es noch weitere Vorteile, wenn Einschränkungen an erster Stelle stehen. Selbst wenn neue Daten hinzugefügt werden, ist die hier angegebene Genauigkeit garantiert, sodass die Verwendung sehr einfach ist. Die vorhandene Methode kann zur "globalen Optimierung durch Residuum" verwendet werden. Es ist eine Erklärung des Grades. Ersteres war für den Menschen nur einfach, mathematische Formeln zu organisieren, und ich denke, letzteres ist besser für die Verarbeitung mit Z3.

Diskussion der globalen Optimierung

Diese Methode ist keine globale Optimierung. Das könnte man denken. Halb Ja, halb Nein. Dies hängt von der Position ab, entweder von der Computerposition oder von der Mathematikposition. Ich denke, es gibt wahrscheinlich zwei Behauptungen. Einer ist der Fehlerpunkt. Zum Beispiel gibt es die Zahl √2. Dies wird mathematisch ausgedrückt, kann jedoch nicht auf einem allgemeinen Computer ausgedrückt werden. Computer können nur mit rationalen Zahlen umgehen. Daher gibt es normalerweise keine Möglichkeit, die Zahl √2 perfekt zu handhaben. Daher wird im Fall eines 64-Bit-Gleitkommas √2 angenähert und im Fehlerbereich von etwa 1e-15 behandelt. Daher gibt es auf dem Computer kein mathematisch genaues √2. Dies ist jedoch eine Geschichte, die mir persönlich egal ist. Unabhängig davon, wie oft Sie die Formeln manuell bis zum Limit organisieren und sie leicht lesbar machen, können Sie sie nicht programmgesteuert verwenden, es sei denn, Sie reduzieren sie auf numerische Werte. Daher muss der Fehler zwischen rationalen und irrationalen Zahlen oder mathematisch ausgedrückten numerischen Werten und auf einem Computer ausgedrückten numerischen Werten programmgesteuert zugelassen werden (sollte so eingerichtet sein, dass er zulässig ist). Bis jetzt habe ich keine andere Wahl, als es zu tolerieren, oder bis mir gesagt wurde, dass es nicht toleriert wurde, glaube ich nicht, dass es ein praktisches Problem gibt. Der zweite ist nicht offiziell. darüber. Wenn Sie sich den Titel ansehen, denken Sie wahrscheinlich an eine Formel für die Lösung einer quadratischen Gleichung. Es ist möglich, eine begrenzte Lösung in einem begrenzten Bereich numerischer Werte auf einer begrenzten mathematischen Formel zu finden. Ich denke, das ist die allgemeine Lösungsformel. Es ist eher ein Algorithmus, eher eine Prozedur als eine Formel. Da es unter der Annahme erstellt wurde, dass die Implementierung von Z3 Prover korrekt ist, weiß ich natürlich nicht, ob dieses Verfahren notwendigerweise zum richtigen Wert führt. Ich halte es jedoch für sinnvoll, anhand einiger Beispiele tatsächlich die optimale Lösung präsentieren zu können. Vielleicht hat diese Methode mathematisch viele unnatürliche Punkte, aber es scheint, dass es im praktischen Gebrauch in Bezug auf Computer kein besonderes Problem gibt. Daher wird es hier als "numerische" globale Optimierung ausgedrückt, nicht als "mathematische" globale Optimierung.

Attraktivität der globalen Optimierung durch Z3

Wie Sie dem Code entnehmen können, kann er nur durch Definieren der Formel optimiert werden. Ich denke, dass die schwierigen Punkte beim maschinellen Lernen "Formulierung mathematischer Formeln" und "Analyse mathematischer Formeln" sind. Ersteres kann bei einem Problem ziemlich reibungslos durchgeführt werden. Eine "Analyse mathematischer Formeln" ist jedoch auch als Menge erforderlich. Wie man den Gradienten der Zielfunktion berechnet ... Da der Gradient nicht berechnet werden kann, muss die Form der Zielfunktion geändert werden ... usw. Und es ist notwendig, die schlammige mathematische Formel selbst zu transformieren, was seit vielen Jahren ein schmerzhaftes Problem ist. Da ich jedoch die Optimierungsmethode für Z3 Prover entwickelt habe, frage ich mich, ob dies der richtige Zeitpunkt ist. Ich fühle mich so.

Unterschied zum Formelverarbeitungssystem

Berühmte mathematische Verarbeitungssysteme sind Mathematica, Maple, OSS ist Maxima und Minderjährige sind PySim und Sage. Ich habe Maxima selbst benutzt, war aber persönlich nicht zufrieden damit. Insbesondere gibt Maxima nach 3 Tagen Wartezeit keine fehlerhafte Antwort zurück, wenn der Umgang mit Ungleichheit schwach ist oder wenn zu komplizierte Ausdrücke eingegeben werden. Da war so etwas. Auch wenn eine Antwort zurückgegeben wurde, versuchte Maxima manchmal, sie mit einer mathematischen Formel zu behandeln, und gab eine unverständliche Antwort zurück. Als Programmierer interessiert mich die Wahrheit der Mathematik nicht und ich bin oft zufrieden, wenn nur die numerische Lösung einer bestimmten Formel angegeben wird. In diesem Sinne können Sie die Antwort zurückgeben, selbst wenn Sie eine komplizierte Formel eingeben, und Z3 mit Python-Bindung ist sehr dankbar. (Ich möchte nicht mehr schreiben, wie Maximas Formeln analysiert und in Programme konvertiert werden.)

Herausforderungen der globalen Optimierung mit Z3

Es ist sowieso langsam. Ich habe es mehrmals versucht, aber es kann schwierig sein. Ich habe dieses Z3 verwendet, um alle Variablen des neuronalen Netzwerks zu optimieren, aber manchmal kehrte es auch nach 3 Tagen nicht zurück. Darüber hinaus scheint es, dass es manchmal die Grenze der Expression von Brüchen durchbricht. In diesem Fall kann es mit einer Ausnahme sterben. Daher ist es oft unmöglich, das Modell zu überprüfen, wenn es zu viel getan wird, obwohl es möglich ist, eine nichtlineare globale Optimierung durchzuführen. Obwohl es sich möglicherweise in der Entwicklungsphase befindet, denke ich, dass es eine sehr attraktive Methode ist, da mathematische Formeln so wie sie sind in das Programm aufgenommen werden und der gesamte Bereich ohne Erlaubnis optimiert wird.

[PYTHON] Globale Allzweckoptimierung mit Z3