Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

Die Arbeit stellt Apply2Isar vor, ein Werkzeug für Isabelle/HOL, das automatisch prozedurale „Apply-Style"-Beweisskripte in lesbare und robuste deklarativen Isar-Beweise umwandelt, wie eine Auswertung auf Basis des Isabelle Archive of Formal Proofs zeigt.

Das Wesentliche

Hier ist eine einfache Erklärung des Papers „Apply2Isar" auf Deutsch, verpackt in anschauliche Bilder und Metaphern.

Das Problem: Der chaotische Koch vs. das Kochbuch

Stell dir vor, du möchtest ein kompliziertes Gericht kochen (in diesem Fall einen mathematischen Beweis beweisen). Es gibt zwei Arten, wie man das tun kann:

1. Der „Apply-Style" (Der chaotische Koch):
   Stell dir einen Koch vor, der einfach drauflos kocht. Er nimmt eine Zutat, rührt sie um, schmeckt, fügt Gewürze hinzu und schaut, was passiert. Er weiß nicht genau, wie der Teller am Ende aussehen wird, aber er probiert sich durch.

   • Vorteil: Es geht sehr schnell! Man kann sofort sehen, ob etwas funktioniert.
   • Nachteil: Wenn man das Rezept später jemand anderem gibt, ist es ein undurchdringliches Durcheinander. Wenn sich eine Zutat ändert (z. B. wird das Salz durch Pfeffer ersetzt), bricht das ganze Gericht zusammen, und man weiß nicht mehr, wo der Fehler lag. Es ist schwer zu lesen und noch schwerer zu reparieren.

2. Der „Isar-Style" (Das strukturierte Kochbuch):
   Hier schreibt man ein echtes Rezept auf: „Nimm zuerst 2 Eier, dann rühre sie auf, dann füge Mehl hinzu." Jeder Schritt ist klar benannt und erklärt.

   • Vorteil: Jeder kann das Rezept lesen und verstehen. Wenn sich eine Zutat ändert, sieht man sofort, welcher Schritt im Rezept betroffen ist. Es ist robust und sicher.
   • Nachteil: Es dauert länger, das Rezept zu schreiben, besonders wenn man noch nicht genau weiß, wie das Gericht schmecken soll.

Die Lösung: Apply2Isar – Der Übersetzer-Roboter

Das Paper stellt ein neues Werkzeug namens Apply2Isar vor. Man kann es sich wie einen super-intelligenten Übersetzer-Roboter vorstellen.

• Was er tut: Du gibst ihm deinen schnellen, chaotischen „Koch-Code" (den Apply-Style-Beweis). Der Roboter schaut sich genau an, was der Koch Schritt für Schritt getan hat.
• Was er macht: Er schreibt das Chaos in ein sauberes, strukturiertes Kochbuch (den Isar-Code) um. Er notiert jeden Zwischenschritt, benennt die Zutaten und erklärt, warum etwas getan wurde.
• Das Ergebnis: Du hast am Ende das gleiche Gericht (den gleichen mathematischen Beweis), aber jetzt liegt ein perfektes, lesbares Rezept vor, das jeder verstehen kann.

Wie funktioniert das im Detail? (Die Magie hinter den Kulissen)

Der Roboter muss einige knifflige Tricks anwenden, weil die beiden Sprachen sehr unterschiedlich sind:

