Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Guten Tag allerseits. Willkommen zur letzten Woche KI.

Ich bin gerade zurück von zwei Wochen Konferenzen über Formalisierung von Mathematik und alle

solchen Sachen und ich stelle es sich heraus, dass einige der Vorträge in diesen Konferenzen

darum gehen, wie man denn mit KI-Methoden Formalisierung von Mathematik, was ja ein

eigentlich sehr menschenorientiertes Verfahren ist, automatisieren kann.

Es werden durchaus da Machine Learning-Verfahren und Verfahren, auch so wie wir sie im Wesentlichen

hier gesehen haben, natürlich mit ein bisschen mehr Engineering dahinter, aber nicht mehr

sehr viel mehr dahinter, werden eingesetzt, um zum Beispiel sowas wie automatische Beweise

zu steuern.

Das sind Logikmaschinen, so wie wir sie gesehen haben in dpll.

Die müssen ja in dem Suchbaum irgendwie weiter kommen und da werden solche Verfahren benutzt.

Da werden Beweise angesetzt auf große Datenmengen und dann wird versucht, die zu lernen und

das stellt sich heraus, dass diese Heuristiken einigermaßen lernbar sind und dass man meistens

sowas wie zwischen 30 und 40 Prozent mehr Beweise rauskriegt als ohne Strategie lernen.

Das war jetzt gerade so eine Sache, wo diese ganzen Sachen, die wir jetzt hier gemacht

haben, mir mal wieder über den Weg gelaufen sind.

Es gibt natürlich jede Menge andere Anwendungen.

In der letzten Woche ist die Neural Nets Challenge gelaufen.

Wer hat da von Ihnen mitgemacht?

Ich hätte schon eine Vermutung, dass das eine gute Korrelation sein würde zwischen den Leuten,

die hier sind und die da mitmachen.

Hat das alles gut geklappt?

Es geht ja noch bis morgen.

Es tut mir leid, ich habe mir das gar nicht angeguckt.

Ich war bis gestern Abend auf der Konferenz und bin erst heute Morgen wieder da.

Gut, wunderbar.

Dann hoffen wir mal, dass Sie alle gewinnen.

Das werden Sie mit Sicherheit, wenn Sie mitmachen, denn man lernt eine ganze Menge.

Die Woche davor haben Sie einen kleinen, wohlverpackten Exkurs gesehen, wie man auch mit Logik lernen

kann.

In diesem Fall ist es etwas, was wir schon vorher erworben haben, irgendwie zu verpacken.

In Aussagen der Logik 1.

Stufe oder so.

Sodass man dann hinterher darauf aufbauend wieder darauf zugreifen kann und als eine

Möglichkeit vorhandenes Wissen in den Lernprozess einzuspeisen.

Wenn Sie sich überlegen, was wir vorher gemacht haben, diese Decision Trees, diese ganzen

statistischen Lernverfahren, die fingen immer an, das waren sogenannte Tabula rasa Methoden.

Das heißt, immer wenn man neue Beispiele sieht, fängt man wieder von Null an.

Das ist natürlich zumindest was menschliche Intelligenz oder auch weiteres Lernen angeht,

ist das natürlich nicht sehr erfolgreich.

Auch für die ganzen Verfahren, die wir jetzt hier auf die statistisch basiert sind, die

brauchen sehr viel Rechenzeit umzulernen.

Es wäre doch hübsch, wenn man das irgendwie inkrementell machen kann.

Eine Möglichkeit haben Sie gesehen, besonders wichtig da ist das sogenannte Interactive

Logic Programming.

Das ist also eine Sache, die tatsächlich in vielen Anwendungen benutzt wird.

In der Biologie oder so etwas werden diese Verfahren, insbesondere das Foilsystem wird

da eingesetzt und sind auch wohl konkurrenzlos im Wesentlichen.

Allerdings beschränkt man sich dabei sehr stark auf Situationen, die relativ gut mit