CISPA-Faculty Prof. Bernd Finkbeiner wird vom Europäischen Forschungsrat (European Research Council) mit einem ERC Advanced Grant ausgezeichnet.
Damit fließen in den kommenden Jahren rund 2,3 Millionen Euro Förderung in sein Projekt HYPER. Ziel des Projektes ist es, eine Spezifikationssprache zu entwickeln, mit der auch komplexe gesellschaftliche Konzepte wie Gerechtigkeit, Privatsphäre oder Erklärbarkeit mathematisch formalisiert werden können. Gelingt dem theoretischen Informatiker das, kann künftig automatisiert geprüft werden, ob Künstliche Intelligenz (KI) die geforderten Standards erfüllt. Bisher müssen dafür manuell schwierige Beweise von Expert:innen geführt werden. Bernd Finkbeiner will damit die mathematisch-logische Grundlage für weitere Diskussionen über Datenschutzstandards sowie die Gerechtigkeit und Erklärbarkeit von KI legen.
KI-Systeme halten uns so manches Mal auf unangenehme Art den Spiegel vor: Aus unserem Verhalten und den von uns produzierten Daten lernen sie, Entscheidungen zu treffen wie ein Mensch – und so fallen diese manchmal auch ebenso diskriminierend aus. Das zu verhindern und Gerechtigkeit bei der Entscheidungsfindung von KI zu garantieren, gehört zu den derzeit wohl größten Herausforderungen der Informatik. Ebenso treibt die Forschungsgemeinschaft um, wie die Entscheidungsfindung der Maschine erklärbar wird und wie personenbezogene Daten, mit denen die KI trainiert wird, geschützt werden können.
Doch wie lassen sich diese enormen Anforderungen in nachweisbare Eigenschaften von Computerprogrammen umwandeln? „Erklärbarkeit oder Gerechtigkeit sind keine wohldefinierten mathematischen Eigenschaften, sondern komplexe gesellschaftliche Konzepte. Unser Ziel ist nicht, ein für alle Mal zu definieren, was zum Beispiel Gerechtigkeit ist. Diese Frage hat riesige philosophische und gesellschaftliche Dimensionen. Wir wollen Forscher:innen und Entwickler:innen aber die Möglichkeit geben, präzise auszudrücken, was genau sie unter Fairness für ein spezifisches Programm verstehen. Nur zu sagen ‚es soll fair sein‘ lässt 1000 denkbare Interpretationen zu“, erklärt Bernd Finkbeiner.
Deshalb arbeitet der CISPA-Forscher im Projekt HYPER an einer Spezifikationssprache mit der genau das möglich ist. Spezifikationssprachen erlauben es, auf einer höheren Ebene ein Programm und das, was es können soll, zu beschreiben. So kann ein logisches und konsistentes Modell entwickelt werden, das später in Programmcode übersetzt wird.
Um Eigenschaften wie Erklärbarkeit, Gerechtigkeit und Privatsphäre so ausdrücken und beschreiben zu können, dass sie in unterschiedlichen Programmen eingebettet und mit verschiedenen Analysetechniken auch nachgewiesen werden können, fehlt es laut Bernd Finkbeiner bislang an einer vereinigenden Theorie. Grund dafür ist die Komplexität dieser Eigenschaften, die als Hypereigenschaften bezeichnet werden. „Sie sind sehr viel ausdrucksstärker als andere Eigenschaften, die traditionellerweise zur Beschreibung der Korrektheit und Zuverlässigkeit von Programmen verwendet werden, und können auch Beziehungen zwischen verschiedenen Situationen ausdrücken.“ Ein Beispiel: In einem Programm soll etwa der Grundsatz ‚Männer und Frauen werden gleichbehandelt‘ gelten. Dessen Einhaltung lässt sich nicht an isolierten Programmausführungen prüfen, sondern nur, wenn man alle Programmausführungen analysiert und miteinander vergleicht. Eine Programmausführung ist dabei die Reaktion des Programms auf eine Folge von Eingaben, wie sie ein Nutzer oder eine Nutzerin produzieren würde. „Bisherige Versuche, diese Eigenschaften in einer Spezifikationssprache für Softwaresysteme zu erfassen, waren nur für einen schmalen Ausschnitt des gesamten Spektrums von Hypereigenschaften erfolgreich“, sagt Bernd Finkbeiner.
Mit seinem Projekt soll sich das ändern. Ist die gemeinsame Spezifikationssprache dann gefunden, soll es im nächsten Projektschritt um die Entwicklung neuer Algorithmen gehen. Sie übernehmen das Monitoring, die Verifikation und die Synthese von Programmen. „Monitoring heißt, wir analysieren die Daten, die ein Programm produziert und prüfen, ob die gewünschten (Hyper-)Eigenschaften tatsächlich gelten oder verletzt werden. Verifikation bezeichnet das Finden von Problemen im Programmtext. Ein weiteres wichtiges Ziel ist die Synthese, also das automatisierte Erstellen eines Programmes, das nachweisbar die gewünschten Eigenschaften hat.“
So sei es letztlich auch möglich, den Erfolg des Projektes zu messen, indem die Forscher:innen die Methoden in reale Anwendungen einfließen lassen. „Meine Forschung kommt dann prinzipiell überall dort zum Einsatz, wo Menschen die Entscheidungsgewalt an Maschinen abgeben. Das umfasst vor allem alle autonomen Bereiche wie zum Beispiel selbstfahrende Fahrzeuge, unbemannte Drohnen, Bewerbungsmanagementsysteme, die über die Jobvergabe mitentscheiden und ähnliches“, erklärt der leitende Wissenschaftler.
Bernd Finkbeiner hat in der Vergangenheit bereits einen ERC Consolidator Grant erhalten. Den Advanced Grant erhalten erfahrene Forscher:innen mit bedeutenden Forschungsergebnissen in den vergangenen zehn Jahren. Für den Forscher ist das eine große Auszeichnung. „Der Advanced Grant gibt mir als Forscher die Möglichkeit, verwegene Ideen umzusetzen – auch mit dem Risiko zu scheitern. Die Förderung wird vor allem in Stellen für Nachwuchsforscher:innen fließen, die mich bei der Umsetzung des Projektes unterstützen.“
www.cispa.de
