A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry

Die Studie stellt einen neuro-symbolischen Ansatz vor, der durch das Abrufen analoger Probleme und die Nutzung eines formalen Verifizierers die Fähigkeit von Large Language Models zur Erzeugung korrekter Beweise in der euklidischen Geometrie signifikant verbessert.

Das Wesentliche

Stellen Sie sich vor, Sie haben einen extrem klugen, aber etwas chaotischen Assistenten. Er kann fließend sprechen, Geschichten erfinden und sieht auf den ersten Blick alles sehr schlau aus. Das ist ein Large Language Model (LLM), wie ChatGPT oder Gemini.

Das Problem? Wenn Sie ihn bitten, einen mathematischen Beweis zu schreiben (z. B. in der Geometrie), stolpert er oft. Er versucht, die Antwort zu „erraten", indem er Muster aus seinen Trainingsdaten nachahmt, anstatt logisch zu denken. Es ist, als würde er versuchen, ein komplexes Puzzle zu lösen, indem er einfach die Teile auf den Tisch wirft und hofft, dass sie passen. Oft sieht die Lösung gut aus, ist aber mathematisch falsch.

Die Autoren dieses Papers haben eine Lösung gefunden, die sie „Neuro-Symbolisch" nennen. Lassen Sie uns das mit einer einfachen Geschichte erklären:

Die Idee: Der Assistent, der Mentor und der Prüfer

Stellen Sie sich unser System wie eine Dreier-Team vor, das gemeinsam eine schwierige Hausaufgabe löst:

1. Der Assistent (Das LLM): Das ist unser KI-Modell. Es ist kreativ und schnell, aber es braucht Hilfe, um nicht in die Irre zu gehen.
2. Der Mentor (Analoge Probleme): Bevor der Assistent überhaupt anfängt zu schreiben, schaut er in ein Archiv. Dort sucht er nach ähnlichen Aufgaben, die er schon gelöst hat.
   • Die Metapher: Stellen Sie sich vor, Sie müssen einen neuen Kuchen backen, aber Sie kennen das Rezept nicht. Der Mentor gibt Ihnen nicht das Rezept für den neuen Kuchen, sondern sagt: „Hey, hast du schon mal einen Apfelkuchen gebacken? Der war fast gleich, nur mit Birnen statt Äpfeln. Schau dir an, wie du das gemacht hast!"
   • Das System sucht also nach geometrischen Problemen, die im Aufbau gleich sind, und zeigt dem KI-Assistenten die Beweise dafür. Das gibt dem Assistenten einen festen Startpunkt.
