Zertifizierende Algorithmen auf der HLF-Eröffnungsveranstaltung

BLOG: Heidelberg Laureate Forum

Laureates of mathematics and computer science meet the next generation
Heidelberg Laureate Forum

Im Vergleich mit anderen Eröffnungsfeierlichkeiten war die des diesjährigen Heidelberg Laureate Forum recht kurzweilig. Natürlich muss es bei solcher Angelegenheit offizielle Worte von Vertretern wichtiger Partner und Unterstützer geben, wie der baden-württembergischen Wissenschaftsministerin Theresia Bauer, dem Rektor der Universität Heidelberg, Bernhard Eitel, und Heidelbergs Oberbürgermeister Eckart Würzner. Aber (a) die waren recht gut und informativ, (b) HLF  bündelte etliche davon in Interviews, geführt vom souveränen Moderator der Veranstaltung, Günter Ziegler und (c) war an geeigneter Stelle ein Fachvortrag eingeschoben, um die Angelegenheit aufzulockern.

© Heidelberg Laureate Forum Foundation / Flemming – 2017
Kurt Mehlhorn bei seinem Vortrag © Heidelberg Laureate Forum Foundation / Flemming – 2017

Der Vortrag von Kurt Mehlhorn vom Max-Planck-Institut für Informatik befasste sich mit zertifizierenden Algorithmen. Woher wissen wir, dass Software tatsächlich das tut, was sie tun soll? Dass sie die richtigen Berechnungen anstellt, die optimale Pärchenzusammenstellung für das Online-Dating findet, oder die richtige Entscheidung trifft, ob ein lineares Gleichungssystem gelöst werden kann oder nicht?

Wenn wir es nicht mit einem Programm zu tun hätten, sondern mit einem menschlichen Assistenten, würden wir jenen fragen: Wie sind Sie zu Ihrem Ergebnis gekommen? Können Sie das rechtfertigen? Wie sind sie vorgegangen? Ähnlich funktionieren zertifizierende Algorithmen. Die werden so geschrieben, dass sie nicht nur das Ergebnis, sondern auch ein “Zertifikat” bzw. einen “Zeugen” ausgeben, nämlich zusätzliche Informationen, die eine direkte Überprüfung der Richtigkeit erlauben. Ein einfaches Beispiel: Zusätzlich zur Berechnung des größten gemeinsamen Teilers g von zwei ganzen Zahlen berechnet der Algorithmus zwei zusätzliche ganze Zahlen, die einen direkten Test erlauben um festzustellen, dass g tatsächlich der größte  gemeinsame Teiler ist (sogenannter erweiterter euklidischer Algorithmus; dies und weitere Beispiele finden sich in diesem Aufsatz von Mehlhorn und Kollegen).

Ich persönlich hoffe auf ein Heidelberger Preisträgerforum, das nicht nur interessante Informationen liefert, sondern in diesem speziellen Sinne zertifizierend ist: mit Vorträgen und Diskussionen, die uns nicht nur sagen, was was ist, sondern die uns jene zusätzlichen Informationen liefern, die wir benötigen, um selbst nachzuvollziehen und zu prüfen, was uns da gesagt wird.

Avatar photo

Markus Pössel hatte bereits während des Physikstudiums an der Universität Hamburg gemerkt: Die Herausforderung, physikalische Themen so aufzuarbeiten und darzustellen, dass sie auch für Nichtphysiker verständlich werden, war für ihn mindestens ebenso interessant wie die eigentliche Forschungsarbeit. Nach seiner Promotion am Max-Planck-Institut für Gravitationsphysik (Albert-Einstein-Institut) in Potsdam blieb er dem Institut als "Outreach scientist" erhalten, war während des Einsteinjahres 2005 an verschiedenen Ausstellungsprojekten beteiligt und schuf das Webportal Einstein Online. Ende 2007 wechselte er für ein Jahr zum World Science Festival in New York. Seit Anfang 2009 ist er wissenschaftlicher Mitarbeiter am Max-Planck-Institut für Astronomie in Heidelberg, wo er das Haus der Astronomie leitet, ein Zentrum für astronomische Öffentlichkeits- und Bildungsarbeit, seit 2010 zudem Leiter der Öffentlichkeitsarbeit am Max-Planck-Institut für Astronomie und seit 2019 Direktor des am Haus der Astronomie ansässigen Office of Astronomy for Education der Internationalen Astronomischen Union. Jenseits seines "Day jobs" ist Pössel als Wissenschaftsautor sowie wissenschaftsjournalistisch unterwegs: hier auf den SciLogs, als Autor/Koautor mehrerer Bücher und vereinzelter Zeitungsartikel (zuletzt FAZ, Tagesspiegel) sowie mit Beiträgen für die Zeitschrift Sterne und Weltraum.

