StartseiteMathlog

Die Macht der Maschinen

Von / 27. Januar 2018 / 16 Kommentare
Mehr

Algorithmen kontrollieren immer mehr, aber wer kontrolliert eigentlich die Algorithmen? Einen eher harmlosen(1) Aspekt dieses Themas diskutiert seit einigen Tagen die Frage- und Antwortseite mathoverflow: Proof assistent, cura te ipsum2

(1) nicht nur weil Beweisassistenten im Alltagsgeschäft der Mathematik noch keine große Rolle spielen
(2) dtsch.: “Beweisassistent, heile dich selbst”

Die Frage ist, wie man automatische Theorembeweiser gegen das irrtümliche Beweisen falscher Theoreme absichern kann; befriedigende Antworten scheint es bisher nicht zu geben.

Eine andere, komplementäre Frage, die bei mathoverflow auch gerade diskutiert wird, betrifft Proofs shown to be wrong after formalization with proof assistant.

Zwar sind die meisten bisher mit automatischen Theorembeweisern überprüften Lehrsätze eher klassische Sätze, deren Beweise schon Tausende Male von Mathematikern gelesen und verstanden wurden und wo man schon deswegen keine versteckten Fehler mehr finden wird. Aber es wurde jedenfalls bei der Computerüberprüfung des Beweises der Keplerschen Vermutung ein (korrigierbarer) Fehler gefunden und es gibt in den Antworten der mathoverflow-Frage den Bericht eines an computer-formalisierten Beweisen arbeitenden Doktoranden, der in anonymisierter Form von den zahlreichen Fehlern berichtet, die er dank seiner Arbeit in Lehrbüchern und Veröffentlichungen findet.
(Eine kuriose Geschichte in dem Zusammenhang: in einem von Kurt Gödel in seinen späten Jahren veröffentlichten Gottesbeweis fand 2013 ein automatischer Theorembeweiser eine bis dahin übersehene Inkonsistenz: The inconsistency in Gödel‘s ontological argument: a success story for AI in metaphysics.)

Jedenfalls scheint es einfacher zu sein, mit Computern Fehler in menschlichen Arbeiten zu finden, als Computer dazu zu bringen, Fehler in ihren eigenen Algorithmen aufzuspüren.

Stichworte: ,
Mehr