3. Der Prüfer (Der Symbolische Verifizierer): Das ist der strenge Lehrer, der keine Fehler toleriert. Er ist kein KI-Modell, sondern ein streng logisches Computerprogramm (ein „Beweis-Checker").
   • Die Metapher: Der Assistent schreibt einen Beweisentwurf. Der Prüfer liest ihn nicht nur, sondern rechnet ihn nach. Wenn der Assistent sagt: „Winkel A ist 90 Grad", prüft der Prüfer: „Stimmt das wirklich basierend auf den anderen Winkeln?"
   • Wenn etwas falsch ist, sagt der Prüfer nicht nur „Falsch!", sondern gibt einen konkreten Hinweis: „Du hast Schritt 3 übersprungen" oder „Deine Annahme in Schritt 1 passt nicht zu Schritt 2".
   • Der Assistent nimmt diesen Hinweis, korrigiert seinen Entwurf und reicht ihn erneut ein. Dieser Kreislauf läuft so lange, bis der Beweis zu 100 % stimmt.

Was haben sie herausgefunden?

Die Forscher haben dieses System an SAT-Geometrieaufgaben getestet (das sind anspruchsvolle Schul- und Studienaufgaben).

• Ohne Hilfe: Wenn man die KI allein arbeiten lässt, scheitert sie oft. Sie liefert zwar manchmal die richtige Zahl, aber der Weg dorthin (der Beweis) ist Unsinn.
• Mit dem Team: Wenn der Assistent den Mentor (ähnliche Beispiele) und den Prüfer (Korrektur-Feedback) hat, explodiert die Erfolgsrate.
  • Bei den besten KI-Modellen (wie OpenAI's o1) stieg die Erfolgsrate um 58 % bis 70 %.
  • Das bedeutet: Aufgaben, die vorher fast unmöglich waren, werden jetzt zuverlässig gelöst.

Warum ist das so wichtig?

Bisher waren KIs wie „glänzende Blätter": Sie sahen toll aus, aber wenn man sie auf harte Fakten prüfte, bröckelten sie.

Dieser Ansatz macht die KI zuverlässig.

• Vertrauen: In Bereichen wie Medizin, Ingenieurwesen oder Sicherheit können wir uns keine „vermuteten" Antworten leisten. Wir brauchen Beweise, die zu 100 % logisch korrekt sind.
• Kosten: Durch den Mentor (die ähnlichen Beispiele) muss die KI nicht mehr das gesamte Wörterbuch aller mathematischen Sätze lesen. Sie bekommt nur die wenigen Sätze gezeigt, die sie wirklich braucht. Das spart Zeit und Geld.

Zusammenfassung in einem Satz

Die Autoren haben eine KI nicht dazu gebracht, besser zu rechnen, sondern sie mit einem Mentor (der auf ähnliche Lösungen zeigt) und einem strengen Prüfer (der jeden Schritt logisch überprüft) ausgestattet, damit sie endlich Beweise liefern kann, auf die man sich verlassen kann – genau wie ein guter Schüler, der lernt, nicht nur zu raten, sondern zu verstehen.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry" auf Deutsch.

1. Problemstellung

Große Sprachmodelle (LLMs) zeigen zwar beeindruckende Leistungen in vielen Bereichen, scheitern jedoch häufig in formalen Domänen, die rigorose logische Deduktion und symbolisches Denken erfordern, wie z. B. bei der Generierung mathematischer Beweise. Dies liegt an ihrer inhärenten Architektur, die auf probabilistischen Sequenzgenerierungen basiert, die auf statistischen Mustern aus Textdaten beruhen, anstatt auf echter logischer Konsistenz.

• Herausforderungen: Mathematische Beweise erfordern absolute Wahrheit, Abwesenheit von Ambiguitäten und eine langanhaltende logische Kohärenz, die für aktuelle LLMs schwer zu erreichen ist. Selbst oberflächliche Änderungen an Problemen führen oft zu drastischen Leistungseinbußen, was darauf hindeutet, dass LLMs eher Mustererkennung als echtes mathematisches Denken nutzen.
• Ziel: Die Entwicklung eines Systems, das LLMs befähigt, verifizierbare und korrekte formale Beweise zu generieren, um deren Zuverlässigkeit, Genauigkeit und Konsistenz zu erhöhen.

2. Methodik: Ein neuro-symbolischer Ansatz

Die Autoren schlagen einen hybriden Ansatz vor, der die generativen Stärken von LLMs mit zwei strukturierten Komponenten kombiniert: analoger Führung und symbolischer Verifikation. Das System wurde im Kontext von SAT-Level-Euklidischer Geometrie (FormalGeo-7k Datensatz) getestet.

Der Prozess gliedert sich in folgende Schritte:

A. Problemabstraktion und Analogie-Retrieval

• Abstraktion: Um strukturell ähnliche Probleme zu finden, werden Oberflächendetails (Namen von Entitäten, spezifische Zahlenwerte) durch Platzhalter (z. B. <word>, <num>) ersetzt.
• Retrieval: Basierend auf der Jaccard-Ähnlichkeit der abstrahierten Konstruktionen, Bedingungen und Ziele werden analoge Probleme aus dem Datensatz abgerufen.
• Trainiertes Regressionsmodell: Ein einfaches neuronales Netzwerk wurde trainiert, um die Ähnlichkeit von Beweisen basierend auf der strukturellen Ähnlichkeit der Probleme vorherzusagen.
• Anwendung: Die gefundenen analogen Probleme und deren vollständige formale Beweise dienen als Few-Shot-Beispiele (In-Context-Learning) für das LLM.
• Effizienzgewinn: Anstatt das gesamte Theoremdictionary (196 Theoreme) einzufügen, wird dieses auf die Theoreme reduziert, die in den analogen Beweisen vorkommen. Dies reduziert den Token-Verbrauch drastisch (von 18k auf durchschnittlich 2,5k Tokens) und verkleinert den Suchraum für das Modell.

B. LLM-Beweisgenerierung

Das LLM erhält als Prompt:

1. Das Zielproblem (Text und formale Darstellung).
2. Die top-analogen Probleme mit ihren Beweisen.
3. Das reduzierte Theoremdictionary.
   Das Modell muss einen formalen Beweis generieren, der nur die bereitgestellten Theoreme verwendet.

C. Symbolische Verifikation und Iteratives Feedback

Ein externer symbolischer Verifizierer (basierend auf dem Z3-Theorembeweiser und SMT-Lösern) überprüft den generierten Beweis:

• Funktionsweise: Der Verifizierer kodiert Beweisschritte und geometrische Constraints als logische Formeln und prüft deren Konsistenz. Er kennt die Lösung nicht, sondern prüft, ob die Antwort aus den Beweisbedingungen logisch folgt.
• Iterativer Loop: Wenn der Beweis fehlerhaft ist, gibt der Verifizierer strukturiertes Feedback zurück. Das LLM nutzt dieses Feedback, um den Beweis in einer neuen Iteration zu korrigieren (bis zu 5 Versuche pro Lauf).
• Fehlerkategorien:
  1. Syntaxverletzung: Ungültige Theoremaufrufe.
  2. Prämissenverletzung: Theoreme werden aufgerufen, ohne dass die Voraussetzungen bewiesen wurden.
  3. Ziel nicht erreicht: Der Beweis ist fehlerfrei, führt aber nicht zum Ziel oder liefert eine falsche numerische Antwort.

3. Wichtige Beiträge

1. Neuro-symbolisches System: Ein Framework, das LLMs durch analoge Führung und Verifikationsfeedback bei der Beweisgenerierung unterstützt.
2. Spezialisierter Verifizierer: Ein auf Geometrieprove zugeschnittener symbolischer Verifizierer, der den gesamten Beweis und nicht nur das Endergebnis evaluiert.
3. Kostenreduktion: Durch die Fokussierung auf relevante Theoreme aus analogen Problemen wird der Kontext drastisch verkleinert.
4. Reproduzierbarkeit: Code und Daten werden veröffentlicht.

4. Ergebnisse

Die Methode wurde auf dem FormalGeo-7k Datensatz (50 Stichprobenprobleme über 5 Schwierigkeitsstufen) mit OpenAI's o1 und Gemini-2.5-Flash getestet.

• Leistungssteigerung:
  • OpenAI o1: Die Genauigkeit stieg von 10% (Basis-Modell) auf 80% (vollständiger Pipeline mit Analogie, Verifizierer und mehreren Läufen). Das entspricht einem Gewinn von 58–70%.
  • Gemini-2.5-Flash: Die Genauigkeit stieg von 22% auf 86% (Gewinn von 52–64%).
• Beitrag der Komponenten:
  • Analogie-Retrieval: Alleinige Nutzung von Analogien (ohne Verifizierer) erhöhte die Genauigkeit von 10% auf 48%.
  • Verifizierer-Feedback: Iteratives Korrigieren durch Feedback steigerte die Leistung weiter signifikant (ca. +20% bis +30% je nach Modell und Setting).
  • Mehrere Läufe: Mehrere unabhängige Versuche pro Problem brachten zusätzliche Gewinne, besonders bei schwierigen Problemen.
• Genauigkeit vs. Richtigkeit: Während das Basis-Modell oft die richtige numerische Antwort fand, scheiterte es häufig am korrekten Beweis. Die vorgeschlagene Methode erreichte bei korrekten Antworten eine Beweis-Genauigkeit von 80% (vs. 57,7% beim Basis-Modell).
• Fehleranalyse: Die Methode reduzierte Fehler in allen Kategorien (Syntax, Prämissen, Zielverfehlung) im Vergleich zum Basis-Modell. Syntaxfehler waren am häufigsten, wurden aber durch Feedback schnell behoben.

5. Bedeutung und Ausblick

Dieses Paper demonstriert, dass die Kombination von LLMs mit symbolischen Werkzeugen und analogem Denken die Zuverlässigkeit von KI in kritischen Anwendungen (Mathematik, Wissenschaft, Sicherheit) erheblich steigern kann.

• Vertrauenswürdigkeit: Die Fähigkeit, provable korrekte Schlussfolgerungen zu generieren, ist entscheidend für den Einsatz in sicherheitskritischen Systemen.
• Skalierbarkeit: Der Ansatz ist nicht auf Geometrie beschränkt, sondern kann auf andere Domänen übertragen werden, die SMT-basierte Verifikation unterstützen.
• Zukünftige Arbeit: Die Autoren planen, den Ansatz auf dynamische Systeme (mittels temporaler Logik) zu erweitern und die Analogie-Retrieval-Mechanismen zu verfeinern.

Zusammenfassend zeigt die Studie, dass neuro-symbolische Ansätze die Lücken der reinen probabilistischen Modelle schließen und LLMs zu verlässlichen Werkzeugen für formale Deduktion machen können.