Anti-Unification Completeness Analysis in PVS

Stellen Sie sich vor, Sie haben zwei sehr unterschiedliche Lego-Burgen. Die eine ist ein winziger, einfacher Turm, die andere eine massive, komplexe Festung mit Geheimpassagen. Stellen Sie sich nun vor, Sie möchten einen „Master-Blaupausen“-Entwurf erstellen, der das Wesen beider Burgen einfängt. Sie wollen die Teile finden, die sie gemeinsam haben (wie „hat eine Tür“ oder „hat ein Dach“), und die einzigartigen, verwirrenden Teile in generische Platzhalter verwandeln (wie „ein Block irgendeiner Farbe“). Dieser Prozess, das Gemeinsame zu finden und gleichzeitig die Unterschiede zu verbergen, wird Anti-Unifikation genannt.

Jahrzehntelang haben Informatiker diesen Trick verwendet, um Bugs zu beheben, kopierten Code zu finden und sogar langsame Software in schnelle, parallele Software umzuwandeln. Aber es gab einen Haken: Wir hatten zwar ein Rezept (einen Algorithmus), um solche Blaupausen zu erstellen, aber wir hatten keinen mathematisch wasserfesten Beweis dafür, dass das Rezept immer perfekt für jedes mögliche Paar von Burgen funktioniert. Wir wussten, dass es nicht abstürzt (es war „sound“), aber wir hatten nicht bewiesen, dass es immer die bestmögliche Blaupause findet (es war „komplett“).

Dieses Paper ist die Geschichte eines Teams von Forschern, die diesen fehlenden Beweis schließlich mithilfe eines digitalen Beweisprüfers namens PVM erbracht haben.

Das Rätsel der „gelösten“ Teile

Um zu verstehen, warum dies so schwierig war, muss man sich ansehen, wie der Algorithmus arbeitet. Er zerlegt die zwei Burgen Stück für Stück.

• Der einfache Teil: Wenn er zwei identische Steine sieht, sagt er: „Verstanden!“ und macht weiter.
• Der knifflige Teil: Wenn er zwei verschiedene Steine sieht (sagen wir, einen roten und einen blauen), gibt er nicht einfach auf, wie es bei einem normalen Abgleichspiel der Fall wäre. Stattdessen sagt er: „Ah, diese sind unterschiedlich! Ich werde mir diesen Unterschied merken und weiter nach anderen Rot-gegen-Blau-Differenzen an anderer Stelle suchen.“

In einem normalen Abgleichspiel (genannt „Unifikation“) bedeutet das Finden eines Unterschieds, dass man sofort verliert. Bei der Anti-Unifikation ist das Finden eines Unterschieds jedoch tatsächlich das Ziel. Der Algorithmus muss ein fortlaufendes Tagebuch über jeden gefundenen Unterschied führen.

Die Forscher stellten fest, dass der Beweis, dass der Algorithmus für die „einfachen“ Teile funktioniert, überraschend schwierig war. Tatsächlich ging bei ihrer bisherigen Arbeit 91,10 % der Anstrengung, den Algorithmus korrekt zu beweisen, in nur zwei spezifische Fälle: das Handhaben von „gelösten“ Problemen (wo der Algorithmus einen Unterschied erkennt) und „syntaktische“ Probleme (wo die Teile identisch sind). Es klingt einfach, aber zu beweisen, dass der Algorithmus diese Unterschiede korrekt aufzeichnet, ohne verwirrt zu werden, erforderte eine enorme Menge an strenger Überprüfung.

Das „Geschichtsbuch“ des Algorithmus

Der entscheidende Durchbruch in diesem Paper bestand in der Erkenntnis, dass man nicht nur den aktuellen Schritt betrachten kann, um zu beweisen, dass der Algorithmus die beste Blaupause findet. Man muss die gesamte Historie der Berechnung betrachten.

Die Autoren führten eine neue Art des Denkens über das „Gedächtnis“ des Algorithmus ein. Sie definierten einen „Total Generalizer“ – einen schicken Begriff für eine Master-Blaupause, die Folgendes berücksichtigt:

1. Die Teile, die noch darauf warten, geprüft zu werden.
2. Die Teile, die bereits geprüft und als „unterschiedlich“ markiert wurden.
3. Die „Substitution“ (die Liste der Regeln), die der Algorithmus während des Prozesses aufbaut.

