Can LLM Aid in Solving Constraints with Inductive Definitions?

Die vorgestellte Arbeit demonstriert, dass ein neuro-symbolischer Ansatz, der Large Language Models zur Generierung von Hilfslemmata mit Constraint-Lösern kombiniert, die Erfolgsrate beim Lösen von Induktionsdefinitionen um etwa 25 % gegenüber dem aktuellen Stand der Technik steigert.

Das Wesentliche

Stellen Sie sich vor, Sie versuchen, ein sehr komplexes mathematisches Rätsel zu lösen. Dieses Rätsel basiert auf rekursiven Regeln – also Regeln, die sich selbst wiederholen, wie eine russische Matrjoschka-Puppe, die immer kleinere Puppen in sich hat. In der Informatik nennt man das „induktive Definitionen". Sie sind überall: in Programmiersprachen, bei der Überprüfung von Software-Sicherheit und in der Mathematik.

Das Problem? Herkömmliche Computer-Programme (die sogenannten „Solver" oder „Beweiser") sind wie extrem schnelle, aber sehr starre Rechenmaschinen. Sie können einfache Schritte gut, aber wenn das Rätsel zu viele verschachtelte Schichten hat, kommen sie oft ins Stocken. Sie wissen nicht, welche zusätzlichen Zwischenschritte sie brauchen, um das große Ziel zu erreichen.

Hier kommt die Idee dieses Papers ins Spiel: Künstliche Intelligenz (LLMs) als kreativer Assistent für den starren Rechner.

Die Hauptakteure

1. Der Starre Rechner (SMT-Solver): Stellen Sie sich diesen als einen extrem disziplinierten, aber etwas sturen Mathematiklehrer vor. Er prüft jede Aussage auf logische Richtigkeit. Wenn ihm aber ein wichtiger Hinweis fehlt, gibt er auf und sagt: „Ich kann das nicht beweisen."
2. Der Kreative Assistent (LLM): Das ist wie ein erfahrener, aber manchmal etwas träumerischer Mentor. Er kann Ideen haben, Muster erkennen und sagen: „Hey, vielleicht hilft es, wenn wir hier noch diese eine kleine Regel hinzufügen?" Aber er macht auch Fehler, halluziniert manchmal Dinge, die nicht stimmen, oder schlägt Ideen vor, die zwar richtig, aber für das aktuelle Rätsel nutzlos sind.

Die Lösung: Ein Team aus Traum und Logik

Die Autoren haben ein System namens LLM4Ind entwickelt, das diese beiden Welten vereint. Es funktioniert wie ein gut koordiniertes Duo bei einer Detektivarbeit:

Schritt 1: Die Idee (Der Kreative)

Der Rechner stößt an eine Wand. Also ruft er den kreativen Assistenten (das LLM) zu Hilfe.

• Das Problem: Wenn man dem Assistenten einfach nur sagt: „Gib mir eine Idee!", wirft er oft dumme oder falsche Ideen raus.
• Die Lösung: Die Autoren haben dem Assistenten spezielle Anweisungen (Prompts) gegeben. Sie sagen ihm nicht nur „Löse das", sondern zeigen ihm, wie ein Mensch denken würde: „Schau dir die Basis an, dann den nächsten Schritt, und überlege, was fehlt, um von A nach B zu kommen."
• Die Analogie: Statt dem Assistenten blind zu vertrauen, geben ihm die Autoren eine Landkarte und einen Kompass, damit er gezielt nach den fehlenden Puzzleteilen sucht.

Schritt 2: Der Filter (Der Skeptiker)

Der Assistent wirft nun eine Handvoll Ideen (Konjekturen) auf den Tisch.

• Das Problem: Manche Ideen sind Unsinn (falsch), manche sind zwar wahr, aber helfen bei diesem spezifischen Rätsel nicht (nutzlos), und manche sind gut, aber der Rechner kann sie noch nicht sofort beweisen.
• Die Lösung: Bevor der Rechner Zeit verschwendet, prüft ein schneller Filter: „Ist das überhaupt möglich? Stimmt das mit den Grundregeln überein?" Wenn die Idee offensichtlich falsch ist, wird sie sofort verworfen. Das spart Zeit.

Schritt 3: Die Validierung (Der Richter)

Was übrig bleibt, sind vielversprechende Ideen.

• Der Rechner nimmt diese Ideen und prüft: „Wenn ich diese neue Regel hinzufüge, kann ich dann das ursprüngliche Rätsel lösen?"
• Wenn ja: Super! Die Idee wird als „Hilfssatz" (Lemma) akzeptiert.
• Wenn nein: Vielleicht ist die Idee selbst zu schwer zu beweisen. Dann wird sie als neues kleines Rätsel behandelt, und der Prozess beginnt von vorne (rekursiv), bis alles geklärt ist.

