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.

Es gab viele “Warnzeichen” bevor Computer starke Schachspieler und bevor sie starke Gospieler wurden. Computer machten im Schach von 1976 bis 1998 stetigen Fortschritt von rund 100 Elo-Punkte pro Jahr, und sie machten stetigen Fortschritt in den Rankings der Internet-Go-Server. Wir haben bisher keine solche “Warnzeichen” aus der Mathematik bekommen. Wir können Berechnungen, Integration und kombinatorisches Teleskoping automatisieren, aber das führt nicht zu naheliegenden Verallgemeinerungen. Außerdem machen wir in der Mathematik viel mehr als Sätze zu beweisen.

Über den Stand der maschinellen Beweisverifikation hatten wir hier und hier mal geschrieben und zu von Computern aufgestellten mathematischen Vermutungen gibt es diese Webseite von Doron Zeilberger.

Kommentare (10)

  1. #1 Jan
    29. März 2016

    Selbst wenn es so weit kommen sollte (was meiner semi-fachkompetenten Meinung nach noch ein gutes Stück “den Fluss hinunter” liegt), dann ist dies kein Grund für Angst unter den Mathematikern, sondern fast ausschließlich für Hoffnung. Es wäre ein neues, äußerst mächtiges Werkzeug, eine Art Geschenk an die Zunft. Und es muss immer Leute geben, die mit den Theoremen und deren Beweisen umgehen und sie verstehen können. Eigentlich wäre es wie überall in der Automatisierungsgeschichte: Ein paar der althergebrachten Arbeiten fallen weg, dafür entstehen neue, die unter Umständen viel aufregender und spannender sind.

  2. #2 Gast
    29. März 2016

    Es besteht kein Grund, inPanik zu verfallen.
    Go zu spielen scheint mir für die Menschheit völlig irrelevant, ca. 1% spielen Go davon dann noch mal 1% einigermaßen gut.
    Ob die Fähigkeit eines Computers “besser” zu sein als ein menschlicher Mathematiker ebenfalls von dieser Irrelevanz ist, würde ich hier jetzt nicht zu behaupten wagen. Für mich als (Fast)Mathematiker gibt es Beweise, die ich in endlicher annehmbarer Zeit nicht nachvollziehen kann, weil sie sehr lang sind (>200 Seiten), weil sie ein extremes Spezialwissen voraussetzen (großer Fermat), oder mit Computerhilfe erstellt werden (4-Farbenproblem).
    Nach meiner Erfahrung als (Natur)Wissenschaftler besteht die Kunst darin, die Frage zu stellen, also das Problem zu formulieren. Dann finde ich auch immer einen gut ausgebildeten, hochbegabten Studenten/Absolventen, der mir dieses Problem lösen wird.
    Also zeige mir den Computer, der ein so einfach formuliertes, klar strukturiertes Spiel wie Go erfindet, oder der selber ein mathematisches Theorem formuliert, um es dann zu beweisen.

  3. #3 Dr. Webbaer
    29. März 2016

    Funktioniert Mathematik nicht so, dass auf Grund von Erfahrungen mit der Naturwelt Axiome aufgestellt werden und dann Sätze, die direkt von diesen ableitbar sind bzw. als Vermutung durch Rückführung auf die Axiomatik bewiesen werden (oder auch nicht bewiesen werden, dennoch vielleicht von besonderem Interesse bleiben)?
    Dass die Mathematik insofern eine Lehre über das Lernen ist und insofern “Key and Gate to the Sciences” (Bacon)?

    Wobei Brettspiele Spiele mit vollständiger Information sind und insofern sozusagen aus sich heraus minderkomplex und verschiedenen Formen der Berechnung vglw. gut zugänglich sind?
    Interessant vielleicht der Hinweis auf Poker, das noch vglw. schlecht gespielt wird von den Rechnern.
    Wobei aber auch Poker, wenn es von Rechnern geschlagen wäre, nichts über die Mathematik im hier gemeinten Sinne aussagen würde?

    MFG + weiterhin viel Erfolg,
    Dr. Webbaer

  4. #4 Gast
    29. März 2016

    Als eher Schach- denn Gospieler würde ich sagen, der Sinn von Schach besteht nicht darin gegen einen Computer zu spielen.
    Der Sinn von Fußball bestände nicht darin, gegen Roboter zu spielen.
    Der Sinn von AlphaGO besteht auch nicht darin Go zu spielen, sondern zu demonstrieren, wie man riesige komplexe Informationsmengen bündeln, analysieren und einer Zielfunktion zuführen kann.

  5. #5 schlappohr
    30. März 2016

    Abseits der Möglichkeiten und Gefahren hochintelligenter Computer gibt einen Aspekt, der mich ein wenig nachdenklich macht. Unsere Intelligenz ist das Resultat einer evolutionären Notwendigkeit. Wir haben uns zu dem entwickelt, was wir sind, weil wir so am besten überleben konnten. Mit den Maschinen fällt diese Notwendigkeit weg. Selbst wenn wir die ganzen Schreckensszenarien wie Skynet und Colossus einmal außer acht lassen, frage ich mich, welche Auswirkungen Maschinenintelligenz auf unsere evolutionäre Zukunft hat. Sicher können wir die Maschinen so programmieren, dass sie uns bedingungslos zu Diensten sind (Asimov’sche Robotergesetze), aber würden die Maschinen am Ende nicht einen Haufen degenerierter Schwachköpfe am Leben erhalten? Welchen Sinn hätte das?

  6. #6 Dr. Webbaer
    31. März 2016

    Sicher können wir die Maschinen so programmieren, dass sie uns bedingungslos zu Diensten sind (Asimov’sche Robotergesetze)

    Dies geht wohl nicht, zumindest nicht zuverlässig, zumindest nicht mit der eigentlich benötigten Zuverlässigkeit.
    Es sei denn diese Roboter wären menschen-ähnlich, sehr menschen-ähnlich und anhaltend unterwürfig.

    Nach einigem Überlegen scheint dieser Satz wichtig zu sein: ‘Im Grundsatz also eine klare Sache: es gibt keinen Grund, dass gerade die Mathematik von der maschinellen Dominanz verschont bleiben sollte.’
    Es müsste schon so sein, dass in einem klar begrenzten Bereich der Mathematik, der dann sozusagen als Spiel der Regression unterworfen werden könnte, bei der Topologie vielleicht?!
    >:->,
    Rechner Datenbanken mit Sätzen und Beweisen bereit stellen könnten.

  7. #7 Thilo
    17. Dezember 2017

    Alpha Math ist zwar noch nicht gekommen, dafür aber Alpha Zero, ein Schachprogramm, das mit 24 Stunden Lernen eine Spielstärke von mehr als 3500 Elo erreicht: https://arxiv.org/pdf/1712.01815.pdf

  8. […] AlphaGo ist natürlich das offensichtlichste Beispiel für das Leistungswachstum selbsttrainierender Maschinen. Auf Spiegel Online diskutiert Christian Stöcker den Nutzen, den solche künstlichen Intelligenzen auch bereits in relevanteren Bereichen haben, etwa beim Medikamentendesign. […]

  9. #9 uwe hauptschueler
    21. Mai 2018

    Wenn zwei oder mehr KI, kapitalistische vs. kommunistische KI z.B., zu einem Thema, mit dringenden Handlungsbedarf, unterschiedliche Empfehlungen vorlegen, ist man nicht schlauer als ohne KI.