Wissen Sie noch - damals in der Schule? Die ebenso eleganten wie manchmal verwickelten, aber stets streng logisch aufeinanderfolgenden Schlußfolgerungs-Schritte, mit denen beispielsweise der Satz des Pythagoras oder auch der des Thales von Milet als allgemeingültiges Wissen festgeschrieben wurden? Es gibt sie heute in einer modernen Variante, die auch für die Informatik ausgesprochen interessante Perspektiven eröffnet.

Wenn Mathematiker lange Reihen logischer Schlußfolgerungen ausarbeiten, so sind das im Prinzip zwar keine anderen Gedankengebäude, als die lernend nachvollzogenen - Beweisketten aus der Schulzeit. Doch unterscheiden sie sich von jenen oft grundlegend, was ihren schieren Umfang betrifft: Denn wo die einen allenfalls winzige Modellbahn-Häuschen sind, da stellen die anderen sich als prächtige, stattliche Schlösser mit Hunderten von Kammern, Sälen und Gemächern dar. Entsprechend unüberschaubar, also schwer nachprüfbar, ist denn auch, was solche Beweisfolgen oft aussagen.

So dachte , beispielsweise schon 1879 ein gewisser Alfred Kempe, er hätte das bekannte Vierfarben-Problem der Geographen durch einen schlüssigen Beweis gelöst und mithin unwiderleglich demonstriert, daß tatsächlich für jede denkbare Landkarte vier verschiedene Farben genügen, will man zuverlässig verhindern, daß je zwei beliebige, benachbarte Länder, in gleicher Farbe erscheinen. Doch so staunenswert und umfangreich Kempes Beweisführung war - so falsch war sie leider auch; was zwar erst elf Jahre später bekannt wurde, im nachhinein aber höchst verständlich ist. Denn als 1976 mit Hilfe eines Rechners dann doch noch der korrekte Beweis des Theorems gelang, da umfaßte jener doch glatt - einige Millionen einzelner logischer Schlußfolgerungen. Nur mit Rechnerhilfe ist es möglich, solche logischen Ketten im Griff zu behalten, während "unbewaffnete" Menschen schon vor der schieren Größe einer solchen Verifizierungs-Aufgabe verzweifeln müßten. Mancher Mathematiker fühlt sich in dieser Abhängigkeit vom Computer durchaus unwohl.

Künftig indes kann dies alles ganz anders werden. Denn praktisch erstmals seit den Tagen der alten Griechen hat ein amerikanischer Mathematiker jetzt ein Verfahren zum Verifizieren mathematisch-logischer Beweisgänge entwickelt, das nicht allein auf dem schrittweisen Nachprüfen einer logischen Einzelaussage nach der anderen durch jeweils unabhängig nachdenkende Fachkollegen basiert.

Sanjeev Arora von der University of California zu Berkeley arbeitet bei seiner Methode mit einem neu entwickelten Computer-Algorithmus, der den jeweils zu untersuchenden Beweisgang automatisch in eine ganze Reihe einzelner Gleichungen umformt. Doch, diese Sammlung neu formulierter Gleichungen hat nun eine ganz spezielle Besonderheit: Sie ist so aufgebaut, daß ein beliebiger, logischer Fehler in der ursprünglichen Kette von Schlußfolgerungen verheerende Konsequenzen haben muß. Er führt nämlich dazu, daß in nahezu allen der neu generierten, einzelnen Gleichungen eben Fehler auftreten. Mithin genügt es fortan, wenn Mathematiker nur einfach eine bestimmte Anzahl der automatisch abgeleiteten Gleichungen auf interne Konsistenz prüfen: Zeigt sich dabei kein Fehler, sind also jeweils beide Seiten links und rechts vom Gleichheitszeichen wirklich gleich, so ist auch der Gesamt-Beweisgang - egal, wie umfangreich er auch sein mag - mit sehr großer Wahrscheinlichkeit korrekt.

Automatische Kontrolle der Programme

