Einführung von ProofBuddy: Verbesserung der Beweisfähigkeiten in der Bildung

Der Nachweis von Kompetenz, also die Fähigkeit, mathematische Beweise zu schreiben und zu überprüfen, ist eine wichtige Fähigkeit in der Informatik. Viele Studis finden das jedoch knifflig. Die Hauptprobleme, mit denen sie konfrontiert sind, sind die korrekte Verwendung der formalen Sprache und die Überprüfung, ob ihre Beweise vollständig und korrekt sind. Während einige vorgeschlagen haben, Beweisassistenten zu nutzen, um diese Fähigkeit zu vermitteln, ist es unklar, wie effektiv dieser Ansatz wirklich ist.

Um diese Herausforderungen anzugehen, haben wir ein Tool namens ProofBuddy eingeführt. Es ist ein webbasiertes Tool, das den Isabelle-Beweisassistenten nutzt. Dieses Tool ermöglicht Forschern, zu untersuchen, wie effektiv Beweisassistenten in der Bildung sind, indem detaillierte Daten darüber gesammelt werden, wie Studis mit ihnen arbeiten.

Wir haben eine erste Studie zu ProofBuddy an der Technischen Universität Dänemark durchgeführt. Ein typisches Bachelor-Programm in Informatik beinhaltet Programmierung, technische Fähigkeiten über Computer, theoretisches Wissen und Mathe. Letztere zwei bereiten oft Schwierigkeiten für die Studis. Die Kurse konzentrieren sich auf Formale Sprachen, Logik und Beweise. Da die Studis in mehreren Kursen Beweise schreiben und verifizieren müssen, brauchen sie Beweiscompetenz, die vier spezifische Fähigkeiten umfasst:

1. Fachliche Kompetenz: Das ist Wissen über den Kontext des Beweises, der erstellt werden muss.
2. Darstellungskompetenz: Dabei geht's darum, einen Beweis in formaler Sprache zu schreiben.
3. Kommunikationskompetenz: Das bezieht sich auf das Diskutieren und Erklären des Beweisprozesses und der Lösungen.
4. Methodische Kompetenz: Das fasst die Methoden in Beweisen zusammen, wie deren Struktur und logische Schlussfolgerungsketten.

Obwohl diese Fähigkeiten in Einführungskursen gelehrt werden, ist Beweiskompetenz selten ein klares Ziel in den Lehrplänen. Daher arbeiten die Studis oft die Beweise durch, die von den Dozenten präsentiert werden, und versuchen, sie zu replizieren. Leider haben viele damit Probleme.

In einer Studie haben Forscher Hausaufgaben und Prüfungen aus einem Einführungskurs analysiert. Sie fanden heraus, dass die Studis die meisten Fehler bei Übungen machten, die Beweise beinhalteten, egal wie gut ihre Gesamtnoten waren. Die Probleme stammen hauptsächlich von der Verwendung formaler Sprache und der Beurteilung, ob ein Beweis korrekt ist. Das führt zu einer hohen Durchfallquote in Einführungskursen zu Beweisen.

Beweisassistenten wurden als Möglichkeit vorgeschlagen, die Beweiskompetenz zu verbessern. Ein Beweisassistent kombiniert Merkmale einer funktionalen Programmiersprache mit Werkzeugen zum Denken über Programme. Dieses Setup ermöglicht es den Nutzern, Beweise formeller zu schreiben und sofortiges Feedback zur Korrektheit vom Beweisprüfer zu erhalten.

Befürworter der Verwendung von Beweisassistenten in der Bildung heben viele Vorteile hervor. Leider mangelt es diesen Behauptungen oft an starker Evidenz. Kritiker sind auch besorgt, dass die mit Beweisassistenten erworbenen Fähigkeiten möglicherweise nicht gut auf traditionelle Papierbeweise übertragbar sind. Sie befürchten, dass diese Werkzeuge „brute-force proving“ begünstigen, wo die Studis einfach weitermachen, bis sie Erfolg haben, anstatt zu verstehen, warum ein Beweis funktioniert. Ausserdem könnte die Einführung eines Beweisassistenten wertvolle Unterrichtszeit in Anspruch nehmen.

