Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny

• URL: http://arxiv.org/abs/2506.22370v2
• Date: Mon, 30 Jun 2025 10:08:05 GMT
• Title: Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
• Authors: Carolina Carreira, Álvaro Silva, Alexandre Abreu, Alexandra Mendes,
• Abstract summary: Students in computing education increasingly use large language models (LLMs) such as ChatGPT.<n>This paper investigates how students interact with an LLM when solving formal verification exercises in Dafny.
• Score: 79.56218230251953
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Students in computing education increasingly use large language models (LLMs) such as ChatGPT. Yet, the role of LLMs in supporting cognitively demanding tasks, like deductive program verification, remains poorly understood. This paper investigates how students interact with an LLM when solving formal verification exercises in Dafny, a language that supports functional correctness, by allowing programmers to write formal specifications and automatically verifying that the implementation satisfies the specification. We conducted a mixed-methods study with master's students enrolled in a formal methods course. Each participant completed two verification problems, one with access to a custom ChatGPT interface that logged all interactions, and the other without. We identified strategies used by successful students and assessed the level of trust students place in LLMs. Our findings show that students perform significantly better when using ChatGPT; however, performance gains are tied to prompt quality. We conclude with practical recommendations for integrating LLMs into formal methods courses more effectively, including designing LLM-aware challenges that promote learning rather than substitution.

Related papers

• LLMs are Imperfect, Then What? An Empirical Study on LLM Failures in Software Engineering [38.20696656193963]
  We conducted an observational study with 22 participants using ChatGPT as a coding assistant in a non-trivial software engineering task. We identified the cases where ChatGPT failed, their root causes, and the corresponding mitigation solutions used by users.
  arXiv  Detail & Related papers  (2024-11-15T03:29:41Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• Exploring Knowledge Tracing in Tutor-Student Dialogues using LLMs [49.18567856499736]
  We investigate whether large language models (LLMs) can be supportive of open-ended dialogue tutoring.<n>We apply a range of knowledge tracing (KT) methods on the resulting labeled data to track student knowledge levels over an entire dialogue.<n>We conduct experiments on two tutoring dialogue datasets, and show that a novel yet simple LLM-based method, LLMKT, significantly outperforms existing KT methods in predicting student response correctness in dialogues.
  arXiv  Detail & Related papers  (2024-09-24T22:31:39Z)
• I don't trust you (anymore)! -- The effect of students' LLM use on Lecturer-Student-Trust in Higher Education [0.0]
  Large Language Models (LLMs) in platforms like Open AI's ChatGPT, has led to their rapid adoption among university students.<n>This study addresses the research question: How does the use of LLMs by students impact Informational and Procedural Justice, influencing Team Trust and Expected Team Performance?<n>Our findings indicate that lecturers are less concerned about the fairness of LLM use per se but are more focused on the transparency of student utilization.
  arXiv  Detail & Related papers  (2024-06-21T05:35:57Z)
• The GPT Surprise: Offering Large Language Model Chat in a Massive Coding Class Reduced Engagement but Increased Adopters Exam Performances [26.688772122455745]
  Large language models (LLMs) are quickly being adopted in a wide range of learning experiences. We conducted a large-scale randomized control trial with 5,831 students from 146 countries in an online coding class. We estimate positive benefits on exam performance for adopters, the students who used the tool, but over all students, the advertisement of GPT-4 led to a significant average decrease in exam participation.
  arXiv  Detail & Related papers  (2024-04-25T15:39:22Z)
• Toward Self-Improvement of LLMs via Imagination, Searching, and Criticizing [56.75702900542643]
  We introduce AlphaLLM for the self-improvements of Large Language Models.<n>It integrates Monte Carlo Tree Search (MCTS) with LLMs to establish a self-improving loop.<n>Our experimental results show that AlphaLLM significantly enhances the performance of LLMs without additional annotations.
  arXiv  Detail & Related papers  (2024-04-18T15:21:34Z)
• Rethinking the Roles of Large Language Models in Chinese Grammatical Error Correction [62.409807640887834]
  Chinese Grammatical Error Correction (CGEC) aims to correct all potential grammatical errors in the input sentences. LLMs' performance as correctors on CGEC remains unsatisfactory due to its challenging task focus. We rethink the roles of LLMs in the CGEC task so that they can be better utilized and explored in CGEC.
  arXiv  Detail & Related papers  (2024-02-18T01:40:34Z)
• Why and When LLM-Based Assistants Can Go Wrong: Investigating the Effectiveness of Prompt-Based Interactions for Software Help-Seeking [5.755004576310333]
  Large Language Model (LLM) assistants have emerged as potential alternatives to search methods for helping users navigate software. LLM assistants use vast training data from domain-specific texts, software manuals, and code repositories to mimic human-like interactions.
  arXiv  Detail & Related papers  (2024-02-12T19:49:58Z)
• AlignedCoT: Prompting Large Language Models via Native-Speaking Demonstrations [52.43593893122206]
  Alignedcot is an in-context learning technique for invoking Large Language Models. It achieves consistent and correct step-wise prompts in zero-shot scenarios. We conduct experiments on mathematical reasoning and commonsense reasoning.
  arXiv  Detail & Related papers  (2023-11-22T17:24:21Z)
• ChatABL: Abductive Learning via Natural Language Interaction with ChatGPT [72.83383437501577]
  Large language models (LLMs) have recently demonstrated significant potential in mathematical abilities. LLMs currently have difficulty in bridging perception, language understanding and reasoning capabilities. This paper presents a novel method for integrating LLMs into the abductive learning framework.
  arXiv  Detail & Related papers  (2023-04-21T16:23:47Z)
• ICL-D3IE: In-Context Learning with Diverse Demonstrations Updating for Document Information Extraction [56.790794611002106]
  Large language models (LLMs) have demonstrated remarkable results in various natural language processing (NLP) tasks with in-context learning. We propose a simple but effective in-context learning framework called ICL-D3IE. Specifically, we extract the most difficult and distinct segments from hard training documents as hard demonstrations.
  arXiv  Detail & Related papers  (2023-03-09T06:24:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.