• Rückwärts vs. Vorwärts: Der chaotische Koch arbeitet oft rückwärts (vom Ziel her). Das Kochbuch muss aber vorwärts gelesen werden. Der Roboter dreht die Schritte also um, damit sie logisch fließen.
• Die „Kleber"-Methode: Manchmal entstehen beim Kochen mehrere Teller gleichzeitig (mehrere Ziele). Der Roboter klebt diese Schritte mit einer speziellen „Klebe-Notiz" (einem Fakt) zusammen, damit sie später wieder passen.
• Das Problem mit den Schatten: Manchmal benutzt der Koch einen Namen für eine Zutat, der schon existiert (z. B. nennt er eine neue Tomate auch „Tomate", obwohl es schon eine gibt). Das verwirrt den Roboter. Er muss dann vorsichtig neue Namen erfinden, damit nichts durcheinandergerät.
• Das „Entweder-Oder"-Problem: Manchmal probiert der Koch etwas aus, und wenn es nicht klappt, macht er einen Schritt zurück und probiert etwas anderes. Der Roboter erkennt diese Unsicherheit und baut sie so ein, dass das fertige Rezept trotzdem stabil ist, ohne die alten „Versuch-und-Irrtum"-Schritte zu zeigen.

Warum ist das wichtig? (Der Test)

Die Autoren haben den Roboter an tausenden echten Rezepten getestet (aus einer riesigen Bibliothek mathematischer Beweise).

• Das Ergebnis: In 95 % bis 99 % der Fälle hat der Roboter das Chaos perfekt in ein sauberes Kochbuch verwandelt.
• Der Nutzen: Forscher und Mathematiker können jetzt schnell ihre Ideen ausprobieren (chaotisch kochen) und lassen den Roboter später das saubere Dokument erstellen. Das spart Zeit und verhindert Fehler.

Fazit

Apply2Isar ist wie ein Assistent, der dir erlaubt, kreativ und schnell zu arbeiten, ohne dass du am Ende ein unlesbares Chaos hinterlässt. Er nimmt dir die mühsame Arbeit ab, aus deinem schnellen „Gedankenstrom" ein sauberes, professionelles Dokument zu machen. So hast du das Beste aus beiden Welten: Geschwindigkeit beim Entdecken und Sicherheit beim Speichern.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar" auf Deutsch:

1. Problemstellung

In Isabelle/HOL existieren zwei primäre Beweisstile:

• Apply-Style (Prozedural): Beweise werden als Skripte geschrieben, die rückwärts arbeiten (vom Ziel zu den Annahmen). Sie sind oft schnell zu schreiben und ermöglichen eine rasche Exploration des Suchraums, leiden aber unter mangelnder Lesbarkeit und Robustheit. Änderungen an Lemmata oder Vereinfachungsregeln können Beweise leicht brechen, ohne dass der Fehlerort sofort ersichtlich ist.
• Strukturierter Isar (Declarativ): Beweise sind explizit, lesbar und robust. Sie arbeiten vorwärts und dokumentieren Zwischenziele. Dies ist der bevorzugte Stil im Archive of Formal Proofs (AFP).

Das Problem besteht darin, dass Benutzer oft zunächst einen Apply-Style-Beweis schreiben, um schnell Ergebnisse zu erzielen, diesen jedoch später in Isar umwandeln müssen, um die Wartbarkeit zu sichern. Dieser manuelle Umwandlungsprozess ist mühsam, fehleranfällig und erfordert das manuelle Kopieren von Zwischenzuständen.

2. Methodik und Implementierung

Das Tool Apply2Isar wurde entwickelt, um diesen Prozess zu automatisieren. Es ist in Isabelle/ML implementiert und tief in die Isabelle-Umgebung integriert.

Kernprozess:

1. Parsing: Das Eingabe-Skript (ein Apply-Style-Beweis) wird tokenisiert und in einen abstrakten Syntaxbaum (AST) umgewandelt.
2. Replay (Wiedergabe): Apply2Isar führt den Beweis schrittweise aus, indem es die entsprechenden Isabelle/ML-Funktionen aufruft. Dabei werden die Zwischenzustände (Ziele und Fakten) nach jeder Methode protokolliert.
3. Konstruktion: Aus den protokollierten Zuständen wird ein neuer AST für den strukturierten Isar-Beweis aufgebaut.
4. Ausgabe: Der resultierende Isar-Beweis wird als String generiert und kann direkt in das Dokument eingefügt werden.

Herausforderungen und Lösungen:

• Umgang mit mehreren Zielen: Apply-Skripte können mehrere Ziele gleichzeitig bearbeiten (z. B. durch auto). Apply2Isar nutzt eine „Smart Goals"-Strategie, um redundante Wiederholungen zu vermeiden und nur die sich ändernden Ziele in have-Anweisungen zu drucken.
• Beweisfluss und Subziele: Befehle wie subgoal oder supply (die Fakten einführen) müssen in Isar oft an den Anfang des Beweises verschoben werden, um die Abhängigkeiten korrekt darzustellen. Das Tool hebt diese Befehle automatisch an oder verwendet „Dummy"-Subbeweise, um die ursprüngliche Reihenfolge beizubehalten.
• Namenskonflikte (Shadowing): Bei der Umwandlung von subgoal (das Variablen skolemisiert) können Namenskonflikte mit bestehenden Variablen entstehen. Apply2Isar bietet Optionen, um Variablennamen automatisch zu freshen (neu zu benennen), wobei dies bei expliziten Referenzen im Skript Grenzen hat.
• Schema-Variablen: Wenn Beweise schematische Ziele enthalten (die erst später instanziiert werden), kann Isar diese nicht direkt in have-Anweisungen abbilden. In solchen Fällen wird der entsprechende Teil des Beweises als vorläufiger Apply-Block innerhalb des Isar-Beweises belassen („partielle Übersetzung").
• Typen: Um Typfehler zu vermeiden, prüft das Tool, ob Typannotationen notwendig sind, und fügt diese nur bei Bedarf hinzu.

3. Schlüsselbeiträge

• Automatisierung: Das erste Tool, das Apply-Style-Skripte vollständig automatisch in strukturierten Isar-Code übersetzt, ohne dass der Benutzer manuell Zwischenziele definieren muss.
• Robustheit: Die generierten Beweise sind deutlich widerstandsfähiger gegen Änderungen in der Beweisumgebung (z. B. neue Simplifikationsregeln), da die Struktur explizit ist.
• Flexibilität: Das Tool unterstützt eine Vielzahl von Befehlen (siehe Tabelle 1 im Paper), einschließlich using, unfolding, subgoal und sogar sorry (für teilweise bewiesene Beweise).
• Determinismus: Im Gegensatz zu LLM-basierten Ansätzen (wie dem Isabelle Assistant) ist Apply2Isar vollständig deterministisch und läuft lokal ohne Cloud-Abhängigkeit.

4. Ergebnisse (Evaluation)

Die Autoren bewerteten Apply2Isar an einem Benchmark von 4.461 Apply-Style-Beweisen aus fünf großen Einträgen des AFP (u. a. Group-Ring-Module, AutoCorres2, Flyspeck-Tame).

• Erfolgsrate: In 95 % bis 99 % der Testfälle konnte der Beweis vollständig oder teilweise in Isar übersetzt werden.
• Partielle Übersetzungen: Viele „Fehler" waren in Wirklichkeit nur partielle Übersetzungen, bei denen der Großteil des Beweises in Isar vorlag, aber kleine Abschnitte mit schematischen Zielen als Apply-Blöcke erhalten blieben.
• Fehlerquellen: Die meisten vollständigen Fehler traten aufgrund von Inkonsistenzen im Isabelle-Typ-Druckmechanismus auf (wenn Ziele gedruckt und neu geparst werden, entstehen Syntaxfehler). Dies ist ein bekanntes Problem in Isabelle und nicht spezifisch für das Tool.
• Performance: Das Tool wurde auf einem Standard-Hardware-Setup getestet und hielt sich in den meisten Fällen innerhalb eines 30-Sekunden-Timeouts pro Beweis.

5. Bedeutung und Ausblick

Apply2Isar schließt eine wichtige Lücke in der Isabelle/HOL-Toolchain. Es ermöglicht Entwicklern, die Vorteile der schnellen Exploration von Apply-Skripten zu nutzen, ohne auf die Wartbarkeit und Lesbarkeit von Isar verzichten zu müssen.

• Wartung: Es erleichtert die Pflege bestehender AFP-Einträge, die veraltete Apply-Skripte enthalten.
• Lernkurve: Es hilft neuen Benutzern, den Übergang von prozeduralen zu deklarativen Beweisen zu meistern.
• Zukunft: Mögliche Verbesserungen umfassen den Umgang mit benutzerdefinierten Befehlen, die Vermeidung von Namenskonflikten durch tiefere Methodenanalyse und die Integration von „Deautomation"-Techniken, um komplexe Automatisierungsschritte in primitive Schritte zu zerlegen.

Zusammenfassend stellt Apply2Isar einen signifikanten Schritt zur Verbesserung der Qualität und Nachhaltigkeit von formalen Beweisen in Isabelle/HOL dar, indem es die Brücke zwischen schneller Entwicklung und robuster Dokumentation schlägt.