Using Formal Methods to Validate Research Hypotheses: The Duolingo Case Study

Abstract

In this paper we present a methodology that combines formal methods and informal research methods to validate research hypotheses. We use the CSP (Communicating Sequential Processes) process algebra to model the system as well as some aspects of the user, and PAT (Process Analysis Toolkit) to perform formal verification. We illustrate our methodology on Duolingo, a very popular application for language learning. Two kinds of data are considered: a log of the interaction of the user with the application and the assessment of the user’s level of proficiency in the language to be learned (subject profile). The goal is to validate research hypotheses that relate the subject profile to the user’s cognitive approach during interaction (cognitive profile). To this purpose, two CSP processes, one modelling the cognitive profile that is associated by the considered research hypothesis to the subject profile and one modelling the interaction log are composed in parallel with the system model. Thus, for each user with the given learner profile and specific interaction log, the verification of the functional correctness of the overall system validates the correlation between cognitive profile and subject profile.