Wien - Was ist notwendig, um die Entwicklung von künstlicher Intelligenz voranzutreiben? Mehr Speicher und schnellere Prozessoren in den Computern werden nicht reichen. "Ein qualitativer Sprung ist nötig. Wir brauchen bessere Mechanismen in der Logik, um neue Begriffe zu generieren", antwortet Alexander Leitsch auf die Frage. "Wenn man der Maschine nicht sagt, was der Begriff der Primzahl bedeutet, wird sie sie nicht finden." Die Frage ist, wie wir Computer dazu bringen, Begriffe wie die Primzahl von selbst zu entdecken - etwas, was dem Denkvermögen und der Kreativität des Menschen vorbehalten ist.

Leitsch leitet die Arbeitsgruppe Theoretische Informatik und Logik am Institut für Computersprachen der TU Wien und ist einer der Pioniere im Bereich der computergestützten Logik in Wien. Österreichs einschlägige Forscherszene, die beim Vienna Summer of Logic ab Mittwoch gemeinsam mit Wissenschaftskollegen aus aller Welt vor den Vorhang tritt, hat in den vergangenen 30 Jahren eine international geachtete Position errungen. Eine ganze Reihe von Arbeitsgruppen arbeitet an den Fragen, die die von technischer Entwicklung geprägte Zeit an die Logik stellt. Fragen etwa im Bereich der Softwareverifikation, des automatischen Beweisens - oder eben der künstlichen Intelligenz.

Ein Theorem, verfasst in der Sprache der Prädikatenlogik, mag den meisten Menschen unverständlich und fremd erscheinen. Dabei ist es eigentlich eine Vereinfachung: "Wissen ist in den natürlichen Sprachen sehr kompliziert codiert. Daraus logische Schlüsse zu ziehen ist für Menschen leicht, für Maschinen aber sehr schwer." In Logiksprachen wie der Prädikatenlogik wird Wissen in eine strukturierte Form gebracht.

Automatisch generierte Beweise

Leitsch und seine Kollegen beschäftigen sich mit der Frage, wie man per Computer umfangreiche logische Beweise automatisch generieren und aus den Beweisen Informationen gewinnen kann. Für einen mathematischen Beweis, den seine Studenten in einer Viertelstunde lösen, benötigt der Computer immerhin weniger als eine Sekunde, so Leitsch. Für sehr komplizierte Beweise sei allerdings immer noch menschliche Kreativität erforderlich.

Einer der ersten logischen Beweise der Geschichte ist der Satz von Euklid, wonach es unendlich viele Primzahlen gibt. So wie in der Sprache der Logik derartige Aussagen bewiesen werden können, kann auch bewiesen werden, ob komplexe Hard- oder Software eines Computersystems ordnungsgemäß funktioniert. Automatische Verifikation oder formale Methoden nennen sich die entsprechenden Forschungsbereiche, mit denen sich etwa die Arbeitsgruppe von Helmut Veith am Institut für Informationssysteme der TU Wien beschäftigt.

Unter dem Namen Forsyte (Formal Methods in System Engineering) wird von Veith und Kollegen Software etwa auf sogenannte Heisenbugs, also schwer reproduzierbare, weil nicht konstant auftretende Fehler, durchsucht. Die Forscher erfassen zudem Programme in logischen Modellen, um die genaue Dauer der Ausführung und den Arbeitsspeicherverbrauch zu eruieren. Oder sie entwickeln automatische Verifikationsmethoden für fehlertolerante Algorithmen, also Programme, die etwa in Flugzeugen eingesetzt werden und die auch noch funktionieren sollen, wenn einzelne Prozessoren ausfallen.

Rechnen mit vielen Kernen

Veith ist auch Teil des vom Wissenschaftsfonds FWF finanzierten, österreichweiten Forschungsnetzwerks RISE (Rigorous systems engineering). Hier geht es darum, mithilfe der Logik von vornherein fehlerfreie Programme zu generieren. Beispielsweise haben Computer heute zumeist mehrere Rechenkerne, da die Geschwindigkeit der einzelnen Prozessoren kaum mehr erhöht werden kann. Die Aufteilung eines herkömmlichen Programms auf die Rechenkerne wollen die RISE-Forscher dem Computer überlassen. "Unsere Softwaretools sollen das Programm um schwierige Teile erweitern und für Systeme mit mehreren Rechenkernen übersetzen", sagt Veith.

"Ähnlich wie für die Planung eines Motors Differenzialgleichungen verwendet werden, verwenden wir die mathematische Logik, um Programme präzise zu beschreiben." Ein intensiver Dialog zwischen Logik und Computertechnik von Cloud-Computing bis Embedded Systems stehe im Vordergrund. Das Netzwerk aus Wissenschaftern von Universitäten in Graz, Linz und Salzburg sowie der TU Wien und dem IST Austria bildet auch die Bedeutung ab, die die Forschungsdisziplin mittlerweile in Österreich hat.

Die Logik als Luxus

Dass die Logik heute in Österreich wieder floriert, ist nicht selbstverständlich. Im Land von Ludwig Wittgenstein und Karl Popper blieb während der Naziherrschaft und der Jahrzehnte danach die Logik ein Luxus, den man sich nicht leistete. Im Land, in dem Kurt Gödel die wichtigsten Sätze der modernen Logik niederschrieb, wurde der Disziplin kein Raum mehr gegeben.

Erst in den 1980er-Jahren erwachte die moderne wissenschaftliche Logik in Wien wieder, vorerst in Form eines privaten Zirkels großteils autodidaktischer Interessierter. Einer der Einflussgeber war der in Österreich geborene Logiker Georg Kreisel, der Gödel persönlich gekannt hatte. "Wir haben bewusst an die Geschichte angeknüpft", sagt Leitsch, der damals neben Wissenschaftern wie Georg Gottlob oder Matthias Baaz zu der jungen Logikergeneration gehörte. 1987 resultierte aus dem priva- ten Zirkel die Kurt-Gödel-Gesellschaft, heute eine internationale Plattform zur Förderung von Logik, Philosophie und Mathematik und Veranstalter des Vienna Summer of Logic.

Spieltheorie löst Probleme

Der neuen Generation von Logikern ging es nicht mehr nur um die Grundlagen der Mathematik. In der Informatik fand sich ein Umfeld, das ihre Ansätze sehr gut gebrauchen konnte. Die schnell wachsenden Arbeitsgruppen bekamen Gewicht innerhalb der Computerwissenschaften. "Das, was die Mathematik für die Physik ist, ist die Logik für die Informatik", sagt Leitsch.

Auch am 2007 gegründeten IST Austria in Klosterneuburg wird Logik als Mittel der Programmverifikation ein wichtiger Stellenwert eingeräumt. Krishnendu Chatterjee, der neben IST-Leiter Thomas Henzinger eine Gruppe zu dem Thema leitet, verwendet unter anderem Ansätze der Spieltheorie, um spezielle Probleme der Logik zu lösen, die auch helfen, stabilere Computersysteme zu schaffen. Auch er forscht im Rahmen von RISE an effizienteren Analysetechniken. "Österreich ist zu einem guten Nährboden für Logik in Mitteleuropa geworden. Für mich ist es eine große Chance, Teil davon zu sein", sagt Chatterjee. (Alois Pumhösel, DER STANDARD, 9.7.2014)