Das neue Verfahren des amerikanischen Mathematikers beschreibt genau, wie viele der neuen, einzelnen Gleichungen jeweils überprüft werden müssen, will man mit einer Zuverlässigkeit von n Prozent aussagen können, die ursprüngliche Beweisführung sei korrekt, also fehler- und widerspruchsfrei: Es wird dabei nämlich nur verlangt, daß diese Gleichungen nach dem Zufallsprinzip ausgewählt werden. Ihre Zahl ist für jedes gewünschte (Konfidenz-)n gleich groß, egal, wie umfangreich der ursprüngliche Beweisgang, den der Computer dann in Einzelgleichungen umgeformt hat, auch sein mag.

Mit der neuen Technik aus Berkeley soll es gleichzeitig auch möglich sein, die Resultate verwickelter Computerberechnungen auf Korrektheit zu überprüfen, was letztlich auf eine automatische Kontrolle der zugrundeliegenden Programme auf Fehlerfreiheit hinauslaufen würde. Und außerdem soll Aroras Methode nützliche Hilfen beim Bearbeiten jener bekannten Optimierungsaufgaben geben , bei denen man wegen der Komplexität des Problemes und der Begrenztheit der Rechenzeit meist nur die annähernd beste Lösung, kaum jedoch die wirklich günstigste Lösung finden kann. Man denke da nur etwa an das bekannte Problem des Handlungsreisenden, der zwischen vielen tausend Orten die kürzeste Reiseroute finden soll, Analoge Aufgaben stellen sich, wenn Leiterbahnen neuer Chips und Computer geplant werden, Flugpläne erarbeitet oder auch Ölleitungs- beziehungsweise Telefonnetze eingerichtet werden müssen.

Das neue Verfahren zur Überprüfung von mathematischen Schlußfolgerungs-Ketten unterscheidet sich vom gängigen, Schritt-für-Schritt-Nachvollziehen der logischen Einzel-Folgerungen durch Wissenschaftler vor allem dadurch, daß hier erstens Elemente des Zufälligen mit ins Spiel kommen und zweitens eine Art von Wechselspiel zwischen einem "Beweisführer" und einem "Verifizierer" stattfindet. Sowie außerdem natürlich darin, daß die interessante Kombination zweier auf diesem Gebiet ungewöhnlicher Ansätze nunmehr erlaubt, selbst solche Beweisgänge mit nahezu beliebig hoher Zuverlässigkeit als richtig oder falsch zu klassifizieren, die sich wegen ihrer schieren Komplexität bisher jeder Nachprüfung durch Gelehrte entzogen haben.

Die praktische Anwendung der Arbeiten Aroras und anderer Wissenschaftler auf das Problem, die - erhoffte - Fehlerfreiheit von komplizierten Rechnerprogrammen zu verifizieren, hat vor allem Aroras Berkeley-Kollegen Manuel Blum beschäftigt. Denn bisher kann man die Fehlerfreiheit von Programmen ja nur mit Hilfe von ausgedehnten Testläufen überprüfen; doch ist dies kein völlig wasserdichtes Verfahren, wie jeder Fachmann weiß. Und der zweite bekannte Weg, nämlich das logische Überprüfen des Programms Schritt für Schritt und unter Beachtung aller denkbaren Eingaben und System-Zwischenzustände, ist wiederum ein Vorgehen, nur bei einfachen Programmen tatsächlich praktikabel, während komplexe und umfangreiche Rechnerprogramme sich der logischen Überprüfung ebenso entziehen wie komplexe und lange mathematische Beweisketten.

Blum konzentrierte sich bei seinen Studien strikt auf die Frage, wie man eine Garantie dafür erlangen könne, daß ein bestimmtes Programm, bezogen auf bestimmte Eingabedaten, auch wirklich korrekte Ausgaben liefert.

Es gibt keine Garantie

Dabei arbeitet er grundsätzlich mit dem gleichen gedanklichen Ansatz, mit dem auch ein Schüler operiert, der eine nach mühsamen Wurzelziehen gefundene Lösung einfach und mühelos quadriert, um ihre Richtigkeit zu testen. Wobei dieses probate Verfahren übrigens, und dies zu sehen ist in diesem Zusammenhang höchst wichtig, nichts darüber aussagt, ob der Schüler beim Radizieren nicht zwischendurch einen Fehler gemacht hat, der nur zufälligerweise folgenlos geblieben ist.