Warum ist das wichtig?

Bisher konnten die besten Computer-Programme nur etwa 75 % solcher komplexen, rekursiven Rätsel lösen. Mit diesem neuen Ansatz, der die Kreativität der KI mit der Strenge der Logik verbindet, konnten sie rund 25 % mehr Rätsel lösen.

Zusammenfassend:
Stellen Sie sich vor, Sie bauen ein riesiges Schloss aus Legosteinen. Der Computer ist gut darin, Steine zu stapeln, aber er weiß nicht, welche speziellen Verbindungsteile er braucht, um die Turmspitze zu erreichen. Der KI-Assistent schlägt vor: „Vielleicht brauchen wir hier ein rotes Zahnrad!" Der Computer prüft sofort: „Passt das? Ja? Dann bauen wir weiter." Ohne den KI-Assistenten würde der Computer ratlos vor dem fehlenden Teil stehen. Ohne den Computer würde der KI-Assistent vielleicht ein Zahnrad aus Zucker vorschlagen, das sofort zerfällt. Zusammen bauen sie das Schloss.

Das Paper zeigt also, dass wir KI nicht ersetzen, sondern verstärken müssen, um komplexe logische Probleme zu lösen, die für reine Computer zu schwer und für reine Menschen zu zeitaufwendig sind.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Can LLM Aid in Solving Constraints with Inductive Definitions?" auf Deutsch:

1. Problemstellung

Das Lösen von Constraints, die induktive (rekursive) Definitionen beinhalten, ist eine der größten Herausforderungen in der automatisierten Programverifikation. Solche Definitionen treten häufig in Form von Algebraischen Datentypen (ADTs) und rekursiv definierten Funktionen (RDFs) auf.

• Limitationen bestehender Werkzeuge: State-of-the-Art SMT-Solver (wie cvc5) und First-Order-Logic-Theorembeweiser (wie Vampire) bieten nur begrenzten Support für solche Constraints. Oft scheitern sie daran, dass für den Beweis einer Eigenschaft zusätzliche Hilfssätze (Auxiliary Lemmas) notwendig sind, die weder aus den Axiomen noch aus der Induktionshypothese direkt ableitbar sind.
• Schwächen traditioneller Methoden: Bestehende Ansätze zur automatischen Lemma-Generierung (z. B. Theorie-Exploration, Generalisierung oder CHC-basierte Methoden) leiden unter begrenzter Skalierbarkeit, mangelnder Ausdruckskraft oder der Unfähigkeit, komplexe rekursive Funktionen effektiv zu handhaben.
• Herausforderung mit LLMs: Große Sprachmodelle (LLMs) zeigen zwar Potenzial im Code- und Beweisgenerierung, leiden jedoch unter Zufälligkeit, Halluzinationen und mangelnder Spezifität für induktive Reasoning-Aufgaben, wenn sie nicht gezielt gesteuert werden.

2. Methodik: Ein Neuro-Symbolischer Ansatz

Die Autoren schlagen einen hybriden, neuro-symbolischen Ansatz vor, der die generativen Fähigkeiten von LLMs mit der rigorosen Validierung durch symbolische Constraint-Löser (SMT) kombiniert. Der Workflow besteht aus drei Hauptphasen: Query (Abfrage), Filter und Validate (Validierung).

A. Workflow (Algorithmus)

Der Prozess wird durch die Funktion ProveRun gesteuert, die rekursiv aufgerufen wird:

1. Initialprüfung: Der SMT-Solver versucht zunächst, das Ziel ohne Hilfssätze zu beweisen.
2. LLM-Abfrage: Falls dies fehlschlägt, werden strukturierte Prompts an das LLM gesendet, um eine Menge von Konjekturen (Kandidaten-Hilfssätzen) zu generieren.
3. Filterung (Filter Stage): Das LLM generiert oft falsche oder unnütze Aussagen. Ein schneller Filter (unter Verwendung des SMT-Solvers mit kurzer Zeitbegrenzung) eliminiert:
   • Syntaxfehler.
   • Aussagen, die identisch mit dem Beweisziel sind (unhilfreich).
   • Inkonsistente Aussagen (die den Axiomen widersprechen).
4. Validierung (Validate Stage):
   • Nützlichkeitstest: Der Solver prüft, ob die gefilterten Konjekturen zusammen mit den Axiomen das ursprüngliche Ziel beweisen ($A \land \bigwedge L_i \to P$).
   • Rekursive Verifikation: Wenn die Konjekturen das Ziel beweisen, werden sie als neue Unterziele behandelt. Der Prozess wird rekursiv aufgerufen, um sicherzustellen, dass diese neuen Konjekturen selbst aus den Axiomen beweisbar sind ($A \to L_i$).

