Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

Die Arbeit stellt Strat2Rocq vor, ein Framework, das Beweissstrategien aus großen Sprachmodellen extrahiert und als formale Lemmas in Rocq integriert, um die Erfolgsrate symbolischer Beweiser wie CoqHammer sowie von LLM-Beweisagenten signifikant zu steigern.

Das Wesentliche

Hier ist eine einfache Erklärung der Forschung, als würde man sie einem Freund beim Kaffee erzählen, mit ein paar kreativen Vergleichen:

Das Problem: Der teure Genie-Experte vs. der solide Handwerker

Stell dir vor, du musst ein sehr komplexes mathematisches Rätsel lösen (in der Welt der Software: einen Beweis dafür, dass ein Programm sicher ist).

1. Der Handwerker (Symbolischer Beweiser): Das ist wie ein hochspezialisierter, extrem schneller Handwerker namens CoqHammer. Er ist super, wenn er die richtigen Werkzeuge hat. Aber manchmal fehlt ihm eine bestimmte Schraube oder ein spezieller Trick, und dann gibt er auf, auch wenn die Lösung eigentlich naheliegend wäre. Er arbeitet schnell, kostet nichts und ist absolut sicher (keine Daten werden nach außen geschickt).
2. Der Genie-Experte (KI-Modell / LLM): Das ist wie ein genialer, aber teurer Professor, der alles über Mathematik weiß. Er kann die Lösung oft sofort sehen, weil er Millionen von Beispielen gelernt hat. Aber: Er ist langsam, braucht riesige Stromkosten und man darf ihm keine geheimen Firmenpläne zeigen, weil man Angst hat, dass er sie "verrät".

Das Dilemma: Wir wollen die Sicherheit und Geschwindigkeit des Handwerkers, aber wir vermissen die genialen Ideen des Professors. Normalerweise müssten wir den Professor fragen, was teuer und riskant ist.

Die Lösung: Strat2Rocq – Der "Werkzeugkasten-Diebstahl"

Die Forscher haben sich eine clevere Idee ausgedacht: Warum fragen wir den Professor jedes Mal neu? Warum stehlen wir ihm nicht einfach seine besten Tricks und bauen sie in das Werkzeug des Handwerkers ein?

Das ist genau das, was Strat2Rocq macht. Es ist wie ein Übersetzer und Werkzeugmacher in einem.

Schritt 1: Der Offline-Training (Das "Ausspionieren")

Stell dir vor, der Handwerker (CoqHammer) und der Professor (KI) arbeiten an einem Haufen alter Rätsel (einem Trainingsdatensatz).

• Der Forscher fragt den Professor: "Wie würdest du dieses Rätsel lösen? Erkläre es mir Schritt für Schritt in normaler Sprache."
• Der Professor erklärt es: "Nun, ich sehe hier, dass man A und B vertauschen kann, ohne dass sich das Ergebnis ändert. Das ist ein wichtiger Trick!"
• Der Clou: Anstatt den Professor weiter zu nutzen, nimmt der Forscher diesen "Trick" (z. B. "Vertauschen von A und B"), schreibt ihn als eine offizielle, mathematisch korrekte Regel (ein Lemma) auf und fügt sie in den Werkzeugkasten des Handwerkers ein.

Das passiert einmalig offline. Der Professor wird danach nicht mehr gebraucht.

Schritt 2: Die Online-Arbeit (Der Handwerker allein)

Jetzt kommt ein neues, schwieriges Rätsel.

• Der Handwerker (CoqHammer) schaut in seinen Werkzeugkasten.
• Dank Strat2Rocq liegen dort jetzt die "gestohlenen" Tricks des Professors als offizielle Regeln.
• Der Handwerker nutzt diese neuen Regeln, löst das Rätsel erfolgreich und das alles ohne den Professor, ohne Internet und ohne hohe Kosten.

Ein konkretes Beispiel aus dem Papier

Stell dir vor, du hast einen Satz mit vielen Buchstaben: A + B + C.