Auch im Falle der Computerprogramme garantiert das beschriebene Vorgehen nicht, daß das jeweilige Programm wirklich ganz frei von Fehlern ist: Nach Blums Methode wird eben bloß mit einem sehr hohen Maß an Sicherheit gesagt, daß das fragliche Resulat in der Tat das richtige ist, während das Programm selber durchaus noch Fehler haben mag, die in anderen Fällen lästig werden könnten.

Ein Beispiel für Blums Verfahren ist das Überprüfen zweier - hinreichend komplizierter - Graphen, die die Gestalt von Gitternetzen aufweisen, auf Gleichheit. Diese Aufgabe kann heute ein kommerziell bewährtes Programm lösen - doch ist dessen Antwort, also entweder ja oder Nein, denn auch mit Sicherheit die richtige?

Um dies beispielsweise im Falle einer Nein-Aussage exakt zu prüfen, geht der Verifizierer am besten in zwei Schritten vor. Dazu gibt er dem System zu. nächst den ersten der beiden Graphen gleich zweimal ein, wobei er aber die Benennung der Punkte des einen dieser identischen Graphen nun zufallsgesteuert ändert, nicht aber dessen Gestalt. In einem zweiten Schritt programmiert der Anwender, wie schon beim allererste n Programmlauf, sowohl Graph 1 als auch Graph 2 ein, wobei er in Graph 2 aber gleichfalls die Benennung der Punkte zufallsgesteuert modifiziert, während dessen Gestalt voll beibehalten wird.

Arbeitet das Vergleicherprogramm - sowie obendrein der Computer selbst - korrekt, so muß in Schritt 1 nun stets die Antwort Ja, also Gleich, erscheinen; in Schritt 2 indes stets die Antwort Nein beziehungsweise Ungleich. Und wird dieses Verifizierungsverfahren nun mehrere Dutzend Male wiederholt und dabei immer wieder sinnvoll variiert, so wird am Ende die Möglichkeit, daß ein fehlerbehaftetes Vergleicherprogramm rein zufällig doch immer wieder korrekte Antworten gibt, irgendwann extrem beziehungsweise beliebig klein.

Daß Blums System des Verifizierens tatsächlich praktisch nutzbar ist, erwies sich en passant im Falle eines Verschlüsselungs-Algorithmus, dessen Ausgaben fortlaufend auf eine Weise ähnlich der eben skizzierten überprüft wurden. Dabei stellte sich nämlich heraus, daß bei ganz bestimmten, äußerst selten auftretenden Zeichenkonstellation en irgend etwas schief ging - und siehe da: Tatsächlich hatte das Programm einen ganz bestimmten Unauffälligen und sich nur selten auswirkenden Fehler.

Fehler müssen ins Auge springen

Weiterentwicklungen der gedanklichen Ansätze Aroras und Blums führten inzwischen zu einem Verfahren, bei dem ein simpler PC sogar zur Kontrolle veritabler Supercomputer genutzt werden kann, die unabhängig voneinander beide zur gleichen Zeit an der gleichen Aufgabe arbeiten. Dabei werden die Superrechner auf raffinierte Weise dazu gebracht, widersprüchliche Aussagen zu liefern, wenn irgendwo im Gesamtsystem von Programmen und Maschinen ein Fehler vorliegt.

Diese Methode wurde von Wissenschaftlern wie Arora inzwischen so ausgebaut, daß man nunmehr einen Computer-Algorithmus oder auch eine mathematische Beweisführung in eine, wie es heißt, transparente beziehungsweise holographische Form überführen kann, die - wie oben schon skizziert - jeden vorkommenden Fehler ins Groteske übersteigert. Dabei wird die ursprüngliche Kette von logischen beziehungweise Programm-Einzelschritten in einzelne, formelle mathematische Aussagen transformiert, die dann auf eine ganz spezifische Weise miteinander verkoppelt werden. Was wiederum bewirkt, daß Fehler in den ursprünglichen Schlußfolgerungen sich nunmehr in vielen der neu generierten Einzelschritte auswirken und somit rasch ins Auge springen müssen.

Dank dieser Fortschritte, so erläutert als einer der Väter dieser innovativen Techniken Laszlo Babai von der Universität Chicago, kann ein Verifizierer, der mit einem simplen, aber als zuverlässig bekannten Kleinrechner Arbeitete die Korrektheit des transformierten und nahezu beliebig umfangreichen Berechnungsgangs beziehungsweise der transformierten mathematischen Beweisführung nachprüfen. Und zwar geht dies laut Babai weitaus schneller vonstatten als die eigentliche, komplizierte Berechnung auf der vielleicht , unzuverlässigen Supermaschine mit dem möglicherweise fehlerbehafteten Programm dauert.