Sie bewiesen mehrere „Invarianz-Eigenschaften“. Dies sind Regeln, die besagen: „Egal wie viele Schritte der Algorithmus macht, die bisher gefundene Gesamtliste der Unterschiede verschwindet nie oder ändert nicht ihre Bedeutung.“ Sie zeigten, dass selbst wenn der Algorithmus ein großes Problem in winzige Teilprobleme zerlegt, die „Geschichte“ des ursprünglichen Problems intakt bleibt, genau wie ein Puzzle, das dasselbe Bild zeigt, auch wenn man es in kleinere Teile zerlegt und durchmischt.

Die „eingeschränkte“ Blaupause

Hier kommt der clevere Kniff. Um den Beweis zu ermöglichen, mussten die Autoren eine spezielle Art von Blaupause erfinden, die „Restricted Total Generalizer“ (eingeschränkter Total Generalizer) genannt wird.

Stellen Sie sich vor, Sie versuchen, ein Rezept zu schreiben. Wenn Sie Zutaten verwenden, die bereits in der Küche vorhanden sind (Variablen, die der Algorithmus gerade verwendet), könnten Sie versehentlich das Rezept ändern, während Sie es schreiben. Deshalb sagten die Autoren: „Lassen Sie uns für unseren Beweis nur frische, unbenutzte Zutaten verwenden.“ Sie bewiesen, dass man, wenn man eine Blaupause unter Verwendung dieser „frischen“ Zutaten finden kann, diese immer wieder in eine normale Blaupause zurückübersetzen kann.

Durch die Beschränkung der Blaupause auf diese „frischen“ Zutaten konnten sie den Theorem 20 beweisen: Das Endergebnis des Algorithmus ist immer mindestens so spezifisch wie jede andere mögliche Blaupause, die man erstellen könnte. Mit anderen Worten: Der Algorithmus übersieht niemals eine bessere Lösung.

Was dies bedeutet (und was es nicht tut)

Das Paper beweist (nicht nur suggeriert), dass der regelbasierte Algorithmus für die syntaktische Anti-Unifikation komplett ist. Das bedeutet, dass mathematisch garantiert ist, dass er immer den am wenigsten allgemeinen Generalisierer (die präziseste gemeinsame Blaupause) für zwei beliebige Terme findet.

Das Paper ist jedoch sehr vorsichtig bezüglich dessen, was es noch nicht leistet:

• Es liefert nicht den fertigen, maschinengeprüften Code, den man jetzt direkt ausführen kann. Die Autoren geben an, dass die Formalisierung der neuen Definitionen und Lemmata ein „Work in Progress“ ist.
• Es behauptet nicht, die Anti-Unifikation für alle Arten von Mathematik (wie jene, die Kommutativität oder Assoziativität beinhalten) gelöst zu haben. Es konzentriert sich strikt auf die „syntaktische“ Anti-Unifikation (die Standard-Variante).
• Es behauptet nicht, dass der Algorithmus in Bezug auf die Geschwindigkeit schnell oder effizient ist; es beweist lediglich, dass die Logik korrekt und vollständig ist.

Das Fazit

Dieses Paper ist eine rigorose, schrittweise Zerlegung eines Computer-Algorithmus. Die Autoren haben nicht nur gesagt: „Es funktioniert.“ Sie haben eine digitale Festung der Logik errichtet und jeden einzelnen Schritt überprüft, insbesondere die langweiligen, aber kritischen Teile, in denen der Algorithmus Unterschiede erkennt. Sie haben gezeigt, dass man, indem man ein perfektes „Geschichtsbuch“ der Berechnung führt und eine clevere „eingeschränkte“ Art des Denkens über Lösungen verwendet, garantieren kann, dass der Algorithmus immer die richtige Antwort findet.

Da die Mathematik nun bewiesen ist, steht die Tür für den nächsten Schritt offen: die Extraktion von „zertifiziertem ausführbarem Code“. Das bedeutet, dass wir in Zukunft diesen Algorithmus nehmen und in Software verwandeln können, die mathematisch garantiert ist, niemals Fehler beim Finden gemeinsamer Muster in Code oder chemischen Verbindungen zu machen. Aber für den Moment liegt der Sieg im Beweis selbst: Das Rätsel darüber, warum es funktioniert, ist endlich gelöst.