Teaching Support Systems for Formal Foundations of Computer Science

I presented a brief introduction to Intelligent Tutoring Systems. In this abstract I will review the themes I discussed, and include pointers for further reading.

A good introduction to Tutoring Systems is VanLehn’s the behavior of tutoring systems [17]. He distinguishes two components:

• $\mathrm{■}$

  the inner loop, in which a student works on a task, takes steps towards solving the task, and a tutoring system provides support in the form of feedback and hints;

• $\mathrm{■}$

  the outer loop, which helps a student with finding a path in the learning material, for example by suggesting next tasks to work on.

Through the years, many approaches to supporting a student when solving an exercise (the inner loop) have been developed:

• $\mathrm{■}$

  cognitive tutors, built upon theories such as ACT-R [7];

• $\mathrm{■}$

  constraint-based tutors [6];

• $\mathrm{■}$

  domain reasoners [5, 4, 3];

• $\mathrm{■}$

  data-driven tutors [2];

• $\mathrm{■}$

  LLM-based tutors [15];

• $\mathrm{■}$

  and more.

Some approaches use a student model to keep track of the learning progress of a student, and to adapt the kind of feedback given to a student. There exist many approaches to student modelling [1]; some well known examples are:

• $\mathrm{■}$

  ELO ratings

• $\mathrm{■}$

  Overlay models

• $\mathrm{■}$

  Knowledge space theory

• $\mathrm{■}$

  Constraint-based modelling

• $\mathrm{■}$

  Bayesian modelling

• $\mathrm{■}$

  Model tracing

Student models are also used to support the outer loop. The outer loop typically presents tasks to a student. The sequence in which tasks are offered is often fixed, sometimes determined by the student, and sometimes supported by a giving suggestions for a next task to work on. Recommendations can be based on a learner model and task attributes, on behavior from other students, on ratings on earlier items, and sometimes other components [8].

Many experiments have been performed to study the effectiveness of Tutoring Systems. VanLehn has shown that if you compare the effects of a tutor that supports stepwise exercises with the help of teaching assistants, there is little difference [16]. Quite a few other meta-reviews on the effectiveness of tutoring systems have been performed, but it is hard to use these reviews to make general statements: they regularly compare apples and pears [9, 10].

There is quite a lot of recent work on teaching-support systems for formal foundations of computer science [11, 12, 13, 14]. A complete overview would require a more systematic approach.

In this demo, we present pseuCo Book, a truly interactive textbook experience designed to help teachers and students alike. In pseuCo Book, interactive demonstrations and exercises are interwoven with traditional textual elements. Its technical foundation, the Hybrid Document Framework, is a toolset that makes authoring interactive textbooks as easy as possible. PseuCo Book contains three chapters: The first one, covering Milner’s Calculus of Communicating systems, is built around an interactive editor for CCS semantics derivations. The second chapter, teaching notions of equality for concurrent processes, features custom-built exercises covering proofs and algorithms around trace equality, bisimilarity, and observation congruence. The third chapter, which covers practical concurrent programming in a minimal, academic programming language called pseuCo, is built around a set of verification technologies that allow deep inspection of the concurrency-related features of pseuCo programs, enabling fast autograding of user-submitted solutions to programming tasks. PseuCo Book has been used extensively as part of the Concurrent Programming lecture at Saarland University. A comprehensive user study, run as part of the course, demonstrates that pseuCo Book is both well-received by students and has a measurable, positive impact on student performance.

I gave a brief demo session on FLACI, a web-based system designed for working with formal languages, context-free grammars, and automata. FLACI simplifies the application of these theories to compiler construction, making it accessible even at the high school level. The system allows users to visually construct and simulate automata, derivations, and compiler processes. The goal is to help students learn formal foundations while they work towards translating their own simple language into visual or acoustic output using a compiler they generate from a formal definition.