Kommentare (16)

  1. #1 Joseph Kuhn
    27. Januar 2018

    Dass die Computer eher Fehler bei anderen finden als bei sich selbst, macht sie fast ein bisschen menschlich 😉

  2. #2 rolak
    27. Januar 2018

    Och menno^^ Tante, der Joseph hat mir meine Idee und Förmchen geklaut!
    Da bekommt ‘KristallDetektor’ völlig neue semantische Bedeutungsfelder – der Compi, dein Seelenverwandter bei Splitter/Balken.

    Formale und vor allem automagische Sinnkontrolle bis Funktionsbeweise sind auch bei der Programmierung der heiße Shice (aktuellst-Bsp). Aktuell seit ich zurückdenken kann; ein ‘so muß dat’ beim Zuhören generierend; trotz gefühlter DauerAnkündigung erstaunlicherweise immer noch nicht am Markt durchgesetzt; es funktioniert zwar in Spezialfällen aber nicht unter so übertriebenen Randbedingungen wie ‘realistisch’.

    (Das war.. ein patentierter Universal-rant. Kann mit dezentem StichwortAustausch für schier alles verwendet werden: Kernfusion, gelispelte KI, <endless choices>, Frieden auf Erden)

  3. #3 Fan von kai
    27. Januar 2018

    Das ein Mathematiker AI nicht wirklich verstehen kann verwundert mich nicht. Es sind nicht Algorithmen, es sind Simulationen der Realität, die ihrerseits wiederum Verständnis und Erkenntnisgwinn liefern – klar, auch hier ist Logik und Mathematik der primäre Antrieb, aber eben nur dieser.
    Bleibt nur die Frage, wie derartige Simulationen in einem digitalen System implementiert werden sollen. Neuronale Netzwerke eignen sich dazu offenbar nur bedingt, und der Rest wird sicherlich hier nicht diskutiert – sollte es jemand können, sollte er am besten seine “genialen” Ideen nicht veröffentlichen, des lieben Geldes wegen.
    Aber das Stichwort ist ja schon gefallen, es sind Simulationen mit einer guter Prise Gedächtnis. Beides keine Kleinigkeit. Wer sich ernsthaft mit AI beschäftigt kommt aber nicht daran vorbei. Um es kurz zu machen, es geht um Verständnis der relevanten Aktionskomponenten und des Eigenständnisses der AI – Selbsteinordnung ist zwingend notwendig, aber was rede ich da, ist ja allen klar, oder doch nicht?
    Für sie Thilo, wie kann ein optimiertes Programm wunderbar Go spielen aber nicht die geringste Ahnung und Null Fähigkeit zum Erlernen von “Mensch ärgere Dich nicht” oder “Halma”, Poka usw haben – geschwieige vom Verhalten und Verständnis von Müttern mit Kinderwagen und einem Kleinkind in der Hand wobei sie noch über ein Smartphon telefoniert und so ganz nebenbei die Straße überqueren möchte?
    Tja, alles läuft auf Simulationen, Gedächtnis und Lernfähigkeit hinaus. Schöne Schlagworte, wer sie mit Leben füllen kann, der hat gewonnen – im warsten Sinne des Wortes 🙂

    BTW: Zu ihrer Frage bezüglich Algorithmen und ihrer Kontrolle. Sie könnten genau so gut die Frage stellen, wer kontrolliert die Moleküle in einer Zelle, oder für Puristen die Atome? Jetzt alles klar?

  4. #4 Dr. Webbaer
    27. Januar 2018

    Die Frage ist, wie man automatische Theorembeweiser gegen das irrtümliche Beweisen falscher Theoreme absichern kann; befriedigende Antworten scheint es bisher nicht zu geben.

    Darum geht’s, sofern die maschinelle Erarbeitung sogenannter mathematischer Beweise zukünftig eine wichtige Rolle spielen wird.
    Der Mathematiker bearbeitet dann die Beweis-Algorithmen, arbeitet sozusagen bevorzugt im “Meta”.
    Er bleibt vonnöten, was damit zusammenhängt, dass die Suche nach Erkenntnis, im Bereich der Mathematik ist sie tautologischer, also formaler Art, dem erkennenden Subjekt überlassen bleibt.
    (Solange die Maschine nicht zu einem demselben wird, haha.)

    Jedenfalls scheint es einfacher zu sein, mit Computern Fehler in menschlichen Arbeiten zu finden, als Computer dazu zu bringen, Fehler in ihren eigenen Algorithmen aufzuspüren.

    Muss nicht so sein, der Kick sozusagen besteht darin konkurrierende Beweis-Algorithmen an den Start zu bringen. Ist wohl auch i.p. AI schwer im Kommen, die Kompetitivität den Maschinen so beizufügen.

    MFG
    Dr. Webbaer

  5. #5 Dr. Webbaer
    27. Januar 2018

    @ Kommentatorenkollege ‘Fan von kai’ :

    Sie dürfen bis müssen zwischen der Welt und der “Formalwelt” bestmöglich unterscheiden.
    Die Mathematik ist Tautologie, ist zwar in ihren Regelmengen von der Realität (der “Sachlichkeit”) abhängig, von nichts kommt nichts, abär die Axiomatiken sind, erst einmal festgestellt, rein formal zu bearbeiten.

    Ansonsten, hier liegen Sie richtig, bearbeitet die AI nicht nur die Mathematik / Tautologie, sondern auch die “Realwelt”.

    MFG
    Dr. Webbaer

  6. #6 Dr. Webbaer
    27. Januar 2018

    Dass die Computer eher Fehler bei anderen finden als bei sich selbst, macht sie fast ein bisschen menschlich

    Sogenannte neuronale Netzwerke der Informationstechnologie bauen Kompetitivität nach, kennen auch die Entscheider-Funktionalität, sind insofern ‘menschlich’.
    Können auch irren.
    Was auch nicht so-o überraschend ist, wenn sie menschliches Werk zu sein haben.

  7. #7 rolak
    27. Januar 2018

    aber was rede ich da?

    Die Frage dürfte sich jeder stellen.
    Quite inbelievable that a luddite of sort should have survived…

  8. #8 rolak
    27. Januar 2018

    hmm, der tab war offensichtlich zu lange unerfrischt offen. Nochmal, diesmal mit Bezug:

    → aber was rede ich da?

    Die Frage dürfte sich jeder stellen.
    Quite inbelievable that a luddite of sort should have survived…

  9. #9 Dr. Webbaer
    27. Januar 2018

    ‘Of sorts’ ?

    Sportsfreund, wie Sie hier mit den Ludditen um die Ecke kommen, wird Ihrem Langzeit-Kommentatorenkollegen womöglich für immer unklar bleiben.
    Sie scheinen ein Trottel zu sein, Potential mag vorhanden sein, aber Sie belästigen mit Ihren indisponierten, indischponierten Kommentaren zunehmend, fällt Ihnen dies nicht auf?

    MFG + schönes Wochenende,
    Dr. Webbaer (der sich “Dümpfe” in der Regel nicht zur Brust nimmt, auch um nicht unnötig aufzuheizen, hier abär mal eine Ausnahme gemacht hat, tsk, tsk….)

  10. #10 Kai
    27. Januar 2018

    @Fan von kai: Wusste gar nicht das ich einen Fan habe =P Aber ich verstehe ehrlich gesagt nicht, was sie mit ihrem Beitrag ausdrücken wollen. Erstmal: AI ist nicht gleich AI. Es ist im Grunde genommen nur ein Buzzword unter dem jeder was anderes versteht. Hier geht es ja um Theorem-Beweiser. Das hat rein gar nichts mit neuronalen Netzen zu tun. Neuronale Netze wären hierfür auch denkbar ungeeignet. Mir ist auch nicht klar was sie mit ihrem “Simulationen der Realität” meinen. Neuronale Netze simulieren keine Realität und versuchen das auch gar nicht. Und mathematische Beweise haben mit “Realität” doch erstmal gar nichts zu tun (bzw. sind sie in ihrer eigenen, “mathematischen Realität” bzw. Axiomenwelt formuliert).

  11. #11 Dr. Webbaer
    28. Januar 2018

    @ Kommentatorenkollege ‘Kai’ :

    Erstmal: AI ist nicht gleich AI. Es ist im Grunde genommen nur ein Buzzword unter dem jeder was anderes versteht.

    +1
    Dies hängt auch damit zusammen, dass die Intelligenz, die vor ca. 100 Jahren konzeptualisiert worden ist, eine Art ‘Buzzword’ ist, wobei sie dies letztlich doch nicht ist, weil mit ihr sinnhaft wissenschaftlich gearbeitet werden kann, was mit Alternativen wie bspw. der ‘Klugkeit’, der ‘Weisheit’ oder der ‘Abgefeimtheit’ (“Bauernschläue”) nicht der Fall ist.

    Hier geht es ja um Theorem-Beweiser.

    Die sozusagen rechtwinklig, orthogonal oder logisch vorgehen und insofern nicht irren können.
    Oder?

    Das hat rein gar nichts mit neuronalen Netzen zu tun. Neuronale Netze wären hierfür auch denkbar ungeeignet.

    Vielleicht doch, denn, wenn ‘Theorem-Beweiser’ zu einem neuronalem Netzwerk zusammengeschlossen agieren, könnten sich, auf Basis der verwendeten Algorithmik, unterschiedliche Einschätzungen ergeben, den angestrebten mathematischen Beweis meinend.
    Dies hängt damit zusammen, dass die ‘Theorem-Beweiser’ selbst fehleranfällig sind.

    MFG
    Dr. Webbaer

  12. #12 Dr. Webbaer
    28. Januar 2018

    *
    Vielleicht doch [geeignet]

  13. #13 Frank
    Bellem
    28. Januar 2018

    Ich frage mich, was Kurt Gödel zu diesemThema zu sagen hätte…
    Oder ist das zu weit hergeholt?
    Grüße an alle Freunde dieses Blogs.

  14. #14 joselb
    1. Februar 2018

    Ui, Theorembeweiser. Bin zwar nur Informatiker in der Anwendungsentwicklung und kein Mathematiker. Trotzdem finde ich es ein hochinteressantes Feld. So hatte ich mal kurzzeitig mit coq rumgespielt und beschäftige mich seit einer Weile mit idris. Letzteres hat theoretisch das Potenzial von einem Werkzeug für die Beweisführung hinüber in die “normale” Softwareentwicklung zu wachsen, auch wenn leider die Infrastruktur noch recht klein ist.

    @Kai Übrigens würde ich die Verwendung von AI in Theorem-Beweisern nicht vollkommen ausschließen. Schließlich ist der Suchraum für Beweisstrategien gerade bei komplexen Problemen ziemlich groß. Und eine Speziallität von AI ist ja, große Räume auf kleinere abzubilden und dabei ist sie, wie man bei Go sehen kann, nicht nur nicht schlecht sondern hat auch noch einiges an Potenzial. Um das aber besser abzuschätzen hab ich von beidem noch zu wenig Ahnung.

  15. #15 erik||e oder wie auch immer . . . ..
    Bielefeld-Essenz
    1. Februar 2018

    . . . .. ich freue mich auf eine Welt ohne Lügen, ohne Falschheit . . . ..
    https://www.welt.de/mediathek/dokumentation/technik-und-wissen/sendung157940022/Erfindungen-fuer-die-Zukunft-Maschinen-zum-Gedankenlesen.html

    Wahrheit finde ich bereits überall um mich herum . . . ..
    https://scienceblogs.de/mathlog/2018/01/29/die-freie-welt-und-der-starke-dollar/

    . . . .. oder verwechsle ich Wahrhaftigkeit mit Höherer Wahrheit ? . . . .. oder Wahrheit mit RICHTIG ?

    . . .. Wie würde unser Universum funktionieren, wenn es RICHTIG funktionieren würde? Meine Antwort ist: Ein Universum ohne eine einzige Differenz von irgend etwas wäre ein RICHTIG im Sinne einer „Philosophie“ unseres Universums.
    . . . .. bis dahin muss es noch einen gewaltigen Weg gehen, mit einem Menschen oder mit etwas Anderem . . . ..

  16. #16 hmann
    9. Februar 2018

    joselb
    eigentlich ist in einem Computer alles festgelegt. Die Logigbaustein in der Harware, das Coputerprogramm, die Software. Wenn der Pragrammierer bzw. der Systemanalytiker einen Fehler macht, dann kann man ihn nicht finden, außer das Ergebnis wird sinnlos.
    Worum geht es also hier? Ohne ein konkretes Beispiel, bleibt alles im Ungewissen.