Um diese Behauptungen zu untersuchen, haben wir ProofBuddy entwickelt, das eine verbesserte Version des Isabelle-Beweisassistenten ist. Das Ziel von ProofBuddy ist es, detaillierte Daten über die Interaktionen der Studis mit dem Beweisassistenten zu sammeln und Forschern zu helfen, verschiedene Lehrmethoden zu untersuchen.

In unserer ersten Evaluation haben wir die Benutzerfreundlichkeit von ProofBuddy und die Arten von Daten, die es sammelt, untersucht. Wir glauben, dass die Daten ausreichen, um viele Fragen zu beantworten, die zukünftige Forschung aufwerfen könnte.

Insgesamt bieten wir mehrere Beiträge:

1. Ein Überblick über die aktuellen Herausforderungen bei der Bewertung der Effektivität von Beweisassistenten in der Bildung.
2. Die Einführung von ProofBuddy, einer Version des Isabelle-Beweisassistenten, die Interaktionsdaten sammelt.
3. Eine erste Bewertung der Benutzerfreundlichkeit von ProofBuddy aus der Sicht der Studis.
4. Eine Einschätzung, wie gut die gesammelten Interaktionsdaten von ProofBuddy Forschungsfragen beantworten können.

Als Nächstes diskutieren wir die bestehenden Anwendungen von Beweisassistenten in der Bildung, einschliesslich ihrer behaupteten Vorteile und Nachteile, sowie Werkzeuge aus der funktionalen Programmierung, die das Design von ProofBuddy inspiriert haben. Wir skizzieren auch potenzielle Methoden, um einige der beobachteten Nachteile anzugehen und die Vorteile der Verwendung von Beweisassistenten im Bildungsbereich weiter zu untersuchen.

#Verwandte Arbeiten

Die Verwendung von Beweisassistenten in der Bildung ist keine neue Idee, aber die meisten Ergebnisse aus diesen Bemühungen bestehen aus Erfahrungsberichten und nicht aus gründlichen Bewertungen ihrer Wirksamkeit. Wir geben einen kurzen Überblick über verschiedene Ansätze.

Einige Kurse richten sich an Studis, die schon weiter in ihrem Studium sind und davon ausgehen, dass sie bereits Beweiskompetenz und Fähigkeiten in funktionaler Programmierung haben. Zum Beispiel berichteten Forscher, dass sie den Coq-Beweisassistenten verwendet haben, um die Beweiskompetenz zu steigern. Obwohl die Studis nach dem Kurs Theoreme mit Coq beweisen konnten, verbesserte sich ihre Fähigkeit, Papierbeweise zu schreiben, nur geringfügig.

Andere Studien haben versucht, Beweisassistenten in Erstsemesterkurse zu integrieren. Ein solches Vorhaben nutzte Lean, einen Beweisassistenten, in einem Logikkurs, um mathematische und natürliche Sprachbeweise zu kombinieren. Obwohl Lean während freiwilliger Workshops beliebt war, war es nicht verpflichtend, was bedeutete, dass nur Studis, die bereits gut im Kurs waren, sich entschieden, es zu nutzen.

Einige Kurse an der Technischen Universität Berlin integriert Isabelle in Übungen, bei denen die Studis an Logik arbeiten konnten, aber diese Nutzung war optional. Viele fanden es zwar unterhaltsam, aber zeitaufwendig.

Es wurden auch andere Werkzeuge entwickelt, um Beweise und Logik zu lehren, wie Waterproof, das es Nutzern ermöglicht, Coq-Beweise neben natürlicher Sprache zu schreiben. Es gibt auch das AProS-Projekt, das darauf abzielt, Kurse und Werkzeuge zu entwickeln, die sich auf das Lehren von Logik und Beweisen in interaktiven Umgebungen konzentrieren.

