Zeugen für mathematische Software

Ich bin, wie viele Menschen, ein begeisterter Benutzer von mathematischer Software wie Mathematica und Maple. Ich bin jedoch zunehmend frustriert über die vielen Fälle, in denen eine solche Software Ihnen ohne Vorwarnung einfach die falsche Antwort gibt. Dies kann auftreten, wenn unter vielen anderen Beispielen alle Arten von Operationen ausgeführt werden, von einfachen Summen bis zur Optimierung .

Ich habe mich gefragt, was gegen dieses ernste Problem getan werden könnte. Was benötigt wird, ist eine Möglichkeit, dem Benutzer zu ermöglichen, die Richtigkeit einer Antwort zu überprüfen, damit er ein gewisses Vertrauen in das hat, was ihm gesagt wird. Wenn Sie eine Lösung von einem Mathematikkollegen erhalten, kann er / sie sich einfach hinsetzen und Ihnen ihre Arbeit zeigen. Dies ist jedoch in den meisten Fällen für einen Computer nicht möglich. Könnte der Computer Ihnen stattdessen ein einfaches und leicht überprüfbares Zeugnis für die Richtigkeit ihrer Antwort geben? Die Überprüfung muss möglicherweise vom Computer durchgeführt werden, aber hoffentlich ist die Überprüfung des Überprüfungsalgorithmus viel einfacher als die Überprüfung des Algorithmus, um den Zeugen überhaupt erst zu erstellen. Wann wäre dies machbar und wie genau könnte dies formalisiert werden?

Zusammenfassend ist meine Frage die folgende.

Könnte es zumindest theoretisch möglich sein, dass mathematische Software einen kurzen überprüfbaren Beweis zusammen mit der von Ihnen angeforderten Antwort liefert?

Ein trivialer Fall, in dem wir dies sofort tun können, ist natürlich die Faktorisierung von ganzen Zahlen oder vieler der klassischen NP-vollständigen Probleme (z. B. Hamilton-Schaltung usw.).

1. Das Konzept der "Zeugen" oder "überprüfbaren Beweise" ist nicht ganz neu: Wie in den Kommentaren erwähnt, suchen Sie nach dem Konzept des "Zertifikats". Drei Beispiele kamen in den Sinn, es gibt mehr (in den Kommentaren und anderswo):

   • Kurt Mehlhorn beschrieb 1999 ein ähnliches Problem bei Algorithmen für die rechnergestützte Geometrie (z. B. können kleinere Fehler in Koordinaten zu großen Fehlern bei den Ergebnissen einiger Algorithmen führen), das auf ähnliche Weise in der Bibliothek Leda gelöst wurde , indem er darauf bestand, dass jeder Algorithmus ein "Zertifikat" erzeugt. seiner Antwort zusätzlich zur Antwort selbst.

   • Demaine, Lopez-Ortiz und Munro verwendeten im Jahr 2000 die Konzepte von Zertifikaten (sie nennen sie "Beweise"), um adaptive Untergrenzen für die Berechnung der Vereinigung und des Schnittpunkts (und der Differenz, aber diese ist trivial) sortierter Mengen aufzuzeigen. Schließen Sie ihre Arbeit nicht aus, da sie keine Zertifikate zum Schutz vor Rechenfehlern verwendet haben: Sie haben gezeigt, dass das Zertifikat zwar im schlimmsten Fall linear in der Größe der Instanz sein kann, jedoch häufig kürzer ist und daher überprüft werden kann "in sublinearer Zeit (bei wahlfreiem Zugriff auf die Eingabe als sortiertes Array oder B-Tree) und insbesondere in weniger Zeit als erforderlich, um ein solches Zertifikat zu berechnen.

   • Ich habe das Konzept von Zertifikaten für verschiedene andere Probleme verwendet, seit Ian Munro ihre Implementierung auf der Alenex 2001 vorgestellt hat , insbesondere für Permutationen (Entschuldigung für den schamlosen Stecker, eine weitere kommt), bei denen das Zertifikat im besten Fall kürzer ist als im schlimmsten oder durchschnittlichen Fall, was eine komprimierte Datenstruktur für Permutationen ergibt. Auch hier dauert die Überprüfung des Zertifikats (dh der Bestellung) höchstens linear, weniger als die Berechnung (dh die Sortierung).

2. Das Konzept ist nicht immer nützlich für die Fehlerprüfung: Es gibt Probleme, bei denen die Prüfung des Zertifikats genauso lange dauert wie die Erstellung (oder einfach die Erstellung des Ergebnisses). Zwei Beispiele kommen in den Sinn, eines trivial und eines kompliziert, Blum und Kannan (in den Kommentaren erwähnt) geben andere.

   • $n$$n$
   • Das Zertifikat für die konvexe Hülle in zwei und drei Dimensionen benötigt, wenn die Punkte in zufälliger Reihenfolge angegeben werden, so viele Bits zum Codieren wie Vergleiche zum Berechnen von [FOCS 2009] (anderer schamloser Stecker).

Die Bibliothek Leda ist die allgemeinste (mir bekannte) Anstrengung, deterministische Algorithmen zur Erstellung von Zertifikaten in der Praxis zur Norm zu machen. Das Papier von Blum und Kannan ist die beste Anstrengung, die ich gesehen habe, um es theoretisch zur Norm zu machen, aber sie zeigen die Grenzen dieses Ansatzes.

Ich hoffe es hilft...