The TeachingBook (TB) is a prototype of a web-based platform to create interactive learning materials in a cell-based Jupyter-Notebook-like environment. Its main feature is the flexibility in creating content for lectures such as interactive scripts or exercise sheets by simply arranging cells of different types (see attached screenshot). Currently, several cell-types are supported. Besides markdown cells to provide LateX content and quizzes, also cells are available to foster the learning of topics in the realm of formal foundations in computer science (regular languages, reductions, …). Furthermore, TB is designed to ease the integration of existing tools either as iFrames or natively as front-end components. Several extensions of the TeachingBook are currently under development in student projects and a preliminary usability study has been conducted in a lecture on computability theory. It is planned that a publication will be ready for next year.

DiMo, short for Discrete Modelling, is a tool that supports learning of skills to use propositional logic as a backbone for general problem solving. Typical exercises in this area ask for the construction of propositional formulas depending on problem instance, A good example is: write a propositional formula ${\mathrm{\Phi }}_n$ for $n\ge 1$ that is satisfiable iff the $n$-queens problem has a solution, i.e. it is possible to place $n$ queens on a chessboard with no two of them sharing a row, a column or a diagonal line. Another example is: write a formula ${\mathrm{\Phi }}_G$ for any undirected graph $G$ that is satisfiable iff $G$ is 3-colourable.

DiMo provides a language that is reminiscent of simple imperative programming languages in order to specify formulas. For example, ${\bigvee }_{i=0}^{n-1}D(i,0)\wedge {\bigwedge }_{\genfrac{}{}{0.0pt}{}{j=0}{j\ne i}}^{n-1}\neg D(j,0)$ would be written as

FORSOME i: {0,..,n-1}. D(i,0) & FORALL j: {0,..,n-1} \ {i}. -D(j,0)

DiMo translates formulas in this formal language automatically into the mathematical form above so that students see the connection to the way formulas are presented in lectures etc.

DiMo’s crown feature is a programming language with for-loops and propositions as data types. It is supposed to be used by teachers in order to write programs that turn propositional evaluations into any graphical form, for instance in HTML. DiMO then executes these programs after satisfiability checks on the students’ formulas. This way, it is possible to check correctness of the formulas graphically, for instance by depicting the placement of queens on a chessboard.

DiMo is publically available to try out via a webinterface, located at https://dumbarton.tifm.cs.uni-kassel.de/. Further and more detailed information can be found in two papers on the technical aspects of DiMo [2] and on the graphical feedback interface [1].

The members exchanged the current state of affairs concerning the role of formal methods in K-12 curricula and teacher education in Switzerland, Israel, The Netherlands, Germany, Brazil, the United States, India, and Australia.

Formal methods include algorithmic reasoning, automata, formal languages, and logic. The group discussed possible advantages and hindrances related to teaching aspects of formal methods in K-12. It was useful in distinguishing societal needs, CS as a discipline, curricular content, and pedagogies.

Potential themes for follow-up activities of the group are:

• $\mathrm{■}$

  Why are formal foundations important in K-12? What should be in a dedicated subject and what is important for “everyone” (or just some group) and why? Which elements are critical for compulsory education? (The situation for CS seems to be different from, eg, physics.) An opinion article (column) could be a result.

• $\mathrm{■}$

  A research study on teachers’ perspectives on the “formal foundations”: content knowledge, teacher beliefs, PCK, and a cross-cultural inventory of teaching practices w.r.t. formal methods.

• $\mathrm{■}$

  A research study on students’ point of view on Computing in society and which elements are based on formal foundations of CS.

• $\mathrm{■}$

  Identifying and utilizing the opportunities w.r.t. ‘reasoning’ at primary and upper primary levels and increasing the logic content across secondary school curricula.

• $\mathrm{■}$

  Cross-cultural studies on specific aspects of formal methods, taking the respective cultural contexts into account.

