A method for the automated generation of proof exercises with comparable levels of proving complexity

Diese Arbeit stellt eine Methode zur automatisierten Generierung von Beweisübungen mit vergleichbarem Schwierigkeitsgrad vor, die auf der Analyse von Tableau-Beweisen in der ersten Stufe basiert, um den manuellen Aufwand für die Erstellung von Übungsaufgaben im Bereich der diskreten Mathematik zu reduzieren.

Das Wesentliche

Stellen Sie sich vor, Sie sind ein Lehrer für Mathematik oder Logik. Ihre größte Herausforderung ist nicht das Unterrichten selbst, sondern die Erstellung von Hausaufgaben. Jede Woche müssen Sie neue Beweisaufgaben erfinden, die genau das richtige Schwierigkeitsniveau haben: nicht zu leicht, damit die Schüler nicht gelangweilt werden, und nicht zu schwer, damit sie nicht frustriert aufgeben.

Dieses Papier beschreibt eine Art „automatischen Aufgaben-Generator", der genau das tut. Aber er macht es nicht einfach durch Zufall, sondern mit einem sehr cleveren Trick, um sicherzustellen, dass alle neuen Aufgaben genau so schwer sind wie die Originalaufgabe, die der Lehrer als Vorlage eingibt.

Hier ist die Erklärung des Konzepts, vereinfacht und mit Analogien:

1. Das Problem: Der „Schwierigkeits-Detektor"

Bisher konnten Computer zwar Fragen generieren, aber sie wussten oft nicht, wie schwer diese Fragen für einen Menschen sind.

• Der alte Weg: Ein Computer schaut auf die Länge der Aufgabe oder wie viele Symbole sie enthält. Das ist wie wenn man die Schwierigkeit eines Puzzles nur an der Anzahl der Teile misst. Ein Puzzle mit 1000 Teilen kann leicht sein, wenn alle Teile blau sind, und ein Puzzle mit 500 Teilen kann unmöglich sein, wenn die Teile alle gleich aussehen.
• Das neue Ziel: Der Computer muss verstehen, wie viel Gehirnarbeit nötig ist, um die Lösung zu finden.

2. Die Lösung: Die „Baukasten-Methode" (Theorie-spezifische Beweise)

Die Autoren entwickeln eine Methode, die Beweise nicht als lange, verworrene Texte betrachtet, sondern als klare Baumstrukturen.

Stellen Sie sich einen mathematischen Beweis wie einen Rezept für einen Kuchen vor:

