Automatisierte Numerische Approximationen

Unsere Welt ist kontinuierlich und schwer vorherzusagen, aber unsere Computer arbeiten diskret und liefern präzise aussehende Ergebnisse. Diese grundlegende Diskrepanz macht Approximationen, also Annäherungen, notwendig: wissenschaftliche Simulationen physikalischer Prozesse können nur vereinfachte Modelle der Welt berücksichtigen; Datenanalysen arbeiten mit unvollständigen Daten und mit ungenauen Wahrscheinlichkeitsverteilungen; eingebettete Systeme können nur ein begrenztes Zeit- und Energiebudget verwenden, um Kontrollgrößen zu berechnen; Roboter müssen unklare Anweisungen von Menschen interpretieren; 3D-Drucker produzieren gezackte anstatt glatte Kanten. Das sind nur einige Beispiele für dieses Problem.

Jede Approximation bringt einen gewissen Fehler mit sich, das heißt die Computerprogramme berechnen nicht genau das, was wir gerne berechnen würden. In Anbetracht dessen, dass Approximierungen in vielen unserer Computersysteme zu finden sind, stellt sich die Frage: Sind diese Systeme sicher? Sind die berechneten Ergebnisse gut genug, sodass wir uns auf sie verlassen können? Überraschenderweise lautet die Antwort auf diese Fragen für die meisten Programme heute, dass wir es nicht wissen.

Computerprogramme und -systeme sind äußerst komplex, was die Auswirkungen einzelner Approximierungen unvorhersehbar macht. Ein Fehler, der am Anfang eines Programms eingeführt wird, kann im weiteren Verlauf kompensiert oder aber vergrößert werden. Darüber hinaus beeinflussen sich verschiedene Approximationen gegenseitig, was die Vorhersage noch komplizierter macht. Dadurch ist es praktisch unmöglich, manuell zu bestimmen, wie groß der Gesamtfehler am Ende eines Programms ist.

Bis vor kurzem haben rasante Fortschritte bei der Computerhardware es erlaubt, immer weniger Approximationen zu benutzen. Die Hardware ist in sehr kurzer Zeit immer schneller und energie-effizienter geworden (die Phänomene sind als Dennard's und Moore's Gesetze bekannt). Mit jeder Verbesserung konnte man die Approximationen und dadurch auch die so entstandenen Fehler reduzieren. Nun erreicht Computerhardware allerdings ihre physikalischen Grenzen, und auch der Energieverbrauch unserer Systeme wird immer mehr zu einem Problem. Dies führt dazu, dass Entwickler zunehmend Approximationen einführen, um Ressourcen zu sparen, und dies auch an Orten, an denen sie vorher nicht genutzt wurden.

Automatisierte Approximationen

Unsere Gruppe 'Automatisierte Verifikation und Approximation' am Max-Planck-Institut für Software Systeme entwickelt Methoden, um das Programmieren mit Approximationen einfacher, sicherer und die Programme selbst effizienter zu machen. Unser Ziel ist es, dass Programmentwickler nur das genaue Programm schreiben müssen, welches sie berechnen wollen: Sie sollten nicht über Approximationen nachdenken müssen. Diese werden dann automatisch von den von uns entwickelten Tools eingeführt, die zudem sicher stellen, dass die Programme korrekt und effizient funktionieren.

Angesichts der potenziell vielfältigen Menge an Approximationen und der damit verbundenen Fehler müssen unsere Methoden und Tools vor allem feststellen, wie groß der Gesamtfehler in einem Programm ist. Das heißt, sie müssen ermitteln, wie groß der Unterschied zwischen dem exakten Programm, welches der Nutzer haben möchte, und dem tatsächlich später implementierten ist. Da wir darüber hinaus nicht genau wissen, wie und wo das Programm genau verwendet wird, müssen unsere Tools den Gesamtfehler unter Berücksichtigung aller möglichen Umgebungen ermitteln.

Sobald wir eine solche automatisierte Verifizierungsmethode haben, können wir sie dazu verwenden, Approximationen automatisch einzuführen. Im einfachsten Fall könnten wir so viele Approximierungen ausprobieren, wie es uns in einer bestimmten Zeit möglich ist, und jede mit unserer Prüfmethode überprüfen. Da es im Allgemeinen zu viele verschiedene Möglichkeiten gibt, um diese in einer angemessen Zeit durchzugehen, konzentrieren wir unsere Suche auf bestimmte Kandidaten, die vielversprechend aussehen.

Approximationen von Numerischen Programmen

Eine der fundamentalsten Approximationen in Computersystemen sind Zahlen mit endlicher Genauigkeit. Die meisten wissenschaftlichen Theorien arbeiten mit reellen Zahlen, die unendlich präzise sind. Unsere digitalen Computer müssen jedoch mit einer begrenzten Anzahl an Bits arbeiten und können somit nur mit einer begrenzten Genauigkeit umgehen. Das bedeutet, dass jede Rechenoperation gerundet werden muss und daher immer einen kleinen Fehler einführt.

Wir haben unsere Methoden und Tools dazu verwendet, die Gesamtfehler, die durch diese endliche Arithmetik entstehen, zu berechnen. Unsere Tools ermitteln für Programme aus verschiedenen Bereichen wie maschinellem Lernen oder eingebetteten Systemen automatisch, wie viele Bits erforderlich sind, um eine gewisse Genauigkeit sicher zu stellen. Jedes Bit extra kostet Zeit und Energie, sodass die Reduzierung jedes einzelnen Bits dazu beiträgt, Ressourcen zu sparen.

Viele dieser numerischen Programme treffen auch Entscheidungen. Eine Fahrzeugsteuerung analysiert zuerst die Sensoreingabe, um zu bestimmen, ob zum Beispiel gebremst werden soll. Was passiert, wenn diese Berechnung fehlerhaft ist? Kann der Controller eine falsche Entscheidung treffen? In der Tat kann dies passieren, wird aber normalerweise im nächsten Schritt, wenn die Situation klarer ist, korrigiert. Allerdings sollten solche Fehlentscheidungen nicht zu oft passieren.

Unsere Methoden und Tools können die Wahrscheinlich berechnen, dass genau dies passiert, was wiederum einem Ingenieur hilft, das System anzupassen.