Do AI assistants help students write formal specifications? A study with ChatGPT and the B-Method

TL;DR

This study evaluates whether ChatGPT assists undergraduate students in writing formal B-method specifications, finding limited help in correctness and highlighting trust and interaction patterns as influential factors.

Contribution

It is the first to empirically assess ChatGPT's impact on formal specification tasks and student trust in this context.

Findings

ChatGPT does not improve correctness of B-specifications.

Lower trust in ChatGPT correlates with better student outcomes.

A specific interaction pattern with ChatGPT influences correctness.

Abstract

This paper investigates the role of AI assistants, specifically OpenAI's ChatGPT, in teaching formal methods (FM) to undergraduate students, using the B-method as a formal specification technique. While existing studies demonstrate the effectiveness of AI in coding tasks, no study reports on its impact on formal specifications. We examine whether ChatGPT provides an advantage when writing B-specifications and analyse student trust in its outputs. Our findings indicate that the AI does not help students to enhance the correctness of their specifications, with low trust correlating to better outcomes. Additionally, we identify a behavioural pattern with which to interact with ChatGPT which may influence the correctness of B-specifications.