LeanTutor: Towards a Verified AI Mathematical Proof Tutor

Die Arbeit stellt LeanTutor vor, ein Beweis-tutor-System, das die Stärken von Large Language Models und dem Theorembeweiser Lean kombiniert, um mathematische Beweise in natürlicher Sprache zu erklären und gleichzeitig formale Korrektheit zu gewährleisten, wobei die Leistung anhand des neu eingeführten PeanoBench-Datensatzes evaluiert wird.

Das Wesentliche

Stell dir vor, du lernst Mathe, und zwar nicht nur das Rechnen, sondern das Beweisen von Sätzen – also das logische Herleiten, warum etwas wahr ist. Das ist oft schwer.

In der Vergangenheit gab es zwei extreme Möglichkeiten, dir dabei zu helfen:

1. Der „Allwissende Chatbot" (LLM): Wie ein sehr gesprächiger, aber manchmal etwas verwirrter Freund. Er redet fließend mit dir, erklärt Dinge in einfacher Sprache, aber er macht oft Fehler, erfindet Fakten oder gibt dir einfach die ganze Lösung vor, statt dir zu helfen, sie selbst zu finden.
2. Der „Strenge Roboter" (Theorem Prover): Wie ein extrem präziser, aber sehr steifer Lehrer, der nur eine sehr spezielle, komplizierte Geheimsprache versteht. Er kann dir zu 100 % garantieren, dass dein Beweis richtig ist, aber wenn du einen kleinen Tippfehler machst oder eine andere Formulierung wählst, gibt er dir nur einen kryptischen Fehlercode zurück und hilft dir nicht weiter.

LeanTutor ist der Versuch, das Beste aus beiden Welten zu vereinen. Es ist wie ein hybrider Mathe-Tutor, der die Sprache des Chatbots spricht, aber das Gehirn des Roboters nutzt.

Hier ist, wie das funktioniert, erklärt mit ein paar einfachen Analogien:

Das Team hinter LeanTutor

Stell dir LeanTutor als ein kleines Team aus drei Spezialisten vor, die an einem Tisch sitzen:

1. Der Dolmetscher (Autoformalizer):

   • Die Aufgabe: Der Schüler schreibt seinen Beweis in normaler, deutscher Sprache (z. B. „Ich nehme an, dass..."). Der Dolmetscher übersetzt diesen Satz sofort in die strenge Geheimsprache des Roboters (Lean).
   • Das Problem: Wenn der Schüler einen Fehler macht, versteht der Roboter das nicht. Der Dolmetscher muss also genau hinsehen und prüfen: „Habe ich das, was der Schüler gemeint hat, wirklich korrekt in die Robotersprache übersetzt?"
   • Die Lösung: Das System übersetzt Schritt für Schritt. Sobald der Roboter einen Fehler meldet, weiß der Dolmetscher: „Aha, hier war etwas falsch."

2. Der Wegweiser (Next Step Generator):

   • Die Aufgabe: Wenn der Beweis noch nicht fertig ist oder ein Fehler vorliegt, muss jemand sagen: „Was kommt als Nächstes?"
   • Wie es funktioniert: Der Roboter (Lean) kennt alle möglichen logischen Schritte, die zu einer korrekten Lösung führen. Der Wegweiser schaut sich den aktuellen Stand an und fragt den Roboter: „Welche 12 nächsten Schritte könnten funktionieren?" Der Roboter testet diese Schritte im Hintergrund. Wenn einer funktioniert, wird er als Vorschlag genommen.
   • Die Analogie: Stell dir vor, du bist in einem Labyrinth. Der Wegweiser schaut nicht auf die Karte, sondern probiert im Hintergrund verschiedene Gänge aus, bis er einen findet, der weiterführt, und sagt dir dann: „Versuche mal, links abzubiegen."

3. Der Erklärer (Feedback Generator):

   • Die Aufgabe: Er nimmt die Informationen vom Dolmetscher (wo war der Fehler?) und vom Wegweiser (was wäre der richtige nächste Schritt?) und formuliert eine freundliche, verständliche Antwort auf Deutsch.
   • Das Ziel: Er gibt keine komplette Lösung weg. Stattdessen sagt er: „Du hast hier einen logischen Sprung gemacht. Denk daran, dass du im ersten Schritt noch etwas beweisen musstest. Wie könnte man das formulieren?"

Der Test: PeanoBench

Um zu prüfen, ob das Team funktioniert, haben die Forscher eine spezielle Übungsstunde namens PeanoBench erstellt.
Stell dir das wie ein Arbeitsheft vor, das 371 Aufgaben enthält. Für jede Aufgabe gibt es:

• Eine Lösung, die ein Mensch in normaler Sprache geschrieben hat.
• Eine Lösung, die ein Experte in der Robotersprache geschrieben hat.

Das System hat versucht, diese Aufgaben zu lösen und Fehler zu korrigieren. Das Ergebnis war vielversprechend: LeanTutor konnte Fehler besser finden und hilfreichere Hinweise geben als ein reiner Chatbot, ohne dabei die mathematische Genauigkeit zu verlieren.

Warum ist das wichtig?

Bisher mussten sich Schüler entweder mit den Fehlern von Chatbots herumschlagen (die oft falsche Mathematik liefern) oder sich durch die komplizierte Syntax von Beweis-Software kämpfen (die frustrierend ist).

LeanTutor ist wie ein Brückenbauer. Er erlaubt dir, in deiner eigenen Sprache zu denken und zu schreiben, während im Hintergrund ein unfehlbarer Mathematiker (der Theorem Prover) sicherstellt, dass alles logisch wasserdicht ist. Er gibt dir Hinweise, damit du selbst den Weg findest, anstatt dir den Berg einfach abzutragen.

Kurz gesagt: Es ist ein Tutor, der so freundlich und verständlich ist wie ein guter Lehrer, aber so präzise und fehlerfrei wie ein Computer.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „LeanTutor: Towards a Verified AI Mathematical Proof Tutor" auf Deutsch:

1. Problemstellung

Das Papier adressiert das Dilemma beim Einsatz von KI in der mathematischen Ausbildung, insbesondere beim Erlernen von Beweisen:

• Sprachmodelle (LLMs): Modelle wie ChatGPT ermöglichen eine nahtlose Kommunikation in natürlicher Sprache, neigen jedoch zu „Halluzinationen", geben oft direkt die Lösung an (anstatt den Lernprozess zu steuern) und können logische Fehler in Argumentationen nicht zuverlässig erkennen.
• Theorembeweiser (z. B. Lean): Systeme wie Lean garantieren mathematische Korrektheit, sind aber für Studierende aufgrund ihrer komplexen Syntax und des steilen Lernkurven schwer zugänglich.
• Lücke: Es fehlt an einem System, das die Benutzerfreundlichkeit von LLMs mit der verifizierten Korrektheit von Theorembeweisern kombiniert, ohne den Studierenden die formale Syntax aufzuzwingen.

2. Methodik: Das LeanTutor-System

LeanTutor ist ein Proof-of-Concept-System, das drei Module integriert, um eine Interaktion in natürlicher Sprache (NL) zu ermöglichen, während im Hintergrund der Lean-Theorembeweiser zur Validierung genutzt wird.

A. Architektur der Module

1. Autoformalisierer & Proof-Checker:

   • Wandelt schrittweise die vom Studierenden eingegebene natürliche Sprache in Lean-Code (formale Sprache, FL) um.
   • Jeder Schritt wird sofort kompiliert.
   • Fehlererkennung: Wenn der Compiler einen Fehler meldet (z. B. unbekannte Taktik), wird der Schritt als fehlerhaft markiert und der Prozess gestoppt.
   • Kontext: Das Modell erhält als Eingabe einen Referenzbeweis (Staff Solution), ein Wörterbuch aller Theoreme/Taktiken und Few-Shot-Beispiele.

2. Next-Step Generator (NSG):

   • Wird aktiviert, wenn der Beweis unvollständig oder fehlerhaft ist.
   • Führt eine LLM-gesteuerte Tiefensuche (Depth-First Search) durch, um gültige nächste Taktiken zu finden.
   • Generiert 12 Kandidaten-Taktiken, filtert diese durch einen Compiler und einen „Fortschritts-Check" (verhindert Zyklen und die Verwendung verbotener Theoreme), bis ein vollständiger Beweis gefunden ist.

3. Natural Language Feedback Generator:

   • Generiert pädagogisches Feedback basierend auf den Ergebnissen der vorherigen Module.
   • Liefert drei Arten von Feedback (ähnlich Intelligent Tutoring Systems):
     1. Fehleridentifikation: Wo liegt der Fehler?
     2. Hinweis/Frage: Lenkt den Studierenden zum nächsten Schritt, ohne die Lösung preiszugeben.
     3. Expliziter nächster Schritt: Eine direkte Anleitung (Bottom-out Hint), falls nötig.

B. Der PeanoBench-Datensatz

Da keine geeigneten Datensätze existierten, wurde PeanoBench erstellt:

• Umfang: 371 Beweise in Peano-Arithmetik.
• Struktur: Jeder Beweis besteht aus einer handgeschriebenen natürlichen Sprache (NL) und einer äquivalenten formalen Lean-Version (FL).
• Vielfalt:
  • Staff Solutions: Referenzlösungen aus dem „Natural Numbers Game" (NNG4).
  • Korrekte Beweise: Generiert mit zwei „Personas" (formelbasiert vs. begründungsbasiert), um verschiedene Schreibstile abzubilden.
  • Fehlerhafte Beweise: Durch algorithmisches Überspringen von Schritten in korrekten Beweisen erzeugt, um typische logische Fehler (z. B. das Auslassen von Rechtfertigungen) zu simulieren.
• Besonderheit: Ein 1-zu-1-Mapping zwischen NL-Schritten und FL-Taktiken, was für das Training des Autoformalisierers entscheidend ist.

3. Wichtige Beiträge

• Hybride Architektur: Ein Framework, das LLMs für die natürliche Sprache und Theorembeweiser für die logische Validierung kombiniert, um „verifizierte" KI-Tutoren zu ermöglichen.
• Neues Evaluations-Metrik: Entwicklung einer Metrik für „faithful autoformalization" (treue Autoformalisierung). Da reine Syntax-Korrektheit nicht ausreicht, wird geprüft, ob der generierte Taktik-String oder der resultierende Beweiszustand (Proof State) semantisch äquivalent zum Ground Truth ist (unter Berücksichtigung von Variablennamen).
• Schritt-für-Schritt vs. Ganzheitlich: Untersuchung, dass eine schrittweise Autoformalisierung (Step-by-Step) bei fehlerhaften Eingaben robuster ist als die Generierung ganzer Beweise auf einmal.
• Datensatz: Bereitstellung von PeanoBench als Benchmark für NL-zu-FL-Übersetzungen im Kontext von Tutoring-Systemen.

4. Ergebnisse

Die Evaluation erfolgte an 21 fehlerhaften Beweisen aus PeanoBench unter Verwendung von gpt-4o-mini.

• Autoformalisierung:

  • Die Kombination aus Schritt-für-Schritt-Ansatz und Bereitstellung einer Staff Solution führte zu signifikanten Verbesserungen.
  • Die Genauigkeit bei korrekten Taktiken stieg von 32,9 % (Baseline) auf 56,8 % mit Staff Solution.
  • Bei fehlerhaften Beweisen konnte das System den Fehler in 30,1 % der Fälle korrekt identifizieren (im Vergleich zu 14,4 % bei der Baseline).
  • Limitierung: Das Modell ist stark auf die im Kontext bereitgestellte Staff Solution angewiesen; bei Abweichungen davon sinkt die Leistung.

• Feedback-Qualität (Menschliche Evaluation):

  • LeanTutor schnitt bei den Metriken Genauigkeit (Accuracy) und Relevanz besser ab als eine reine LLM-Baseline.
  • Die Lesbarkeit war bei beiden Modellen hoch und vergleichbar.
  • Antwort-Leckage (Answer Leakage): LeanTutor gelang es besser, die vollständige Lösung zu verschleiern, während die Baseline öfter die Lösung direkt preisgab (besonders bei „Next Step"-Feedback).
  • LLM-as-a-Judge: Ein Versuch, GPT-4 als Bewerter zu nutzen, ergab widersprüchliche Ergebnisse (Baseline wurde höher bewertet), was die Notwendigkeit menschlicher Evaluatoren unterstreicht.

5. Bedeutung und Ausblick

• Pädagogischer Wert: LeanTutor demonstriert, wie KI-gestützte Tutoren entwickelt werden können, die nicht nur Antworten liefern, sondern den Lernprozess durch verifizierte Korrektheit und gezieltes Feedback unterstützen.
• Skalierbarkeit: Das System zeigt, dass es möglich ist, formale Verifikation in natürliche Sprache zu „verstecken", was die Hürde für Studierende senkt.
• Offene Fragen:
  • Die aktuelle Architektur setzt eine 1-zu-1-Entsprechung zwischen NL und FL voraus, was bei komplexeren Beweisen schwierig sein könnte.
  • Die Abhängigkeit von einer bereits formalisierten Staff Solution ist ein Engpass.
  • Zukünftige Arbeiten zielen darauf ab, Backtracking-Mechanismen zu verbessern und das System in großen Vorlesungen (z. B. Diskrete Mathematik) einzusetzen.

Fazit: LeanTutor ist ein vielversprechender Schritt hin zu hybriden KI-Systemen, die die Stärken von LLMs (Kommunikation) und Theorembeweisern (Verlässlichkeit) vereinen, um mathematisches Denken kritisch zu fördern, ohne die Studierenden mit formaler Syntax zu überfordern.