Während viele Beweisassistenten existieren und einige vielversprechende Ergebnisse gezeigt haben, wurden nur wenige gründlich durch strukturierte Studien validiert.

#Vorteile und Nachteile der Verwendung von Beweisassistenten

Die Vorteile von Beweisassistenten in der Bildung sind gut dokumentiert, darunter:

• Sie helfen beim Mathematiklernen.
• Sie sind nützlich für das Lernen funktionaler Programmierung.
• Sie verdeutlichen die Regeln des formalen Denkens.
• Sie lehren den Studis, wie man Beweise strukturiert.
• Sie bieten sofortiges Feedback zum Fortschritt des Beweises.
• Sie ermutigen die Studis, formale Definitionen zu konsultieren und sich damit auseinanderzusetzen.
• Sie helfen den Studis, mit Beweiskonzepten zu experimentieren.
• Sie erleichtern die Korrektur von Aufgaben, die von Beweisassistenten überprüft werden.

Es gibt jedoch auch bemerkenswerte Herausforderungen, mit denen die Studis bei der Verwendung von Beweisassistenten konfrontiert sind. Einige davon sind:

• Das Lernen der Syntax kann schwierig sein.
• Fehlermeldungen können verwirrend sein.
• Fähigkeiten, die mit Beweisassistenten erworben werden, übertragen sich möglicherweise nicht gut auf Papierbeweise.
• Technische Schwierigkeiten können bei der Installation und Nutzung auftreten.
• Einige Studis haben Schwierigkeiten, sich an formale Beweisregeln zu erinnern.

Auch Lehrer können auf Herausforderungen stossen, wie die benötigte Zeit, um Beweisassistenten einzuführen und Übungen zu entwerfen. Es gibt auch Bedenken hinsichtlich Betrugs, da elektronische Werkzeuge es den Studis erleichtern können, Wege zu finden, um Aufgaben zu umgehen.

Mehrere Autoren weisen auf Probleme hin, die mit der Bereitstellung solider Belege für die Ansprüche bezüglich Beweisassistenten verbunden sind. Es gibt keine geeigneten Methoden, um die Beweiskompetenz quantitativ zu messen, was es schwierig macht, Belege darüber zu sammeln, wie die Studis mit diesen Werkzeugen interagieren.

#Es einfacher machen, Beweisassistenten zu lernen

Beweisassistenten sind im Allgemeinen für Expertenbenutzer gemacht, was eine steile Lernkurve für Anfänger schafft. Formale Sprachen können für neue Studis knifflig sein. Lehrkräfte könnten diese Herausforderung verringern, indem sie die Sprache Schritt für Schritt einführen und Werkzeuge nutzen, die die Studis im Lernprozess unterstützen.

Studis finden oft, dass die Fehlermeldungen vage und verwirrend sind. Eine Vereinfachung der Sprache des Beweisassistenten für Bildungszwecke könnte helfen, Missverständnisse zu reduzieren.

Technische Probleme können ebenfalls auftreten. Webbasierte Plattformen können es erleichtern, auf Werkzeuge zuzugreifen und sie zu aktualisieren.

#Beweise sammeln

Eine der Hauptschwierigkeiten mit Beweisassistenten in der Bildung ist das Fehlen von Beweisen dafür, wie sie die Beweiskompetenz verbessern. Zu verstehen, ob die Ressourcen, die in die Erstellung von Kursen mit Beweisassistenten investiert werden, bessere Ergebnisse bringen, ist weiterhin eine Frage. Es ist entscheidend, die Lernziele genau zu definieren, zum Beispiel, ob das Ziel darin besteht, allgemeine Beweiskompetenz oder speziell Fähigkeiten für Papierbeweise zu entwickeln.

