Verifikation kann Lernen bremsen: Asymmetrische Effekte im Logik-Tutor

Große Sprachmodelle (LLMs) werden zunehmend als automatisierte Tutoren eingesetzt, doch ihre Zuverlässigkeit in streng symbolischen Bereichen bleibt unklar. In einer neuen Studie wird die Schritt-für-Schritt‑Feedback‑Qualität für Beweise in der Aussagenlogik untersucht, die präzise symbolische Argumentation erfordert.

Zur Analyse wurde ein neues Benchmark‑Set mit 516 einzigartigen Beweis­zuständen entwickelt. Jeder Zustand ist mit detaillierten Schritt‑Annotations­daten sowie Schwierigkeits­metriken versehen, sodass die Qualität des Feedbacks exakt gegen verifizierte Lösungswege abgewogen werden kann.

Die Autoren testeten drei spezialisierte Pipelines: den „Tutor“, der nur einen Teil der Lösung kennt; den „Teacher“, der die komplette Ableitung einsehen kann; und den „Judge“, der das Feedback des Tutors verifiziert. Die Ergebnisse zeigen eine auffällige Asymmetrie: Verifikation verbessert die Lernleistung, wenn das ursprüngliche Feedback fehlerhaft ist (<70 % Genauigkeit), verschlechtert sie jedoch um 4–6 Prozentpunkte, wenn das Feedback bereits hochpräzise ist (>85 % Genauigkeit). Gleichzeitig gibt es eine gemeinsame Komplexitäts­grenze – keine Pipeline gelingt es zuverlässig, Beweis­zustände mit einer Komplexität von mehr als 4–5 zu lösen.

Diese Erkenntnisse stellen die Annahme in Frage, dass zusätzliche Verifikatoren oder reichhaltigere Kontextinformationen immer zu besseren Tutoren führen. Stattdessen wird ein adaptiver, Schwierigkeits‑bewusster Ansatz gefordert, der Aufgaben je nach geschätzter Komplexität und Zuverlässigkeit des vorangegangenen Feedbacks zuweist.