Standort: science.ORF.at / Meldung: "Die ersten Olympischen Spiele der Logik"

Olympische Ringe als Mengendiagramme

Die ersten Olympischen Spiele der Logik

An der Technischen Universität (TU) Wien geht es dieser Tage sportiv zu. Informatiker aus aller Welt treten bei den ersten Olympischen Spielen der Logik gegeneinander an. Die Disziplinen: automatisches Beweisen und Programmieren, Fehlersuche und Künstliche Intelligenz.

Informatik 04.07.2014

Die Wissenschaft ist bekanntlich ein kompetitives Gewerbe. In manchen Fächern hat der geistige Wettbewerb tatsächlich Turniercharakter. Etwa bei den Logikern und Informatikern: Sie treffen sich seit den 90ern alle vier Jahre zur "Federated Logic Conference".

Damals begannen Forscher ihre theoretischen Erkenntnisse gleich in die Praxis zu übersetzen, Probleme mit dem Computer zu lösen und diese Lösungen zu vergleichen. Und zwar in einem Wettbewerb. So entstanden Turniere für automatische Beweise, solche für Künstliche Intelligenz und dergleichen mehr - allerdings pflegten die Forscher außerhalb ihres angestammten Territoriums lange kaum Kontakt.

Die Zersplitterung des Faches war Moshe Vardi ein Dorn im Auge. Der israelisch-amerikanische Informatiker schlug vor ein paar Jahren vor, all diese Wettbewerbe zu einem Großturnier zusammenzufassen. Und weil sich die Logiker ohnehin alle vier Jahre trafen, um miteinander zu konferieren, nannte Vardi das Ganze "Olympische Spiele der Logik".

"Vienna Summer of Logic"

Neben der "Federated Logic Conference" und den Olympischen Spiele der Logik finden zwischen 9. und 24. Juli noch eine Reihe weiterer Konferenzen zum Thema Logik statt. 2.500 Forscher werden beim "Vienna Summer of Logic" erwartet - bisher die größte Veranstaltung in diesem Fachgebiet weltweit.

Mehr dazu in Logik-"Woodstock" im Juli in Wien

"Bei uns gibt es keine Haltungsnoten"

Die ersten Spiele dieser Art finden nun in Wien statt. Thomas Krennwallner von der TU Wien ist der Organisator des Turniers und kennt daher sämtliche Disziplinen, in denen Forscherteams (bzw. ihre Programme) gegeneinander antreten.

Manche agieren auf theoretischem Gelände, etwa jene, die sich am sogenannten P-NP-Problem abarbeiten: "Dabei geht es um die Frage, ob man komplexe Problemstellungen mit einem Computer in annehmbarer Zeit lösen kann, oder ob man im schlimmsten Fall sehr lange auf das Ergebnis warten muss", sagt Krennwallner.

Andere Programme versuchen, selbständig Fehler in Programmcodes zu erspähen, freilich gibt es auch Wettbewerbe, die stärker mit Alltagsfragen zusammenhängen. "Zum Beispiel die Erstellung eines idealen Stundeplans", so Krennwallner . "Wenn ich an der Uni die Zeiten von Vorlesungen festsetze, dann ist es von Vorteil, zusammenhängende Fächer an einem Tag, am besten hintereinander zu platzieren - und nicht willkürlich über die ganze Woche verteilt. Wenn aber Professor X nur am Dienstag Zeit hat und Professor Y nur Mittwoch bis Freitag, dann wird es kompliziert."

Kompliziert, aber in der Regel nicht unlösbar. Forscher aus dem Fachgebiet Künstliche Intelligenz füttern ihre Programme mit den Zielvorgaben, dann rasen die Elektronen durch die Prozessoren, bis die Maschine die besten Lösungen ausspuckt. Bewertet wird die Performanz nach zwei Kriterien: "Erstens die Geschwindigkeit und zweitens der Prozentsatz gelöster Probleme."

Und wie es sich für Informatiker gehört, werden diese Größen durch eine Formel in ein Punkteschema umgerechnet. "Das Ergebnis ist objektiv. Haltungsnoten wie beim Schispringen gibt es bei uns nicht", sagt der Wiener Informatiker.

Favoriten: "Gringo", "Waldmeister", "Lingeling"

Voraussetzung dafür ist allerdings, dass alle Teams ihre Programme vor dem Turnier bei den Organisatoren abgeben. Die Rechnungen laufen alle auf identen Computern in einem "Weißraum", der Einfluss von außen ist ausgeschlossen. Was die öffentliche Präsentation betrifft, haben sich die Techniker offenbar ein wenig von der Fußballweltmeisterschaft inspirieren lassen.

Medaille mit dem Konterfei Kurt Gödels

Münze Österreich AG

Für Olympiasieger: Kurt-Gödel-Medaille

Im großen TU-Hörsaal in der Gusshausstraße sowie im Freihaus in der Wiener Hauptstraße werden die Olympischen Spiele auf großen Bildschirmen übertragen, was zumindest bei Logik-Aficionados für gute Stimmung sorgen dürfte. Die favorisierten Programme tragen durchaus unakademische Namen. "Vampire" und "Waldmeister" haben gute Chancen beim automatischen Beweisen, von "Gringo" wird im Fach Künstliche Intelligenz ein starker Auftritt erwartet, hoch gehandelt wird auch ein Programm von der Uni Linz:

"Lingeling" hat bei den letzten "Satisfiability Competitions" abgeräumt, ob das auch diesmal der Fall ist, wird sich am 17. und 21. Juli herausstellen. An diesen Tagen findet die Kür der Sieger statt, Medaillenvergabe inklusive. Natürlich ist die Siegermedaille dem Genre entsprechend gestaltet. Ihrer Oberfläche wurde das Gesicht von Kurt Gödel eingeprägt, dem österreichischen Pionier der formalen Logik.

Detail für Feinspitze: Auf der Medaille ist auch eine Formel zu sehen. Sie stammt aus dem Unvollständigkeitssatz, ein Theorem mit historischer Sprengkraft: Darin bewies Gödel mit logischer Strenge, dass die Logik manchmal vor ihren eigenen Sätzen kapitulieren muss.

Robert Czepel, science.ORF.at

Mehr zu diesem Thema: