On Multi-Step Theorem Prediction via Non-Parametric Structural Priors

Die Arbeit stellt einen trainingsfreien Ansatz zur mehrstufigen Theoremvorhersage vor, der durch die Nutzung von Theorem-Vorranggraphen als nicht-parametrische strukturelle Priors das Problem des „Structural Drift" bei In-Context-Learning adressiert und auf dem FormalGeo7k-Benchmark eine Genauigkeit von 89,29 % erreicht, die mit überwachtem State-of-the-Art vergleichbar ist.

Das Wesentliche

🧠 Das Problem: Der KI-Verlierer im Labyrinth

Stell dir vor, du hast einen sehr klugen, aber etwas chaotischen Freund (eine Künstliche Intelligenz oder KI), der dir helfen soll, ein riesiges Labyrinth zu durchqueren. Das Ziel ist es, von Punkt A zu Punkt B zu kommen, indem du eine Reihe von Türen (Satzbeweise) öffnest.

Das Problem ist: Je tiefer du in das Labyrinth kommst (je mehr Schritte du brauchst), desto mehr verirrt sich dein Freund.

• Der "Struktur-Drift": Zu Beginn weiß er noch, wo er hin muss. Aber nach 5 oder 6 Schritten vergisst er die Regeln. Er beginnt, Türen zu öffnen, die gar nicht passen, oder er läuft in leere Gänge. Er verliert den Überblick über die "Topologie" – also die logische Reihenfolge, wie Dinge zusammenhängen.
• Das Ergebnis: Bei einfachen Aufgaben ist er super. Bei komplexen Aufgaben (mit vielen Schritten) scheitert er fast immer, weil er einfach zu viele Möglichkeiten hat und keine Ahnung, welche als Nächstes sinnvoll ist.

💡 Die Lösung: Der "Bauplan" (Pri-TPG)

Die Autoren des Papiers haben eine geniale Idee entwickelt, um diesem Freund zu helfen, ohne ihn neu zu unterrichten (kein "Training" nötig). Sie nennen ihre Methode Pri-TPG.

Stell dir das so vor:

1. Die Bibliothek der Lösungen (Der Wissensschatz):
   Statt dass der Freund alles aus dem Kopf raten muss, schauen sie in ein riesiges Archiv von bereits gelösten Labyrinthen. Sie fragen sich: "Welche Türen wurden in ähnlichen Labyrinthen zuerst geöffnet?"

2. Der "Vorfahren-Baum" (Theorem Precedence Graph):
   Das ist das Herzstück. Sie zeichnen einen Baum, der zeigt, welche Türen vorher geöffnet werden müssen, damit eine andere Tür überhaupt aufgeht.

   • Analogie: Du kannst nicht den "Schlüssel zum Keller" benutzen, bevor du die "Tür zum Haus" geöffnet hast. Der Baum zeigt genau diese Reihenfolge.
   • Wenn der Freund jetzt im Labyrinth steht, schaut er nicht auf alle 300 möglichen Türen, sondern nur auf die 30 Türen, die laut diesem Baum jetzt gerade erlaubt sind. Das ist wie ein Wegweiser, der alle Sackgassen sofort absperrt.

3. Der "Schnelle Blick" (Retrieval-Augmented):
   Bevor der Freund einen Schritt macht, sucht das System schnell nach ähnlichen Problemen in der Bibliothek. Es sagt: "Hey, bei diesem Problem hier haben wir immer erst die 'Winkel-Tür' geöffnet, bevor wir zur 'Längen-Tür' gegangen sind."
   Das System passt den Wegweiser also dynamisch an das aktuelle Problem an.

4. Der "Korrektur-Check" (Symbolischer Executor):
   Der Freund (die KI) schlägt einen Schritt vor. Ein strenger, aber schneller "Prüfer" (ein Computerprogramm) sagt sofort: "Nein, das geht nicht, die Voraussetzungen sind noch nicht erfüllt."
   Dank des Wegweisers muss der Freund nicht raten, sondern wählt nur aus den wenigen, gültigen Optionen. Wenn er einen Fehler macht, wird er sofort korrigiert, bevor er sich im Labyrinth verirrt.

🏆 Das Ergebnis: Warum ist das so toll?

• Kein neues Lernen nötig: Die KI muss nicht wochenlang trainiert werden. Sie nutzt einfach die alten Lösungen als "Stützpfeiler".
• Super-Leistung: Auf dem Test "FormalGeo7k" (eine Art Mathe-Olympiade für Geometrie) erreichte diese Methode 89,29 % Erfolg.
  • Die "dumme" KI ohne Wegweiser hatte nur 26 % Erfolg (und bei schweren Aufgaben fast 0 %).
  • Selbst die besten, trainierten KI-Modelle kamen nicht ganz an dieses Ergebnis heran.
• Skalierbarkeit: Je schwieriger das Problem wird, desto mehr hilft der Wegweiser. Er verhindert, dass die KI in der Flut der Möglichkeiten ertrinkt.

🎯 Die große Metapher

Stell dir vor, du musst einen komplexen Bauklotz-Turm bauen.

• Ohne Methode (Vanilla ICL): Du hast einen Korb mit 10.000 Steinen. Du wirfst sie wild aufeinander und hoffst, dass der Turm steht. Bei kleinen Türmen klappt es. Bei hohen Türmen stürzt er sofort ein.
• Mit Pri-TPG: Du hast eine Bauanleitung, die dir sagt: "Nimm nur diese 5 Steine, die jetzt passen. Und du musst zuerst den roten Stein legen, bevor der blaue kommt."
  Du musst nicht raten. Du baust Schritt für Schritt, und der Turm steht stabil, egal wie hoch er wird.

Zusammenfassend: Die Autoren haben gezeigt, dass man KI nicht zwingen muss, alles auswendig zu lernen. Wenn man ihr stattdessen eine klare Struktur und logische Regeln gibt, die sie aus der Vergangenheit lernt, kann sie schwierige Probleme lösen, ohne dass man sie mühsam neu trainieren muss. Es ist der Unterschied zwischen blindem Raten und klugem Planen.

Technische Zusammenfassung

1. Problemstellung

Die Vorhersage von mehrstufigen Theoremen ist eine zentrale Herausforderung im automatisierten logischen Schließen, insbesondere in der Geometrie.

• Herausforderung: Herkömmliche neuronale-symbolische Ansätze verlassen sich stark auf überwachte, parametrische Modelle. Diese zeigen eine begrenzte Generalisierungsfähigkeit gegenüber sich entwickelnden Theorembibliotheken und erfordern kostspieliges Nachtrainieren bei neuen Datensätzen.
• Das Phänomen „Structural Drift" (Strukturelle Drift): Die Autoren identifizieren ein kritisches Skalierungsproblem beim Einsatz von In-Context Learning (ICL) mit Large Language Models (LLMs). Mit zunehmender Tiefe der Beweisführung (Anzahl der benötigten Theoreme) bricht die Leistung von „Vanilla ICL" (einfaches ICL ohne zusätzliche Struktur) drastisch ein und fällt oft auf nahe Null.
• Ursache: LLMs scheitern daran, latente topologische Abhängigkeiten zwischen Theoremen zu erkennen. Sie führen eine unstrukturierte Exploration durch, da die Wahrscheinlichkeitsverteilung über den Theoremraum nahezu uniform wird, was zu kumulativen Fehlern in langen Beweispfaden führt.

2. Methodik: Pri-TPG

Die Autoren schlagen Pri-TPG (Prior-guided multi-step theorem prediction via Theorem Precedence Graphs) vor. Dies ist ein trainingsfreier (training-free) Ansatz, der LLMs als strukturierte Planer nutzt, ohne Gradienten-basierte Optimierung.

Der Ansatz besteht aus drei Hauptkomponenten:

A. Theorem Precedence Graphs (TPG)

Anstatt Theoreme als unstrukturierte Klassifikationsaufgabe zu betrachten, wird ein gerichteter Graph $G = (V, E)$ erstellt, der die zeitlichen und logischen Abhängigkeiten zwischen Theoremen kodiert.

• Ein Knoten repräsentiert ein Theorem.
• Eine Kante $u \to v$ existiert, wenn die Schlussfolgerung von Theorem $u$ eine notwendige Voraussetzung für die Anwendung von Theorem $v$ ist.
• Dieser Graph dient als explizite strukturelle Priori, die den Suchraum effektiv beschneidet.

B. Query-Adaptive Prior (Multimodales Retrieval)

Da die Abhängigkeiten kontextsensitiv sind, wird für jede neue Problemstellung ein spezifischer Graph konstruiert:

1. Retrieval: Ein multimodaler Encoder (Text, Diagramm, formale Zustände) sucht in einer Datenbank historischer Lösungen nach den $K$ ähnlichsten Problemen.
2. Graph-Konstruktion: Aus den Lösungen dieser ähnlichen Probleme wird ein lokaler, abfrage-spezifischer TPG ($G_q$) synthetisiert. Dies reduziert den Suchraum von der gesamten Bibliothek auf einen relevanten Kandidatensatz.

C. State-Aware Prior & Symbolic Execution

Der Prozess ist iterativ und nicht einmalig (Single-Pass):

1. Symbolic Pruning: Ein symbolischer Solver prüft zu jedem Schritt $t$, welche der retrierten Kandidaten-Theoreme tatsächlich auf den aktuellen formalen Zustand $S_t$ anwendbar sind (Präbedingungen erfüllen).
2. Strukturelle Lokalisierung: Der Graph wird dynamisch eingeschränkt; nur Nachfolger des zuletzt angewendeten Theorems werden betrachtet.
3. Priorisierung: Ein Scoring-Funktion $\Psi(v)$ bewertet Kandidaten basierend auf:
   • Zielorientierung (semantische Ähnlichkeit zum Beweisziel).
   • Graph-Struktur (Förderung direkter Nachfolger im TPG).
   • Historie (Bestrafung bereits verwendeter Theoreme, um Schleifen zu vermeiden).
4. LLM-Planer: Das LLM erhält diese gefilterte, priorisierte Liste und wählt den nächsten Schritt aus. Ein symbolischer Solver führt den Schritt aus und liefert Feedback für den nächsten Zyklus.

3. Wichtige Beiträge

1. Identifikation von Structural Drift: Nachweis, dass reines ICL bei komplexen, mehrstufigen Beweisen aufgrund fehlender topologischer Guidance versagt.
2. Pri-TPG Framework: Entwicklung eines nicht-parametrischen Ansatzes, der historische Lösungspfade in gerichtete Graphen (TPG) umwandelt, um LLMs ohne Training zu führen.
3. Kombination aus Retrieval und Struktur: Überwindung des reinen RAG (Retrieval-Augmented Generation) durch die Einführung von Struktur in die retrierte Information (nicht nur Text, sondern Abhängigkeitsgraphen).
4. Training-Freiheit: Das System passt sich sofort neuen Theorembibliotheken an, da es keine Gewichts-Updates des LLMs erfordert.

4. Ergebnisse

Die Methode wurde auf dem FormalGeo7k-Benchmark (sowie Geometry3K und GeoQA) evaluiert.

• Gesamtleistung: Pri-TPG erreicht eine Genauigkeit von 89,29 % auf FormalGeo7k.
• Vergleich:
  • Deutlich besser als reine LLM-Lösungen (Vanilla ICL fällt bei tiefen Beweisen auf ~0 %; GPT-5.2 im Direct-Solve erreicht nur 73,14 %).
  • Übertrifft die besten trainierten neuronal-symbolischen Baselines (z. B. FGeo-HyperGNet mit 88,36 %).
  • Besonders stark bei mittleren Schwierigkeitsgraden (L1–L3), wo die Genauigkeit nahe 100 % liegt.
• Ablationsstudien:
  • Ohne TPG (nur RAG) fällt die Genauigkeit auf 72,64 %.
  • Ohne iterative symbolische Rückkopplung (Single-Pass) bricht die Leistung bei schwierigen Problemen komplett ein (0 %).
  • Die schrittweise Verfeinerung der Priors (Global $\to$ Query-Adaptive $\to$ State-Aware) verbessert die Leistung systematisch.

5. Bedeutung und Ausblick

• Skalierbarkeit: Der Ansatz bietet einen vielversprechenden Weg, um LLM-basiertes symbolisches Schließen zu skalieren, indem er den kombinatorischen Suchraum durch explizite topologische Priors drastisch reduziert.
• Paradigmenwechsel: Statt auf teures Fine-Tuning zu setzen, nutzt das System strukturelle Induktion aus historischen Daten. Dies ermöglicht sofortige Anpassung an neue Theorembibliotheken.
• Anwendung: Besonders relevant für Bildungssysteme (Tutoring), wo nachvollziehbare, korrekte und überprüfbare Lösungspfade benötigt werden, ohne dass das System ständig neu trainiert werden muss.
• Limitationen: Die Effizienz hängt von der Anzahl der LLM-Aufrufe ab (Rechenkosten). Bei extrem langen Beweisen (Schwierigkeitsgrad L6) bleibt noch eine Lücke zu spezialisierten, trainierten Architekturen, da der TPG primär lokale Abhängigkeiten und weniger globale Tiefe kodiert.

Zusammenfassend demonstriert das Paper, dass die Kombination aus Retrieval, symbolischer Validierung und expliziten strukturellen Priors (Theorem Precedence Graphs) eine leistungsstarke Alternative zu rein parametrischen Modellen für komplexes logisches Schließen darstellt.