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

arXiv: https://arxiv.org/abs/2502.07789 · HTML: https://mlsanity.com/paper/2502.07789/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 16 references that are in the map.
- First posted on arXiv 20 Jan 2025.

## Builds on (most cited first, 4 of 4)

- [Do Users Write More Insecure Code with AI Assistants?](https://mlsanity.com/paper/2211.03622/) (2022)
- [Conversing with Copilot: Exploring Prompt Engineering for Solving CS1 Problems Using Natural Language](https://mlsanity.com/paper/2210.15157/) (2022)
- [Can GPT-4 Support Analysis of Textual Data in Tasks Requiring Highly Specialized Domain Expertise?](https://mlsanity.com/paper/2306.13906/) (2023)
- [Can ChatGPT support software verification?](https://mlsanity.com/paper/2311.02433/) (2023)

## Built on by (most cited first, 2 of 2)

- [PAT-Agent: Autoformalization for Model Checking](https://mlsanity.com/paper/2509.23675/) (2025)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)

## Abstract (arXiv)

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.