Die Verfahren des interaktiven und des transparenten Beweisens dienen dazu, hochkomplizierte Rechnungen und mathematische Beweise auf relativ einfache Art computergestuetzt zu verifizieren. Egon Schmidt* gibt einen Ueberblick.
Tief im Innern eines maechtigen Bergmassivs, abgeschirmt gegen jeden denkbaren Zugriff, summen im Dienste geheimer Regierungsstellen Dutzende der maechtigsten Supercomputer unserer Zeit vor sich hin. Doch ob all die Milliarden von Zahlen, die von ihnen fortlaufend um- und umgewaelzt werden, auch richtig berechnet sind - das ueberwacht am Ende ein simpler, wenngleich hochgradig zuverlaessiger PC.
Ein besonders robuster, ausfallsicherer Kleinrechner als Kontrollinstanz gewaltiger, aber nicht ebenso zuverlaessig operierender Rechenmonster - dieses utopisch anmutende Szenario koennte schon bald Wirklichkeit werden, erwarten Mathematiker und Informatiker. Neuere Fortschritte ihrer wissenschaftlichen Disziplinen eroeffnen Perspektiven, die vor kurzem noch undenkbar schienen.
Im Zentrum dieser Neuerungen steht die Entdeckung, dass eine langwierige mathematische Beweisfuehrung beziehungsweise Berechnung auch anders als muehselig Schritt fuer Schritt und Zeile um Zeile auf Korrektheit ueberprueft werden kann; wenigstens dann, wenn man bereit ist, ein unvermeidbares, aber sehr weitgehend zu minimierendes Risiko gelegentlicher falscher Befunde in Kauf zu nehmen. Die neuen Verfahren koennen vielleicht auch helfen, das - hoffentlich - korrekte Verhalten komplizierter Programme zu bestaetigen beziehungsweise - wie etwa Manuel Blum von der University of California zu Berkeley dies vorhat - Programme zu entwickeln, die sich waehrend ihrer Abarbeitung durch den Rechner selber kontrollieren.
Auf eine kurze Formel gebracht, wird bei der neuen Technik die undurchschaubare Berechnung beziehungsweise das fragliche Programm in einer ganz bestimmten Art und Weise verschluesselt. Dabei nimmt der Ausgangs-Bitstrom eine Gestalt an, bei der seine eventuellen Fehler oder Widersprueche jedem sofort ins Auge springen, der auch nur einige wenige, beliebig ausgewaehlte Bits der verschluesselten Version betrachtet.
Die neuen Ideen wurzeln in Arbeiten erfahrener Kryptologen aus Boston, Toronto und Chicago, die bei der Suche nach besseren Codierverfahren unter anderem auch die Idee des "interaktiven Beweises" kreierten. Er ist eine Technik des logischen Beweisens, bei der ein "Pat" und eine "Vanna" - so die spassigen, einer Fernsehserie entlehnten Namen der amerikanischen Forscher fuer je einen "Beweiser" (Prover) und einen "Verifizierer" - im Wechselspiel zusammenarbeiten. Pat ist zwar sehr leistungsstark, aber unzuverlaessig, Vanna entspricht dem oben erwaehnten, aeusserst zuverlaessigen PC. Beide Partner besitzen eine Kopie der Behauptung, deren Wahrheit Vanna beweisen soll. Vanna wiederum prueft kritisch die Argumente, die Pat vorbringt, und entscheidet schliesslich am Ende: Ja, die Behauptung ist mit hoher und beliebig vergroesserbarer Wahrscheinlichkeit wahr - oder sie ist es nicht. Wie dieses interaktive Beweisen im einzelnen ueber die Buehne geht, laesst sich am Beispiel sogenannter Graphen mit ihren geraden Linien und Eckpunkten verdeutlichen.
Pruefung der Isomorphie bei Graphen essentiell
Beim interaktiven Beweisen interessiert vor allem die Frage, ob zwei Graphen "isomorph" sind. Dazu muessen zwei Voraussetzungen erfuellt sein: Erstens muessen sich die einzelnen Eckpunkte in beiden Graphen in uebereinstimmender Weise benennen lassen; zweitens muessen in beiden Graphen dieselben Eckpunkte miteinander benachbart sein. Als benachbart gelten Punkte, die mit einer Linie verbunden sind, wobei die Verbindungen unterschiedlich lang sein duerfen; entscheidend ist nur, dass sie ueberhaupt bestehen. Bislang ist ein einziger, wenigstens theoretisch stets zum Ziel fuehrender Weg bekannt, zwei Graphen mit - beispielsweise - je 846786 Ecken auf Isomorphie zu pruefen: naemlich der, dass man entsprechend den beiden genannten Bedingungen der Isomorphie zunaechst beim einen einfach alle Ecken auf beliebige Weise durchnumeriert und beim anderen dann stur alle kombinatorischen Moeglichkeiten, die verschiedenen Ecken mit den Zahlen 1 bis 846786 zu benennen, ausprobiert; zweitens muss man dann noch feststellen, ob in beiden Graphen dieselben Ecken benachbart sind.
So muehselig und zeitraubend dieses Verfahren wegen der Fuelle an Kombinationsmoeglichkeiten nun insgesamt auch ist, so leicht und rasch laesst sich damit wenigstens herausfinden, ob eine vorab bereits verifizierte und jetzt einfach behauptete Isomorphie tatsaechlich vorhanden ist. Dazu genuegt es ja, die einzelnen Ecken- Paare jeweils gleicher Numerierung ein einziges Mal vollstaendig auf das Kriterium "benachbart" zu untersuchen. Der umgekehrte Beweis, dass naemlich zwei komplizierte Graphen gleicher Ecken- und Kantenzahl mit Sicherheit nicht isomorph sind, stellte dagegen bislang eine ausgesprochen harte Nuss dar.
Genau hier hilft die neuartige, interaktive Beweisfuehrung weiter, wie die US-amerikanischen Wissenschaftler Oden Goldreich und Avi Wigderson herausgefunden haben. Mit ihr laesst sich eine bereits vorliegende Beweisfuehrung konventioneller Art, die den Non- Isomorphismus zweier Graphen konstatiert, hochgradig zuverlaessig auf Richtigkeit ueberpruefen. Bei diesem Vorgehen waehlt der Verifizierer Vanna zufallsgesteuert einen der beiden Graphen - sie sollen I und J heissen - aus, also beispielsweise den I. Dann uebermittelt er dem Beweiser Pat eine computergerecht verschluesselte Beschreibung - hier I'genannt - dieses Graphen, bei der nun aber die Ecken mit anderen Bezeichnungen versehen sind als bei I.
Nun untersucht das leistungsfaehige und mit beliebig viel Rechenzeit ausgestattete Beweisersystem Pat I' auf Isomorphie mit den ihm schon bekannten Graphen I und J, indem es, wie oben geschildert, systematisch alle Benennungsmoeglichkeiten der Ecken durchprobiert. Dann meldet es dem Verifizierer je nach seinen Feststellungen entweder, I sei mit I' isomorph, oder J sei es; und hat Pat, was bei Isomorphie von I und J ja stets zu erwarten waere, sowohl I als auch J fuer isomorph mit I' befunden, meldet er - nun aber einfach zufallsgesteuert - nur entweder I oder J als isomorph zurueck.
Dieses Verfahren wird mehrfach wiederholt. Vanna registriert dabei lediglich, ob immer nur I als isomorph mit I' zurueckgemeldet wird oder auch J. Mit jeder Rueckmeldung nur von I steigt die Wahrscheinlichkeit, dass I und J - wie ja bewiesen werden soll - nicht isomorph sind; waehrend gelegentliches Rueckmelden von J fuer das Gegenteil spricht. Die Wahrscheinlichkeit, dass wirklich Non- Isomorphie vorliegt, betraegt nach einer Rueckmeldung nur von I zwei zu eins, nach zweien bereits vier zu eins, nach dreien acht zu eins und nach zehnen schon 1024 zu eins. Das skizzierte Verfahren wurde alsbald um Varianten mit mehreren Pats erweitert, die strikt von ihrem/n Kollegen abgeschottet vor sich hin arbeiten. Mathematiker konnten schon bald zeigen, dass die Aussagen, die bei Einsatz mehrerer Pats und einer Vanna erarbeitet werden, besser sind als bei nur einem Pat.
Insbesondere wurde bewiesen, dass bereits mit nur zwei Pats die Loesungen aller Angehoerigen einer sehr grossen Klasse mathematischer Probleme hinreichend kritisch - sowie bislang konkurrenzlos einfach und schnell - ueberprueft werden koennen. Wobei es sich hier, um dies fuer Experten zu notieren, um die Klasse der Nichtdeterministisch-exponentiellen Probleme (NEXP) handelt, die wiederum die Klasse der Nichtdeterministisch-polynomiellen Probleme (NP) einschliesst. Zu letzteren gehoert beispielsweise das klassische Problem, fuer einen Handelsvertreter die kuerzeste Reiseroute zwischen zahlreichen Staedten zu finden - einschliesst.
Vom interaktiven Beweisen ausgehend und mit Blick auf den Wunsch, noch umfangreichere Berechnungen verifizieren zu koennen, kamen Wissenschaftler in Boston und Chicago 1991 auf das noch weiter ausgreifende Konzept des "transparenten Beweises", das auf viel komplizierterer Mathematik basiert und sich hier nur andeutungsweise skizzieren laesst.
Man kann sich einen solchen Beweis im Ergebnis als lange Folge von Nullen und Einsen vorstellen, die eine verschluesselte Variante einer Behauptung BT samt des zugehoerigen Beweisgangs BW darstellt. Diese lange Kette von Binaerzeichen hat die Eigenschaft, dass ein Verifizierer schon nach kurzer Pruefung einiger weniger, zufaellig ausgewaehlter Bits mit hoher Wahrscheinlichkeit sagen kann, ob BW bezueglich BT korrekt ist.
Verifizierung des Beweises "von Hand" nicht moeglich
Dies erklaert sich grob damit, dass die Binaerzeichenreihe unter anderem eine grosse Menge an redundanter Information ueber die Aussage umfasst, dass und wie BW der Beweis fuer BT ist beziehungsweise sein soll. Diese redundante Information wiederum ist in gewissen regelmaessigen Mustern ueber die Binaerzeichen verstreut.
Das neue Verfahren ist schnell. Umfasst der Beweis beispielsweise rund 100000 Symbole, so genuegt zu seiner Ueberpruefung das Betrachten von rund 600 Zeichen seiner transparenten Codierung. Qualitativ entspricht die Methode dem interaktiven Beweisen mit mehreren Pats. Interessante Zusammenhaenge haben Mathematiker mittlerweile zwischen den interaktiven Beweisverfahren einerseits sowie Methoden zur annaehernden Loesung "harter" Optimierungsprobleme andererseits gefunden. Dabei waren vor allem Versuche fruchtbringend, Graphen zu erarbeiten, die das Wechselspiel zwischen zwei Pats und einer Vanna in jenen Faellen symbolisieren, in denen dieses Trio sich mit der Loesung eines eines ausserordentlich schwierigen Optimierungsproblems der formellen Logik befasst.
Die einschlaegigen Studien haben inzwischen gezeigt, dass von Systemen fuer interaktives Beweisen mit mindestens zwei Pats ueber allgemeine Naeherungsverfahren fuer Optimierungsprobleme bis zum erwaehnten Problem des reisenden Vertreters und anderen Schwierigkeiten der angewandten Mathematik direkte Linien zu ziehen sind. Es stellte sich heraus, dass sich die gaengigen und nur zu naeherungsweisen Loesungen fuehrenden Algorithmen der unbekannten wahren Loesung lediglich bis zu einer gewissen Grenze angleichen koennen, aber nicht weiter und schon gar nicht bis auf Nulldistanz. In zukuenftiger Praxis duerfte nicht nur die Ueberwachung schneller Supercomputer durch hochgradig zuverlaessige Kleinrechner von Interesse sein, sondern auch das Komprimieren von Daten in Kommunikationsnetzen und Speichersystemen sowie das (Selbst- )Ueberpruefen, ob bestimmte Programme bislang korrekt gearbeitet haben. Auch die Verifikation mathematischer Beweisketten kann ein interessantes Gebiet fuer den Einsatz der neuen Techniken werden.
Mathematiker haben dabei allerdings weniger solche Beweise im Auge, die Menschen erarbeitet haben. Die muessten ja erst noch aufwendig in eine logisch lueckenlose, umfassende und obendrein voll computergerechte Gestalt ueberfuehrt werden. Anders steht es um Beweise, die ohnehin mit Hilfe eines Computers erarbeitet worden sind, wie etwa 1991 im Fall des bekannten Vierfarben-Theorems der Kartografie.
Dieses Theorem besagt in mathematischer Sprache, was die Hersteller von Landkarten seit jeher wissen, dass es naemlich genuegt, die einzelnen Laender eines beliebigen - hypothetischen wie realen - Kontinents mit vier verschiedenen Farben darzustellen, will man sicher vermeiden, dass irgendwo zwei Laender gleicher Farbe aneinandergrenzen.
Waehrend man diesen Sachverhalt durch Ausprobieren leicht nachvollziehen kann, war zu seinem zwingenden Beweis die Hilfe eines Computers unverzichtbar. Das Verifizieren dieses Beweises "von Hand" - wie dies sonst ja gang und gaebe ist - soll nach Auskunft kundiger Mathematiker unmoeglich sein.
*CW-Mitarbeiter Egon Schmidt ist freier Journalist in Muenchen.