Ein kleiner Rechner genügt für das Verifizieren

Wichtig an alledem ist, daß diese Methode aber nicht etwa geeignet ist, Theoreme, also mathematische Vermutungen und Behauptungen, zu beweisen: Denn dazu, so Babai, bedarf es weiterhin noch eines stattlichen Quentchens Genialität. Doch zum Verifizieren, ob ein vorgeblich korrekter Beweis wirklich mit sehr großer Wahrscheinlichkeit hieb- und stichfest ist - dafür genügt nun einfach ein kleiner Rechner.

Wie steht es schließlich mit den oben schon angesprochenen Optimierungsproblemen? Also mit Problemen der Handlungsreisenden oder beispielsweise auch mit dem sogenannten Cliquenproblem, bei dem aus einer großen Zahl von Menschen unter all den einzelnen Personengruppen - beziehungsweise Cliquen -, in denen jeweils jeder jeden kennt, die größte gefunden werden soll.

Im Kreise dieser und ähnlicher, sogenannter harter Optimierungsaufgaben gibt es jüngsten Forschungen zufolge eine bestimmte Gruppe von Problemstellungen, die der Bearbeitung ganz besonders schwer zugänglich sind. Denn während bei derartigen Aufgaben normalerweise zwar nicht die beste, wohl aber eine recht gute Lösung in akzeptabler Zeit gefunden werden kann, sind die Probleme dieser neu erkannten Gruppe so beschaffen, daß auch kein annähernd gutes Resultat zu finden ist. Oder, genauer gesagt: Man kann hier jeweils nie sicher sein, daß in angemessener Zeit ein akzeptables Ergebnis erzielt werden kann. So daß es also praktisch keinen Sinn mehr hat, hier nach guten Näherungslösungen zu suchen; den auch dies würde ja schon bei mittleren Problemumfängen Rechenzeiten erfordern, die weit länger als die Geschichte unseres Universums dauerten.

Man hat Dank der Arbeiten Blums, Aroras und ihrer Kollegen nun also ein Instrument zur Hand, das zumindest angeben kann, in welchen Fällen man fortan besser gar nicht erst versuchen sollte, die kombinatorische Explosion einer dieser harten Optimierungsaufgaben in den Griff zu bekommen. Und, wie erwähnt, einen Ansatz zum Überprüfen komplexerer , Programme bieten die neuen Verfahren gleich obendrein.

Wenn neue mathematische Verfahren es jetzt endlich möglich machen sollen, die Richtigkeit eines Computer-Outputs für jeweils den konkreten Berechnungsfall mit seinen ganz spezifischen Input-Daten zu bestätigen beziehungsweise zu widerlegen, so hört sich dies zunächst recht gut an. Doch treten gleichzeitig auch logische Probleme auf, die vor allem in der folgenden Frage wurzeln: Wie kann man eigentlich hieb- und stichfest - und hier eben in mathematisch eindeutiger Weise - beschreiben, was ein Computer und was ein Programm exakt "tun" soll? Denn allein schon das Schreiben wirklich wasserdichter und vollständiger Spezifikationen ist ja nur in trivialen Fällen ohne weiteres möglich.

Viel Aufwand für die Nachprüfung

Es kann also sein, daß zum Neuformulieren wichtiger Programme mit dem Ziel, ihren Output maschinell nachprüfbar zu machen, ein hoher Aufwand zu treiben sein wird.

Mit Blick auf extrem sicherheitskritische Programmsysteme ist außerdem zu bemerken: Der Nachweis, daß das Resultat einer Berechnung korrekt ist, läßt sich zwar mit beliebig hoher Wahrscheinlichkeit erbringen - einfach, indem man entsprechend viele Verifizierungsroutinen durchläuft. Aber zumindest für Mathematiker sind 99,9999999 Prozent immer noch etwas grundlegend anderes als glatte 100 Prozent.

Eine Tatsache, um die schon Murphy mit seinem bekannten Gesetz ("Alles, was schiefgehen kann, geht irgendwann schief") wußte.