• Der Handwerker müsste vielleicht Schritt für Schritt beweisen, dass A + B dasselbe ist wie B + A, und dann + C hinzufügen. Das dauert lange und er stolpert vielleicht.
• Der Professor würde sofort sagen: "Hey, das ist doch nur eine Umstellung! Das Ergebnis ist immer gleich, egal wie du die Buchstaben mischst."
• Strat2Rocq hat diesen "Aha-Moment" des Professors eingefangen, in eine Regel umgewandelt und dem Handwerker gegeben. Jetzt sieht der Handwerker sofort: "Ah, ich darf die Buchstaben mischen!" und löst das Problem in Sekunden.

Was hat das gebracht? (Die Ergebnisse)

Die Forscher haben das an echten Software-Projekten getestet:

1. Der Handwerker wurde stärker: CoqHammer konnte 13,41 % mehr Rätsel lösen als vorher. Er hat quasi den "Intelligenz-Boost" des Professors bekommen, ohne ihn zu bezahlen.
2. Sogar der Professor profitiert: Wenn man diese neuen Regeln auch dem Professor gibt, wird er noch besser (plus 4 %), weil er jetzt auf seine eigenen "Notizen" zugreifen kann.
3. Sicherheit: Da der Handwerker nun allein arbeitet, bleiben geheime Firmenpläne sicher im eigenen Computer.

Zusammenfassung in einem Satz

Die Forscher haben einen Weg gefunden, die genialen, aber teuren "Intuitionen" einer KI zu entlarven, sie in handliche, sichere Regeln zu verwandeln und diese dann einem schnellen, kostenlosen Computer-Programm zu geben, damit dieses Programm plötzlich fast so schlau ist wie die KI selbst.

Es ist, als würde man einem schnellen Rennwagen (dem Handwerker) den Fahrplan eines erfahrenen Rallye-Fahrers (der KI) in den Tank füllen, damit er schneller ans Ziel kommt, ohne dass der Rallye-Fahrer selbst am Steuer sitzen muss.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers" auf Deutsch:

Titel: Beweisstrategie-Extraktion aus LLMs zur Verbesserung symbolischer Beweiser

1. Problemstellung

Die formale Verifikation von Software mittels interaktiver Theorembeweiser (ITP) wie Rocq (früher Coq) ist entscheidend für die Sicherheit kritischer Systeme. Allerdings ist das Schreiben formaler Beweise extrem arbeitsintensiv.

• Herausforderung: Während Large Language Models (LLMs) in der Beweisautomatisierung Fortschritte gezeigt haben, sind hybride Ansätze (LLM-Agenten), die LLMs online nutzen, oft teuer, rechenintensiv und bergen Sicherheitsrisiken (z. B. bei proprietärem Code).
• Lücke: Reine symbolische Beweiser (wie CoqHammer) sind kosteneffizient und sicher, aber oft weniger leistungsfähig als LLMs, da ihnen bestimmte heuristische Strategien fehlen.
• Forschungsfrage: Können die internen Beweisstrategien von LLMs extrahiert und formalisiert werden, um die Fähigkeiten rein symbolischer Beweiser zu verbessern, ohne dass LLMs während des eigentlichen Beweisens benötigt werden?

2. Methodik: Das Framework Strat2Rocq

Die Autoren stellen Strat2Rocq vor, ein zweistufiges Framework, das LLM-Wissen in für symbolische Beweiser nutzbare Lemmas überführt.

Stufe 1: Offline-Lemma-Mining (Extraktion)
In dieser einmalig durchgeführten Phase werden Beweisstrategien aus einem Trainingsdatensatz (einer Sammlung von Theoremen) extrahiert:

1. Natürlichsprachliche Beweisgenerierung (NL): Für jedes Theorem wird ein LLM (z. B. Claude 3.7 Sonnet) aufgefordert, einen schrittweisen Beweis in natürlicher Sprache zu erstellen. Dies spiegelt die interne Denkweise des LLM wider.
2. Generalisierung und Formalisierung: Das LLM wird angewiesen, die einzelnen Schritte des NL-Beweises zu generalisieren und in formale Lemmas (in der Sprache Rocq) zu übersetzen.
   • Herausforderung: LLMs machen Fehler. Daher wird ein Proof-Agent eingesetzt, der iterativ Fehler in den generierten Lemmas und deren Beweisen korrigiert (Autoformalisierung).
   • Ergebnis: Ein Satz neuer, verifizierter Lemmas, die die „Intuition" oder Strategien des LLM kodieren.