1 comment

  1. Zertifizierende Algorithmen waren wohl schon immer möglich, doch erst jetzt scheint die Idee aufzukommen, dass dies Sinn macht und sogar wichtig ist. Und tatsächlich: Wenn ein autonom fahrendes Fahrzeug einen Unfall verursacht, wäre es natürlich praktisch, wenn das Auto Auskunft geben könnte, warum es in der Unfallsituation gerade so – und nicht anders – gehandelt hat. Und tatsächlich spielt ja das in der Menschenwelt – vor Gericht beispielsweise -, eine Rolle, warum jemand auf eine bestimmte Art und Weise gehandelt hat. Es stellt sich aber immer wieder heraus, dass Menschen nicht alles begründen können, was sie tun und dass Begründungen nicht immer der Wahrheit entsprechen. Dummerweise gilt das auch für die gerade entstehende selbstlernende Software, die mit mehrlagigen neuronalen Netzen arbeitet und unter dem Namen Deep Learning firmiert. Auch sie kann teilweise erstaunliches leisten, aber kaum Auskunft darüber geben warum sie zu einem bestimmten Resultat kommt. Dabei muss es aber nicht bleiben – darf es nicht bleiben.
    Vor allem erstaunt mich, dass man erst jetzt auf die Idee der zertifizierenden Algorithmen kommt, denn das zugrundeliegende Problem ist schon recht alt: Missionskritische Software muss sich in jeder Situation berechenbar verhalten. Das gilt nicht nur für Raumfahrzeuge, sondern für jeden Autopiloten in jedem Flugzeug. Bis jetzt aber wurde in diesem Zusammenhang keine zertifizierenden Algorithmen eingesetzt, sondern es wurden andere Ansätze verfolgt wie beispielsweise der des verifizierten Algorithmus, eines Algorithmus, dessen Korrektheit (= gehorcht der Spezifikation) mit mathematischen Methoden bewiesen wurde. Solange es allerdings keine automatischen Beweiser für grössere Programme gibt, bedeutet die Verifizierung von Software einen ungeheueren Aufwand – einen Aufwand, der sich zudem nicht immer lohnt, vor allem dann nicht, wenn sich während der Entwicklung die Spezifikation wieder ändert. Der zertifizierende Algorithmus dagegen, aufgefasst als Algorithmus, der über sich selbst Auskunft gibt, entspricht viel stärker den Grundfähigkeiten des Menschen, die in der sprachlichen Kommunkation liegen. Im Grunde gibt es aber bereits eine simple Form von zertifizierenden Algorithmen in der konventionellen Software – in Form des Logging. Heute ist es verbreitet, dass Software Laufzeitdaten auf eine Datei schreibt, die bei Bedarf ausgewertet werden kann. Allerdings sind solche Loggingdaten meist auf einer sehr niedrigen Ebene. Der zertifizierende Algorithmus dagegen scheint auf der rationalen Ebene angesiedelt. Er gibt Auskunft über das Warum und nicht nur über das Wann und Wo.
    Wer weiss, vielleicht stehen wir mit zertifizierender Software am Beginn einer wichtigen Entwicklung in Richtung einer Technologie, die besser in die Menschenwelt integriert ist.

Leave a Reply


E-Mail-Benachrichtigung bei weiteren Kommentaren.
-- Auch möglich: Abo ohne Kommentar. +