Es ist wichtig, objektive, quantitative Daten über die Interaktionen der Studis mit Beweisassistenten zu sammeln, um effektive Forschung zu betreiben. Die meisten Berichte basieren auf Umfragen, die die Studis nach ihren Erfahrungen oder vagen Messungen basierend auf den durchschnittlichen Kursnoten fragen.

#Evaluation von ProofBuddy

Wir wollen ProofBuddy aus zwei Perspektiven bewerten: Wie gut es den Forschern ermöglicht, didaktische Studien durchzuführen, und seine Benutzerfreundlichkeit aus der Sicht der Studis.

Durchgeführt im Frühjahr 2023, fand unsere Evaluation in einem fortgeschrittenen Kurs über automatisches Schliessen an der Technischen Universität Dänemark statt. Der Kurs konzentrierte sich darauf, Isabelle zu nutzen. Wir erwarteten, dass die Studis in diesem Kurs bereits Papierbeweise verstanden.

Die Teilnehmer arbeiteten an Übungen mit ProofBuddy und füllten dann einen kurzen Fragebogen aus. Während der Evaluation beobachteten wir, wie die Studis mit dem Tool interagierten und notierten ihre Fragen an die Dozenten.

Alle Studis begannen die Übungssitzung mit ProofBuddy. Zunächst stellten sie viele Fragen zur Benutzeroberfläche. Die meisten konzentrierten sich auf logische Übungen, obwohl einige mit Programmieraufgaben begannen.

Während der Sitzung sammelten wir Fragen, die in verschiedene Kategorien eingeteilt wurden, darunter Schwierigkeiten beim Erstellen von Beweisen und Probleme beim Verständnis der Isabelle-Syntax und der Logik. Die Studis blieben engagiert mit ProofBuddy, obwohl einige fanden, dass die Rückmeldungen zu langsam waren.

Trotz der Benutzerfreundlichkeitsprobleme funktionierten die Datensammelfunktionen wie vorgesehen. Wir erfassten alle notwendigen Daten, um das Verhalten der Studis bei der Arbeit mit ProofBuddy zu analysieren.

#Zukünftige Arbeiten

Wir haben Pläne zur Verbesserung von ProofBuddy. Zuerst möchten wir die Reaktionszeit optimieren, indem wir Isabelle-Theorien im Frontend bewerten, was helfen könnte, Syntaxfehler zu erkennen, bevor sie zur Überprüfung gesendet werden.

Wir planen auch, die Kursverwaltungsfunktionen zu erweitern, indem wir den Linter, Dropdown-Menüs und die Symboltastatur mit zusätzlichen Übungen in Einklang bringen, um die Lernziele zu unterstützen.

Zusätzlich möchten wir die gesammelten Daten automatisch analysieren. So können wir besser verstehen, welches Feedback die Studis benötigen und in welchen Beweisbereichen sie Schwierigkeiten haben.

Ausserdem entwickeln wir neue Kurse, die sich auf das Lehren von Beweisen an der Technischen Universität Berlin konzentrieren. Dieser Kurs wird darauf abzielen, den Studis in Echtzeit mehr Feedback zu geben, um ihr Engagement mit dem Material zu verstärken und ihr Verständnis zu fördern.

Zusammenfassend haben wir ProofBuddy vorgestellt, ein webbasiertes Tool zur Anleitung und Überwachung der Nutzung von Isabelle in der Ausbildung der Studis. Beweisassistenten wie Isabelle erleichtern das Schreiben von Beweisen über funktionale Programme. Allerdings sind rigorose Studien nötig, um ihren Bildungsbeitrag effektiv zu bewerten. ProofBuddy dient als Plattform zur Datensammlung über die Interaktionen der Studis und bietet wertvolle Einblicke in ihre Lernprozesse, während es den Lehrenden hilft zu verstehen, wie sie den Unterricht verbessern können.