Reductions are a key method in computability and complexity theory to identify unsolvable or intractable problems. Therefore, learning how to reduce one problem onto another is part of every standard curriculum in such courses. We here report on ideas discussed in a working group with the goal of designing an intervention to help students solving exercises on reductions and thus, foster a better understanding of this rather difficult topic. Moreover, our focus is on tool-supported learning by using generative AI. From a learners perspective, a reduction task between two problems $A$ and $B$ essentially can be seen as a programming exercise, where students need to write an algorithm that converts instances of $A$ into instances of $B$, such that a solution for $B$ can be used to solve $A$. Our idea of an intervention aims at this programming part of reductions. More specifically, an educational tool should be designed to help students plan the solution to a given reduction task. That is, before implementing a reduction between two given problems, students use our intended tool to describe in natural language how their algorithm should convert problem instances. This description is then used as a prompt for an LLM (e.g. ChatGPT 4.0) with the task of actually producing an implementation, e.g. in Python. The latter allows feedback to be computed in two ways. First, the AI-generated algorithm can be tested for correctness of the solution (and the plan), by running it on positive and negative examples of problem $A$ and providing its answer to the students. In the case of incorrect solution attempts, i.e. positive instances of $A$ are mapped to negative instances of $B$, or vice versa, further feedback on how to improve the plan could also be provided by the LLM. We suspect that a carefully designed prompt that includes problem-specific information and meta-information on planning can be used for the latter. As the approach described above is intended to be a first idea on the subject, it is clear that a number of issues need to be addressed before the intervention is actually implemented. Among others, it is unclear how planning of reductions in natural language is perceived by students, and how the quality of a plan can be measured. Furthermore, the quality of LLM-output needs to be investigated, especially, if reduction tasks are complex and/or the plans of students are incomplete or ambiguous.

There is not much existing research on misconceptions for FF and TCS. Therefore, we propose to build a base to build such work on. The format will be to gather teachers’ observations on students’ struggles in courses such as Theory of Computer Science. We do this by creating a form asking for descriptions and example questions that these mistakes occur on. These are collected and organized in a document, which could be written up for a discussion paper. In a later stage, we could follow-up on this research by studying error prevalence and identifying underlying misconceptions.

Additionally, the document could be of use for those building Teaching-Support Systems, as they can gain insight into problems teachers or students typically run into. They could translate this into additional exercises or hints within the TSS.

We discussed the feasibility of doing a large scale study of using teaching support systems to help students learn how to write reduction proofs as part of a computing theory course. Such a study would involve helping 2nd year computer science students learn reduction proofs by using Proof Blocks, Faded Proof Blocks, and feedback from large language models fine-tuned on mathematical proof data. Student proofs would be analyzed through the lens of the following rubric: (1) Overall proof structure is there, (2) Reduction Function is clearly defined, (3) Proving the computability/complexity, (4) Proving the Reduction Property (both directions).

The conversion of formal languages (e.g. set notation to context free grammar or PDA) is a difficult problem for students to tackle. But some tasks are more difficult than others. This leads to the question: What properties make a conversion task difficult? We call such properties difficulty-generating factors. They can help to understand why a specific task might be difficult and to adapt tasks for different needs.

But in which ways can such factors be found systematically? And how can hypothesized factors be verified?

To this end we propose a mixture of qualitative and quantitative research designs. First we want to assess possible difficulty-generating factors. For this we will be doing expert and novice interviews to find out, which aspects of such a task they look at. The tasks for these interviews are informed by existing student performance data.

We will then try to verify the found factors in a randomized control trial study by systematically manipulating the aspects and using Rasch-analysis to compare the result with the expected ranking.

Self-regulated learning (SLR) has been shown to be positively correlated to academic succes (Zimmerman et al. 1992, Greene et al. 2021). In this breakout group, we considered the question of whether – and if so how – data from digital learning environments (DLEs) can be used to gain insights into the state of a self-regulated learning process the learner is currently in. For the sake of conciseness, we decided to focus on the ILTIS DLE while reminding ourselves of the fact that there is a broad spectrum of such systems. Building on Zimmerman’s conceptualization (2008), we used the SRL cycle consisting of “Forethought Phase” – “Performance Phase” – “Self-Reflection Phase”. Going through each of the phases of this cycle, we started with the question which SRL-related variables can be generated or derived by the system and what gaps currently exist. We hypothesize that using these variables, we can create an individual learner profile which then in turn can ultimately be used to suggest tailored interventions to help learners improve their study and learning behavior.