Generative KI für den universitären Unterricht von Logik und formalen Methoden: Geht das?

In Lehrveranstaltungen wie “Logik” oder “Formale Methoden der Informatik”, welche die Werkzeuge von symbolischer künstlicher Intelligenz (KI) einführen, geht es um exakte Techniken und Modellierungswerkzeuge. Diese werden zum Beispiel benötigt, um die Korrektheit, Zuverlässigkeit und Sicherheit von Computer-Systemen zu gewährleisten. Symbolische KI steht im Kontrast zu generativer KI, die auf inexakten statistischen Methoden basiert. Trotz der unterschiedlichen Ansätze nutzen Studierende Tools wie ChatGPT, um Logik-Aufgaben zu lösen. In diesem Vortrag betrachten wir, was funktioniert und was nicht, wenn generative KI für die Lösung von Logik-Aufgaben eingesetzt wird und wie Sprachmodelle die Lehre in Fächern wie Logik und Formale Methoden dennoch unterstützen können.