[en] 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.
Disciplines :
Computer science
Author, co-author :
CAPOZUCCA, Alfredo ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
Yampolskyi, Daniil; University of Luxembourg, Department of Computer Science, Esch-sur-Alzette, Luxembourg
Goldberg, Alexander; University of Luxembourg, Department of Computer Science, Esch-sur-Alzette, Luxembourg
Cristia, Maximiliano; Universidad Nacional de Rosario and Cifasis, Rosario, Argentina
External co-authors :
yes
Language :
English
Title :
Do AI Assistants Help Students Write Formal Specifications? A Study with ChatGPT and the B-Method
Publication date :
2025
Event name :
2025 IEEE/ACM 37th International Conference on Software Engineering Education and Training (CSEE&T)
Event place :
Ottawa, Can
Event date :
28-04-2025 => 29-04-2025
By request :
Yes
Audience :
International
Main work title :
Proceedings - 2025 IEEE/ACM 37th International Conference on Software Engineering Education and Training, CSEE and T 2025
Publisher :
Institute of Electrical and Electronics Engineers Inc.
M. Broy, A. Brucker, A. Fantechi, M. Gleirscher, K. Havelund, M. A. Kuppe, A. Mendes, A. Platzer, J. Ringert, and A. Sullivan, "Does Every Computer Scientist Need to Know Formal Methods?" Form. Asp. Comput., Jun. 2024, just Accepted. [Online]. Available: https://doi. org/10. 1145/3670795
B. Dongol, C. Dubois, S. Hallerstede, E. Hehner, C. Morgan, P. Müller, L. Ribeiro, A. Silva, G. Smith, and E. de Vink, "On Formal Methods Thinking in Computer Science Education, " Form. Asp. Comput., Jun. 2024, just Accepted. [Online]. Available: https://doi. org/10. 1145/3670419
T. Guardian, "More Than Half of UK Undergraduates Admit Using AI to Write Essays, " 2024, accessed: 2024-10-05. [Online]. Available: https://www. Theguardian. com/technology/2024/feb/01/more-than-half-uk-undergraduates-ai-essays-artificial-intelligence
H. E. P. I. (HEPI). (2024) Provide or punish? Students' views on generative AI in higher education. Accessed: 2024-10-05. [Online]. Available: https://www. hepi. ac. uk/2024/02/01/provide-or-punish-students-views-on-generative-ai-in-higher-education/
J. Finnie-Ansley, P. Denny, B. A. Becker, A. Luxton-Reilly, and J. Prather, "The robots are coming: Exploring the implications of openai codex on introductory programming, " in Proceedings of the 24th Australasian Computing Education Conference, ser. ACE '22. New York, NY, USA: Association for Computing Machinery, 2022, p. 10-19. [Online]. Available: https://doi. org/10. 1145/3511861. 3511863
P. Denny, V. Kumar, and N. Giacaman, "Conversing with Copilot: Exploring Prompt Engineering for Solving CS1 Problems Using Natural Language, " in Proceedings of the 54th ACM Technical Symposium on Computer Science Education V. 1, ser. SIGCSE 2023. New York, NY, USA: Association for Computing Machinery, 2023, p. 1136-1142. [Online]. Available: https://doi. org/10. 1145/3545945. 3569823
J. Savelka, A. Agarwal, C. Bogart, Y. Song, and M. Sakr, "Can Generative Pre-trained Transformers (GPT) Pass Assessments in Higher Education Programming Courses?" in Proceedings of the 2023 Conference on Innovation and Technology in Computer Science Education V. 1, ser. ITiCSE 2023. New York, NY, USA: Association for Computing Machinery, 2023, p. 117-123. [Online]. Available: https://doi. org/10. 1145/3587102. 3588792
S. Schneider, The B-Method: An Introduction, ser. Cornerstones of Computing. Palgrave, 2001.
N. Perry, M. Srivastava, D. Kumar, and D. Boneh, "Do Users Write More Insecure Code with AI Assistants?" in Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, ser. CCS '23. New York, NY, USA: Association for Computing Machinery, 2023, p. 2785-2799. [Online]. Available: https://doi. org/10. 1145/3576915. 3623157
J. R. Abrial, The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
M. Butler, P. Körner, S. Krings, T. Lecomte, M. Leuschel, L.-F. Mejia, and L. Voisin, "The First Twenty-Five Years of Industrial Use of the B-Method, " Berlin, Heidelberg, p. 189-209, 2020. [Online]. Available: https://doi. org/10. 1007/978-3-030-58298-2 8
C. Jansen, C. Richter, and H. Wehrheim, "Can chatgpt support software verification?" in Fundamental Approaches to Software Engineering, D. Beyer and A. Cavalcanti, Eds. Cham: Springer Nature Switzerland, 2024, pp. 266-279.
Trochim, Donnelly, and A. Kanika, Research Methods: The Essential Knowledge Base. Cengage Learning, 2015.
A. Marzal and E. Vidal, "Computation of normalized edit distance and applications, " IEEE Transactions on Pattern Analysis and Machine Intelligence, vol. 15, no. 9, pp. 926-932, 1993.
A. Capozucca, D. Yampolskyi, A. Goldberg, and M. Cristiá, "Do ai assistants help students write formal specifications? a study with chatgpt and the b-method, " Oct. 2024. [Online]. Available: https://doi. org/10. 5281/zenodo. 13914857
