Vor zwei Wochen hat Google’s ALphaGo Sedol Lee geschlagen und seitdem geht unter Mathematikern die (je nachdem) Angst oder Hoffnung um, dass Computer bald auch besser mathematische Theoreme finden und beweisen könnten als wir.
Diskutiert wird das auch auf MathOverflow, eigentlich die Seite für fachmathematische Fragen und Antworten, aber gelegentlich auch für Metadebatten. Dort wird also seit zwei Wochen diskutiert: What advantage humans have over computers in mathematics?
Viele der Antworten sind natürlich Allgemeinplätze und auch der Beitrag mit den meisten Pro- und Contrastimmen bleibt durchaus im Allgemeinen
Der Tag wird kommen, wo Computer nicht nur gute Mathematik machen, sondern sogar Mathematik, die (nicht-erweiterte) Menschen nicht mehr verstehen können. Das zu bestreiten ist verständlich, aber letztlich so kurzsichtig wie es war zu leugnen, dass Computer jemals beim Go gewinnen könnten.
Das ist nicht so deprimierend wie es klingen mag, denn wir Menschen müssen nicht zurückbleiben. Direkte Gehirn-Computer-Schnittstellen werden kommen und sogar die Unterscheidung zwischen ihnen wird verschwimmen.
Wir waren begeistert (“amazed”), als jemand eine Maschine baute, die schneller als ein Pferd reisen konnte, dann als eine Maschine uns in die Luft fliegen ließ und sogar auf den Mond, dann waren wir begeistert, dass Millionen von uns eine winzige Maschine bei sich führen können, die unsere Position auf dem Planeten innerhalb eines Meters bestimmt und uns mit jedem anderen auf dem Planeten unmittelbar sprechen läßt, und wieder, dass jemand eine Maschine erfindet, die neue Lebensformen kreiert. Aber die Idee, dass eine Maschine Mathematik tun könnte, das ist völlig unmöglich!
Im Grundsatz also eine klare Sache: es gibt keinen Grund, dass gerade die Mathematik von der maschinellen Dominanz verschont bleiben sollte.
Jenseits solch grundsätzlicher Diskussionen ist aber natürlich die Frage, ob mit einer solchen Entwicklung in absehbarer Zeit zu rechnen ist. Und da scheinen die Experten eher skeptisch. Douglas Zare zum Beispiel schreibt (meine Übersetzung):
Die speziellen Techniken, auf denen die Fortschritte beim Go beruhen, scheinen für die Mathematik nicht viel zu helfen. Wir mögen in der Zukunft einmal herausfinden können, wie wir Computer tiefe Theoreme beweisen lassen, die die Einführung neuer mathematischer Ideen erfordern, aber die meiste Arbeit dazu ist noch zu tun.
Neuronale Netze sind ziemlich gut bei Regressionsproblemen, und die meisten Spiele können als Regressionsprobleme aufgefasst werden. Dafür muss man mit einer guten Codierung der Spielsituationen als Vektoren kommen (sagen wir, als Elemente von [0,1]n oder {0,1}n) und dann sucht man eine Approximation zu einer [0,1]-wertigen Funktion dieser Vektoren. In einem Spiel sagen wir Dinge vorher wie die Wahrscheinlichkeit, von dieser Position aus mit perfektem Spiel oder randomisiertem starkem Spiel zu gewinnen.
Soweit ich weiß, haben wir keine gute Möglichkeit, eine mathematische Situation (zum Beispiel einen aufgeschriebenen partiellen Beweis) als Regressionsproblem zu kodieren. Wir könnten etwas wie ASCII verwenden, oder besser eine Codierung einer formalen mathematischen Sprache, aber von solch einer naive Darstellung erwartet man keine gute Performanz. Und dann, welchen Wert würden wir einer solchen Codierung zuweisen? Die Wahrscheinlichkeit, dass ein leicht randomisierter brillanter Mathematiker diesen Code innerhalb weniger Seiten zu einem korrekten Beweis vervollständigen kann? Es wäre schwierig, die Trainingsdaten zu evaluieren.
Es würde helfen, wenn wir eine riesige Datenbank gut geschriebener formaler Beweise bekommen könnten. Damit könnte ein neuronales Netz durch unbeaufsichtigtes Prätraining seine eigene interne Codierung finden. Doch während wir eine riesige Menge (Milliarden) von vernünftigen Spielpositionen schnell durch Spielen gegen sich selbst erzeugen könenn, ist es nicht klar, was das Analogon für mathematische Beweise sein sollte. Wenn man viele kleinere Variationen eines kurzen Beweises für den Satz des Pythagoras oder Beweise für triviale Fakten verwendet, würde das das neuronale Netz nicht darauf vorbereiten, eine mittellangen Beweis für Fermats kleinen Satz oder den Primzahlsatz zu finden, geschweige denn einen längeren Beweis einer offenen Frage.
Kommentare (10)