Stufe 2: Online-Theorembeweis (Anwendung)

• Wenn ein neues Theorem bewiesen werden soll, werden die extrahierten Lemmas in den Beweis-Kontext eingefügt.
• Der reine symbolische Beweiser CoqHammer nutzt diese zusätzlichen Lemmas, um das Theorem zu beweisen.
• Wichtig: In dieser Phase wird kein LLM mehr benötigt. Der Prozess ist rein symbolisch, schnell und sicher. CoqHammer nutzt einen KNN-basierten Mechanismus, um aus dem großen Kontext der neuen Lemmas die relevantesten auszuwählen, ohne die Effizienz zu beeinträchtigen.

3. Schlüsselbeiträge

1. Neues Forschungsparadigma: Die Idee, LLM-Strategien offline zu extrahieren und als formale Lemmas in symbolische Beweiser zu integrieren, anstatt LLMs online zu nutzen.
2. Strat2Rocq Framework: Eine konkrete Implementierung, die NL-Beweise analysiert, generalisiert und in verifizierbare Rocq-Lemmas umwandelt.
3. Empirische Validierung: Umfassende Evaluation auf Open-Source-Projekten, die zeigt, dass diese Methode die Erfolgsrate symbolischer Beweiser signifikant steigert.
4. Dualer Nutzen: Die extrahierten Lemmas verbessern nicht nur symbolische Beweiser, sondern auch LLM-Agenten (durch Retrieval-Augmented Generation).

4. Ergebnisse und Evaluation

Die Evaluation erfolgte auf einem Datensatz von 2.394 Theoremen aus Projekten wie CompCert, Coq-Art, Ext-Lib und Vfa.

• Verbesserung symbolischer Beweiser (CoqHammer):

  • Die Erfolgsrate von CoqHammer stieg im Durchschnitt um 13,41 %.
  • Bei CompCert (einem zertifizierten C-Compiler) war der Anstieg mit 17,75 % am höchsten.
  • Die extrahierten Lemmas halfen CoqHammer, Theoreme zu beweisen, die sonst Induktion erfordert hätten (die CoqHammer nicht unterstützt), indem sie Induktion durch äquivalente Lemmas umgingen.

• Robustheit und Generalisierung:

  • Das System funktioniert auch mit anderen Backend-LLMs (z. B. o3-mini), wobei die Kombination von Strategien verschiedener Modelle zu noch besseren Ergebnissen führt.
  • Ein Ablationsstudie zeigte, dass der Schritt der natürlichsprachlichen Beweisgenerierung essenziell ist: Ohne diesen Schritt sank die Anzahl der extrahierten Lemmas um 63,56 % und die Beweisleistung um 6,21 %.

• Einfluss auf LLM-Agenten:

  • Auch LLM-Agenten profitierten von den extrahierten Lemmas (Steigerung der Erfolgsrate um 4,00 %).
  • Zudem reduzierte sich der Token-Verbrauch der Agenten, da CoqHammer mehr Theoreme eigenständig lösen konnte.

5. Bedeutung und Fazit

• Sicherheit und Effizienz: Strat2Rocq ermöglicht es, die Stärken von LLMs (Heuristiken, Mustererkennung) in sicheren, kostengünstigen und lokal ausführbaren symbolischen Systemen zu nutzen. Dies ist besonders für sicherheitskritische Anwendungen mit begrenzten Budgets oder strengen Datenschutzanforderungen relevant.
• Interpretierbarkeit von LLMs: Das Projekt bietet einen neuen Weg, um zu verstehen, wie LLMs Beweise führen. Indem man ihre Strategien in symbolische Lemmas übersetzt, erhält man eine interpretierbare Repräsentation ihres „Wissens".
• Zukunft: Die Arbeit legt den Grundstein für hybride Systeme, bei denen LLMs als „Lehrer" fungieren, die symbolische Beweiser trainieren, welche dann autonom und effizient arbeiten.

Zusammenfassend demonstriert das Paper, dass die Extraktion von Beweisstrategien aus LLMs eine vielversprechende Methode ist, um die Grenzen reiner symbolischer Beweiser zu überwinden, ohne die Nachteile des direkten LLM-Einsatzes in Kauf nehmen zu müssen.