• Die Zutaten: Das sind die gegebenen Informationen (z. B. „Setze A in B ein").
• Die Schritte: Das sind die Regeln, wie man von einer Zutat zur nächsten kommt.
• Das Ziel: Der fertige Kuchen (der Beweis).

Das Besondere an dieser Methode ist, dass sie die „Zutaten" (die logischen Symbole) entfernt und nur die Struktur der Schritte betrachtet. Sie nennen dies „theorie-spezifische Beweise".

• Die Analogie: Stellen Sie sich vor, Sie wollen zwei verschiedene Kuchen vergleichen: einen Schokoladenkuchen und einen Vanillekuchen. Normalerweise schmecken sie anders. Aber dieser Generator ignoriert den Geschmack (die spezifischen Symbole) und schaut nur auf die Anzahl der Rührschritte, die Backzeit und die Anzahl der Etagen. Wenn beide Kuchen die gleiche „Struktur" haben, sind sie für den Bäcker (den Schüler) gleich schwer zu backen, egal ob es Schokolade oder Vanille ist.

3. Wie funktioniert der Generator? (Der dreistufige Prozess)

Der Generator arbeitet in drei Schritten, die wie ein cleverer Detektiv vorgehen:

Schritt A: Den „perfekten Beweis" finden (Minimaler Aufwand)

Der Computer nimmt eine Beispiel-Aufgabe und baut den kürzesten und effizientesten Weg zur Lösung.

• Analogie: Ein Wanderer sucht den kürzesten Weg von Punkt A nach Punkt B durch einen Wald. Er zählt genau, wie viele Bäume er umgehen muss und wie viele Hügel er übersteigen muss. Das ist der „Maßstab" für die Schwierigkeit.

Schritt B: Die „Bauanleitung" analysieren

Der Computer schaut sich genau an, welche Regeln er benutzt hat, um diesen Weg zu finden.

• Analogie: Er erstellt eine Liste: „Ich musste 3-mal links abbiegen, 2-mal über einen Zaun springen und 1-mal einen Fluss durchwaten." Diese Liste ist das Muster der Schwierigkeit.

Schritt C: Neue Aufgaben mit demselben Muster bauen

Jetzt kommt der Zaubertrick. Der Computer nimmt dieses Muster und baut damit völlig neue Aufgaben, indem er die Symbole austauscht, aber die Struktur beibehält.

• Analogie: Er nimmt das Rezept für den Schokoladenkuchen (das Muster) und tauscht einfach die Zutaten aus: Statt Schokolade nimmt er Erdbeeren, statt Mehl nimmt er Haferflocken.
• Das Ergebnis: Der neue „Erdbeerkuchen" sieht anders aus und schmeckt anders, aber er hat genau die gleiche Anzahl von Rührschritten und Backzeiten. Für den Schüler ist es also genauso schwer (oder leicht) zu lösen wie das Original.

4. Warum ist das „Cut-based Tableau" wichtig?

Der Text erwähnt oft „Cut-based Tableaux". Das klingt kompliziert, ist aber im Grunde ein Strengen-System.
Stellen Sie sich vor, Sie versuchen, einen Weg durch ein Labyrinth zu finden.

• Normale Methoden: Man läuft blind umher und versucht alles. Das dauert ewig.
• Die Methode dieses Papiers: Man darf nur bestimmte, erlaubte Schritte machen (wie „nur geradeaus" oder „nur links abbiegen, wenn eine rote Wand da ist"). Diese Regeln sorgen dafür, dass der Computer nicht in endlosen Schleifen läuft, sondern immer den direktesten Weg findet. Das macht es möglich, die Schwierigkeit exakt zu berechnen.

5. Das große Ziel: Faire und personalisierte Bildung

Warum machen die Autoren das alles?

• Zeitersparnis: Lehrer müssen keine Stunden mehr damit verbringen, Aufgaben zu erfinden. Der Computer macht das in Sekunden.
• Faire Bewertung: Wenn ein Lehrer 50 Aufgaben für eine Klasse braucht, kann der Generator 50 Aufgaben erstellen, die alle exakt gleich schwer sind. Niemand hat Glück, weil er eine „einfache" Aufgabe gezogen hat, und niemand hat Pech, weil er eine „unmögliche" Aufgabe bekam.
• Individuelles Lernen: Ein Schüler, der schnell ist, bekommt automatisch Aufgaben mit einem komplexeren „Baum-Struktur"-Muster, während ein Schüler, der Hilfe braucht, Aufgaben mit einer einfacheren Struktur bekommt.

Zusammenfassung in einem Satz

Dieses Papier beschreibt einen intelligenten Roboter-Lehrer-Assistenten, der neue Mathematikaufgaben erfindet, indem er die Struktur der Lösung eines Originals kopiert und die Inhalte austauscht, sodass jede neue Aufgabe garantiert das gleiche Schwierigkeitsniveau hat wie das Original – ganz ohne menschliches Raten.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des vorliegenden Papers auf Deutsch:

Technische Zusammenfassung: Automatisierte Generierung von Beweisübungen mit vergleichbarem Komplexitätsniveau

1. Problemstellung
Die manuelle Erstellung von Übungsaufgaben für den Unterricht ist für Lehrende eine zeitintensivste und belastende Aufgabe. Zwar existieren Systeme zur automatisierten Generierung von Fragen (Automatic Question Generation, AQG), doch fehlt es diesen häufig an einer präzisen Steuerung der Schwierigkeitsgrade. Bestehende Ansätze zur Schwierigkeitsschätzung basieren oft auf syntaktischen Merkmalen (z. B. Anzahl der Operatoren) oder maschinellen Lernmodellen, die auf menschlichen Bewertungen trainiert sind. Diese Methoden haben zwei wesentliche Mängel:

• Sie erfassen nicht den tatsächlichen kognitiven Aufwand, der für die Lösung einer Aufgabe notwendig ist (z. B. können zwei Formeln mit gleicher Syntaxstruktur völlig unterschiedliche Beweisstrukturen erfordern).
• Maschinelle Lernansätze liefern oft keine nachvollziehbaren Erklärungen für die eingestufte Schwierigkeit und sind anfällig für Inkonsistenzen menschlicher Bewertungen.

Das Ziel dieses Papers ist es, eine Methode zur automatisierten Generierung von Beweisübungen (insbesondere im Bereich der diskreten Mathematik und der Prädikatenlogik erster Stufe) zu entwickeln, bei der die generierten Übungen ein vergleichbares Maß an Beweiskomplexität aufweisen wie eine vorgegebene Eingabeübung.

2. Methodik
Der vorgeschlagene Ansatz basiert auf einer formalen Definition von Beweiskomplexität, die durch theoriespezifische Tableau-Beweise (Theory-Specific Proofs) operationalisiert wird.

• Theoriespezifische Tableaus: Anstelle von klassischen analytischen Tableaus, die logische Symbole ($\neg, \land, \to$ etc.) explizit verarbeiten, werden Tableaus verwendet, deren Knoten nur durch "theoriespezifische Formeln" (atomare Formeln ohne logische Symbole) gekennzeichnet sind. Dies bildet eine Formalisierung informeller mathematischer Beweise ab, wie sie im Unterricht üblich sind.
• Extraktion von Regeln: Aus definitorischen Axiomen einer Theorie (z. B. Mengenlehre) werden durch eine mechanisierbare Prozedur (Konvertierung in Prenex-Normalform, Skolemisierung, CNF, dann Rule Implicational Normal Form - RINF) deduktive Regeln extrahiert. Diese Regeln enthalten keine logischen Symbole in Prämissen oder Konklusionen und erfüllen analytische Einschränkungen (Variablen müssen vorhanden sein, Prädikate müssen in einer wohlgeordneten Relation "kleiner" sein, oder die Tiefe der Formel muss sinken).
• Cut-basierte Erweiterung: Um die Vollständigkeit zu gewährleisten, wird eine Schnittregel (Cut) eingeführt, die auf "minor co-premises" (Nebenprämissen) innerhalb der extrahierten Regelmenge basiert. Dies ermöglicht die Konstruktion von Beweisen, die der menschlichen Beweisführung näher kommen als reine Subformel-Analysen.
• Definition der Komplexität: Die Beweiskomplexität wird nicht durch die Länge des Textes, sondern durch die deduktive Größe (Anzahl der Knoten im "Rechtfertigungsbaum" oder justification tree) des minimalen Tableaus definiert. Zwei Beweisübungen gelten als gleich komplex, wenn ihre minimalen Beweise deduktiv isomorph sind. Das bedeutet, ihre Beweisbäume haben die gleiche Struktur, und die darin verwendeten Formeln sind syntaktisch isomorph (gleiche Variablenmengen und abstrakte Struktur).

3. Der Generierungsprozess
Das Verfahren zur Generierung neuer Übungen erfolgt in zwei Hauptschritten:

1. Suche nach minimalen Beweisen: Für eine gegebene Eingabeübung (formalisiert als Menge signierter Formeln) wird ein minimaler Tableau-Beweis unter Verwendung der extrahierten theoriespezifischen Regeln konstruiert. Dies geschieht durch eine schrittweise Erweiterung der Tableau-Bäume, bis ein geschlossener Beweis gefunden wird.
2. Suche nach beweis-isomorphen Mengen: Basierend auf der Struktur des minimalen Beweises wird der Suchraum für neue Formelmengen eingeschränkt. Das System identifiziert "deduktiv passende Symbole" (deductive matching symbols). Ein Symbol in einer Formel darf nur durch ein anderes Symbol ersetzt werden, wenn dieses in den extrahierten Regeln an einer äquivalenten Position (bezüglich der Beweisstruktur) vorkommt.
   • Beispiel: Wenn in einem Beweis das Mengensymbol $\cap$ verwendet wird, kann es durch $\cup$ oder $\setminus$ ersetzt werden, wenn die Regelstruktur dies zulässt. Funktionssymbole werden entsprechend ihrer Position im Beweisbaum analysiert.
   • Durch diese Einschränkung wird der Suchraum drastisch reduziert, und es werden nur solche neuen Übungen generiert, deren minimaler Beweis deduktiv isomorph zum Eingabebeweis ist.

4. Wichtige Beiträge

• Formalisierung der Beweiskomplexität: Einführung eines metrischen Ansatzes zur Schwierigkeitsbestimmung, der auf der Isomorphie von Beweisstrukturen (Tableaus) und nicht auf syntaktischen Oberflächeneigenschaften basiert.
• Theoriespezifische Regeln ohne logische Symbole: Entwicklung einer Methode, um aus definitorischen Axiomen Regeln zu extrahieren, die logische Operatoren eliminieren und somit informelle Beweisstrategien (wie den "Element-Argument"-Ansatz in der Mengenlehre) direkt abbilden.
• Analytische Cut-Regeln: Eine Erweiterung der Tableau-Methodik, die analytische Schnitte erlaubt, um die Vollständigkeit zu sichern, ohne die Kontrolle über die Beweisexpansion zu verlieren.
• Implementierbarer Algorithmus: Vorstellung eines vollständigen Algorithmus zur Generierung von Übungssätzen mit garantierter Komplexitätsäquivalenz, implementiert in einem Prototyp (verfügbar auf GitHub).

5. Ergebnisse und Validierung

• Der Ansatz wurde am Beispiel der Mengenlehre (mit Axiomen für $\emptyset, \cup, \cap, \setminus, \times, \triangle, \subseteq, \perp$) demonstriert.
• Das System konnte erfolgreich neue Beweisübungen generieren, die strukturell identisch zu einem Eingabebeispiel waren, aber unterschiedliche Operatoren verwendeten (z. B. Austausch von $\cap$ gegen $\setminus$ oder $\triangle$).
• Die Studie zeigt, dass Übungen, die deduktiv isomorphe minimale Beweise haben, als gleich schwierig eingestuft werden können, unabhängig von der spezifischen Wahl der mathematischen Operatoren.
• Ein Prototyp wurde entwickelt und getestet, der die Machbarkeit der Methode unterstreicht.

6. Signifikanz und Ausblick

• Pädagogischer Nutzen: Die Methode ermöglicht Lehrkräften, personalisierte und adaptive Tests zu erstellen, bei denen die Schwierigkeit präzise gesteuert werden kann, ohne dass die didaktische Qualität leidet. Sie vermeidet die Ungerechtigkeit, bei der einige Schüler einfachere Aufgaben erhalten als andere, nur weil die Aufgaben zufällig anders formuliert waren.
• Erklärbarkeit: Im Gegensatz zu Black-Box-ML-Modellen liefert dieser Ansatz eine explizite Begründung für die Schwierigkeitsstufe: Die Struktur des minimalen Beweises.
• Zukünftige Arbeiten: Die Autoren planen, die Einschränkungen bei der Extraktion von Regeln zu lockern, um mehr Axiome abzudecken. Zudem soll die Methode um Invarianzen (z. B. Vertauschung von Argumenten) erweitert werden und in realen pädagogischen Umgebungen validiert werden, um zu prüfen, ob strukturelle Merkmale (z. B. Anzahl der Prämissen in Regeln) tatsächlich von Studierenden als schwieriger empfunden werden.

Zusammenfassend stellt das Paper einen signifikanten Schritt in Richtung einer theoriebasierten, erklärbaren und präzisen Steuerung der Übungsschwierigkeit in der formalen Logik und Mathematik dar.