B. Prompt-Strategien

Um die Qualität der LLM-Ausgaben zu verbessern, wurden zwei spezifische Strategien entwickelt:

1. Strategie 1: Gleichungs-basiertes Reasoning (Equational Reasoning):
   • Das LLM wird angewiesen, schrittweise wie ein Mensch zu reasoning.
   • Es identifiziert die induktive Definition, behandelt den Basisfall und transformiert den Induktionsschritt schrittweise unter Verwendung bekannter Axiome.
   • Wo die Transformation nicht direkt möglich ist, wird eine Konjektur generiert.
2. Strategie 2: Term-Rewriting und Generalisierung:
   • Das LLM wird ermutigt, das Beweisziel zu vereinfachen.
   • Es soll gemeinsame Terme identifizieren, diese durch neue Variablen ersetzen (Generalisierung) und stärkere Lemmas finden, die einfacher zu beweisen sind.
   • Es werden „Brücken-Lemmas" generiert, die zwischen dem vereinfachten Ziel und dem ursprünglichen Ziel vermitteln.

3. Wichtige Beiträge

• Neuro-Symbolische Integration: Erstmalige systematische Integration von LLMs in den automatischen induktiven Reasoning-Prozess, um die Lücke bei der Lemma-Generierung zu schließen.
• Strukturierte Prompts: Entwicklung von zwei spezialisierten Prompt-Strategien, die LLMs anleiten, induktive Reasoning-Muster (wie Term-Rewriting und Generalisierung) anzuwenden, anstatt nur generische Ratschläge zu geben.
• Robuster Validierungs-Workflow: Ein mehrstufiger Prozess (Filter + Validierung + Rekursion), der die inhärenten Fehlerquellen von LLMs (Halluzinationen, Zufälligkeit) durch symbolische Verifikation kompensiert.
• Tool und Benchmark: Vorstellung des Tools LLM4Ind und einer umfassenden Evaluierung auf 706 Beweisaufgaben aus etablierten Benchmarks (StandardDT, StandardDTLIA, Autoproof, IndBen).

4. Ergebnisse

Die Evaluation wurde gegen State-of-the-Art-Solver (cvc5, Vampire, Racer) durchgeführt:

• Steigerung der Erfolgsrate: LLM4Ind löste signifikant mehr Beweisaufgaben als die reinen Solver. Insgesamt wurden etwa 25 % mehr Aufgaben gelöst (525 vs. 293 für cvc5 bei 1200s Zeitlimit).
• Benchmark-Leistung:
  • Auf StandardDT (reine ADTs) löste LLM4Ind 212 von 241 Aufgaben (cvc5: 150).
  • Auf IndBen (komplexe ADTs) zeigte LLM4Ind mit stärkeren LLMs (wie GPT-5) eine deutliche Überlegenheit gegenüber Vampire.
• Robustheit: Das System war robust gegenüber verschiedenen LLM-Modellen (Qwen, DeepSeek, Gemini, GPT-5) und verschiedenen Sampling-Temperaturen. Die Varianz in der Anzahl gelöster Aufgaben war gering.
• Effizienz der Filterung: Der Filter-Modus reduzierte die Token-Kosten und die Lösungszeit, indem er unnütze Pfade frühzeitig abbrach. Ohne Filter wäre die Rechenzeit deutlich höher gewesen.
• Backend-Unabhängigkeit: Der Ansatz funktionierte sowohl mit cvc5 als auch mit Vampire als Backend-Solver, wobei die Kombination mit cvc5 aufgrund dessen besseren Supports für gemischte Theorien (ADT + LIA) leicht besser abschnitt.

5. Bedeutung und Fazit

Dieses Paper demonstriert, dass LLMs nicht nur als „Assistenten" für menschliche Benutzer, sondern als integraler Bestandteil vollständig automatisierter Beweiswerkzeuge eingesetzt werden können.

• Paradigmenwechsel: Es überwindet die Grenzen rein logischer Heuristiken, indem es die semantische Intuition von LLMs nutzt, um komplexe Lemmas zu generieren, die für traditionelle Solver zu schwer zu finden sind.
• Praktische Anwendbarkeit: Die Methode ist besonders wertvoll für die Verifikation von funktionalen Programmen und Systemen mit komplexen rekursiven Datenstrukturen, wo bisher oft manuelle Eingriffe nötig waren.
• Zukunftsperspektive: Die Arbeit legt den Grundstein für weitere Forschung in Richtung Agenten-basierter Methoden und erweiterter Prompting-Techniken für formale Verifikation.

Zusammenfassend beweist die Studie, dass die Synergie aus generativer KI und symbolischer Logik einen signifikanten Fortschritt in der automatisierten induktiven Beweisführung darstellt.