Pith. sign in

REVIEW 1 major objections 4 minor 25 references

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

T0 review · 1 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Access to ChatGPT significantly improved master's students' performance on Dafny formal verification exercises, with all 14 passing the LLM-assisted problem and only 5 passing unaided.

desk verdict The Dafny LLM study has a real, interesting result, but the headline effect size is misreported (5.04 vs 8.03 points) and needs correction before that number is trusted. read the letter →

arxiv 2506.22370 v4 pith:M422PF53 submitted 2025-06-27 cs.SE cs.PL

Carolina Carreira , Álvaro Silva , Alexandre Abreu , Alexandra Mendes This is my paper · ORCID
classification cs.SEcs.PL
keywords largelanguagemodelsDafnyformalverificationdeductivesoftwarecorrectnesscomputingeducationpromptengineeringmixed-methodsstudy
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper reports a controlled experiment asking whether large language models help students do deductive program verification, a cognitively demanding task in which a tool like Dafny checks that code satisfies formal specifications. Fourteen master's students each solved two Dafny problems, one with access to a custom ChatGPT interface and one without, with problem order and condition randomized. The central finding is that students scored on average 5.04 points higher out of 20 when using ChatGPT (17.39 vs. 9.36, p = 0.0002), and all 14 passed the LLM-assisted problem while only five passed without it. The paper argues the benefit is real but conditional: success depended on prompt quality and on students' willingness to interact strategically with the model, and ChatGPT was markedly better at implementation tasks than at writing specifications. These results matter because they are among the first evidence on LLM use in formal methods education, where the correctness bar is high and naive reliance on AI-generated code is risky.

What carries the argument

The load-bearing mechanism is the within-subject paired comparison combined with prompt logging. Each of the 14 participants solved two Dafny problems of supposedly comparable difficulty (Queue and Tree), one with and one without ChatGPT, with the order and condition balanced by bucketed randomization; the custom ChatGPT wrapper recorded every prompt and model response, enabling a paired-samples t-test on the 0–20 rubric grades (p = 0.0002, mean difference 5.04) and a double-blind qualitative coding of interaction strategies that separates high, middle, and low performers. Dafny itself is part of the machinery: because the language's verifier gives immediate feedback on whether code meets its specification, it provides an objective correctness signal that students and the study use to judge the LLM's output.

What would settle it

A direct falsifier would be an independent replication with a larger sample (say 30 or more participants) using the same two problems while balancing which one receives LLM access, or a pre-registered difficulty-equivalence study of Queue and Tree on a separate cohort: if the paired LLM gain shrinks to nothing in that design, or if the two problems' unaided scores diverge substantially, the claim that ChatGPT itself drives the improvement is undercut.

Watch

Extended reading notes

Core claim

The paper sets out to establish that LLMs can substantially help novice users prove software correctness in Dafny, under the right conditions. In a within-subject design, every participant completed both a Queue problem and a Tree problem, once with ChatGPT (behind a logging interface) and once without. After grading with a 0–20 rubric, the authors found a statistically significant paired difference of 5.04 points (d = 1.55, 95% CI [4.59, 11.47]), with mean scores 17.39 with the LLM versus 9.36 without; all 14 participants passed with ChatGPT, versus 5 without. A qualitative coding of the 103 prompts and 206 total messages showed that higher-scoring students copied the full class into the prompt, broke the problem into a single subproblem, avoided unproductive redirections such as demanding lemmas, and built on partial implementations of their own. The authors conclude that ChatGPT serves as a collaborator rather than a solver, and that its value is highest for implementation steps and lowest for specification writing.

Load-bearing premise

The measured effect depends on the assumption that the two problems, Queue and Tree, are genuinely equal in difficulty and that their grading rubrics yield comparable scores; the only evidence for this is a low-power t-test on the same 14 participants, so a modest difficulty gap could inflate or deflate the reported 5.04-point advantage.

Editorial extensions

If this is right

  • Formal methods instructors can treat LLMs as a support tool rather than a threat, but the main benefit shows up in implementation tasks, so exercises should keep specification writing as the human-owned part.
  • Teaching prompting strategy—provide full program context, focus on one subproblem at a time, avoid over-complicated redirections—is a direct lever for improving how much students gain from LLM assistance.
  • For students who cannot start a proof unaided, ChatGPT can carry them to a passing solution, but it does not automatically raise their confidence or understanding, so assessment must probe conceptual grasp separately.
  • The gap between implementation and specification performance implies that LLM-resistant assessment could focus on contracts, invariants, and other formal annotations rather than on generating code.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The comparability of the Queue and Tree problems rests on a post-hoc t-test with only 14 participants (t = -0.653, p = 0.525, d = 0.28); with that sample size the test has low power, so a true difficulty gap of a few points could meaningfully shift the reported 5.04-point effect, and replication should pre-test difficulty on a separate cohort.
  • The implementation-over-specification pattern points to a division of labor for industrial verification work: humans should own the correctness properties and contracts while LLMs fill in code, the reverse of how generative AI is often marketed.
  • The seven-to-seven trust split, with distrust frequently driven by syntax errors, suggests Dafny's built-in verifier can act as a trustworthy fact-checker for LLM output; this may generalize to other verification-aware languages and could be taught explicitly.
  • Participants P8 and P6 obtained near-perfect solutions from a single or slightly varied prompt, so for at least some problems the boundary between collaborator and solver is already thin; as models improve, the paper's 'collaborator not solver' framing may need revisiting.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 4 minor

Summary. The paper reports a controlled mixed-methods study with 14 master's students who each solved two Dafny verification problems, one with access to a custom ChatGPT interface and one without. The abstract claims that students perform significantly better when using ChatGPT. Section 4 reports mean grades of 17.39 with the LLM and 9.36 without, with a paired t-test (p = 0.0002) and an effect size d = 1.55; the paper states that 'participants scored 5.04 points higher' with ChatGPT. Section 5 analyzes interaction logs to identify prompting strategies (e.g., including class context, reducing to one subproblem) that distinguish higher-performing students, and Section 6 reports mixed trust attitudes. The paper concludes with pedagogical recommendations including LLM-aware challenge design.

Significance. The study addresses a timely and underexplored question: whether LLMs help students with deductive verification, a cognitively demanding task where prior work is scarce. Its strengths include a randomized paired design, log-based interaction data, blinded qualitative coding, and a concrete educational context. If the reported effect is accurate, the result is practically significant and contributes to the growing evidence on LLM use in computing education. The evidence for the headline claim is directionally strong (all participants passed with the LLM vs. only 5 of 14 without), but the paper's internal numerical inconsistency and the low-power comparability check mean the precise magnitude of the benefit is not currently established. The qualitative findings on prompting strategies are exploratory but plausible and useful.

major comments (1)
  1. [Section 4 (RQ1 Performance)] The correctness assessment procedure in Section 3.2 relies on researcher-designed rubrics with task weights assigned according to 'effort and difficulty', but no inter-rater reliability is reported. The paper describes a double-blind iterative coding process that reached consensus, yet without a statistic such as Cohen's kappa, the reliability of the 0–20 grades—the primary outcome measure—is not established. Since all grades were assigned by the research team using bespoke rubrics, this is a nontrivial threat to the objectivity of the performance comparison. The authors should report inter-rater reliability on at least a subset of solutions, or clearly state the absence of such a check as a limitation.
minor comments (4)
  1. [Section 3.1] The model identifier is written as 'gpt-4_1-2025-04-14'; this appears to be a typo and should likely be 'gpt-4.1-2025-04-14' or similar, and the exact model version should be clarified.
  2. [Section 4] In the sub-analysis of specification vs. implementation tasks, the paper removes one outlier post hoc to satisfy normality assumptions. This is a secondary analysis, but the outlier removal should be described more transparently (e.g., which participant, what score, and whether the conclusion holds without removal) to avoid the appearance of cherry-picking.
  3. [Section 5.2] Figure 2 is dense and the proportionality of group sizes is not immediately evident; adding percentages per group or a small table would improve readability.
  4. [Section 2] The related-work discussion would benefit from concluding with a clearer statement of how this study's classroom setting and focus on student interaction with an LLM differs from the cited tool-generation work (e.g., Clover, Misu et al., Pascoal et al.), rather than relying on the later 'first empirical study' claim.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the empirical comparison is self-contained and not derived from its inputs, though one reported effect magnitude is internally inconsistent (a reporting error, not circularity).

full rationale

The paper's central claim—that students perform significantly better with ChatGPT—is an empirical result from a crossover experiment, not a derivation from an assumed premise. The grades were observed, the rubrics were applied to those observations, and the paired t-test and effect sizes are computed from the observed grades rather than being used to define the conclusion. The comparability check between the Queue and Tree problems is a post-hoc statistical test on the same data, used as construct-validity evidence; its low power is a statistical concern, but it does not make the inference circular. The self-citations (e.g., Silva et al. [21], Wu et al. [24]) appear in background and related-work sections and are not load-bearing for the main finding. No uniqueness theorem or ansatz is imported from prior author work, and no fitted parameter is renamed as a prediction. The manuscript explicitly acknowledges its limitations: small sample size, a single LLM platform, and possible task-sequence effects. The skeptical observation that the reported 5.04-point average gain is inconsistent with the group means (17.39 vs. 9.36, difference 8.03) and equals the t-statistic is a concrete, checkable reporting error that affects the precision of the main result, but it is a correctness and consistency issue, not a circularity issue. The derivation chain therefore contains no circular step.

Assumptions & free parameters 3 free parameters · 3 assumptions · 0 invented entities

The central claim rests on methodological choices (rubric weights, problem tuning, time limits) rather than on fitted physical parameters. The main statistical result is a within-subject comparison; its validity depends on the comparability of the two problems and on the rubric, which are researcher-designed.

free parameters (3)
  • Rubric task weights
    Section 3.2: 'We gave weights for these tasks according to their effort and difficulty.' These hand-assigned weights define the grades that drive the main comparison; they are not derived from data.
  • Problem selection and difficulty (Queue vs Tree)
    Section 3.1: problems 'developed iteratively over five pilot runs' and 'slightly different from each other to mitigate learning effects.' Difficulty was tuned by the authors; comparability is checked only with a low-power post-hoc test.
  • 30-minute time limit per problem
    Section 3.1: 'Participants had a maximum of 30 minutes per problem.' The limit is chosen by hand and affects both conditions, but may interact with LLM speed.
assumptions (3)
  • domain assumption The grading rubric is a valid measurement of Dafny verification skill, and Queue/Tree grades are commensurable.
    Used throughout Section 4 for paired comparisons; comparability is only supported by an underpowered test in Section 3.1.
  • domain assumption Classifying tasks as specification vs implementation (Section 3.2) captures a meaningful cognitive distinction relevant to LLM support.
    This classification underlies the RQ1 sub-analysis in Section 4 and the recommendation to emphasize specification tasks.
  • standard math Normality assumptions for paired t-tests are met (verified by Shapiro-Wilk).
    Section 4: normality is supported after removing one outlier for the sub-analysis.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny." pith.science (2026). https://pith.science/paper/M422PF53

@misc{pith2026250622370,
  author       = {Pith},
  title        = {Pith review of: Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/M422PF53}},
  note         = {Machine review of arXiv:2506.22370}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2506.22370 by the authors.

Figure 1
Figure 1. Overview of the study’s methodology Survey. We deployed the survey using Qualtrics. The survey served as the study’s entry point and central coordination tool. Participants used the survey to provide informed consent, receive instructions, and access the exercises. After completing each problem, participants returned to the survey to upload their work and respond to follow-up questions. We designed the survey to pre… view at source ↗
Figure 2
Figure 2. Qualitative comparison of interaction patterns across participant groups [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. Participants’ responses to whether they trusted ChatGPT during the [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

25 extracted references · 20 canonical work pages

  1. [1]

    Broy, M., Brucker, A.D., Fantechi, A., Gleirscher, M., Havelund, K., Kuppe, M.A., Mendes, A., Platzer, A., Ringert, J.O., Sullivan, A.: Does every computer scientist need to know formal methods? Formal Aspects of Computing37(1), 1–17 (2024)

    work page 2024

  2. [2]

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

    Capozucca, A., Yampolskyi, D., Goldberg, A., Cristiá, M.: Do AI assistants help students write formal specifications? a study with ChatGPT and the B-Method. arXiv preprint arXiv:2502.07789 (2025)

    work page Pith review arXiv 2025

  3. [3]

    In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs

    Farrell, M., Reynolds, C., Monahan, R.: Using Dafny to solve the VerifyThis 2021 challenges. In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs. pp. 32–38 (2021)

    work page 2021

  4. [4]

    Computers and Education: Artificial Intelligence7, 100290 (2024)

    Groothuijsen, S., van den Beemt, A., Remmers, J.C., van Meeuwen, L.W.: AI chatbots in programming education: students’ use in a scientific computing course and consequences for learning. Computers and Education: Artificial Intelligence7, 100290 (2024)

    work page 2024

  5. [5]

    Hanifi, K., Cetin, O., Yilmaz, C.: On ChatGPT: Perspectives from software engi- neeringstudents.In:2023IEEE23rdInternationalConferenceonSoftwareQuality, Reliability, and Security (QRS). pp. 196–205. IEEE (2023)

    work page 2023

  6. [6]

    Applied Sciences14(10), 4115 (2024)

    Jošt, G., Taneski, V., Karakatič, S.: The impact of large language models on programming education and student learning outcomes. Applied Sciences14(10), 4115 (2024)

    work page 2024

  7. [7]

    In: International conference on logic for programming artificial intelligence and reasoning

    Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: International conference on logic for programming artificial intelligence and reasoning. pp. 348–370. Springer (2010)

    2010

  8. [8]

    arXiv preprint arXiv:2406.08467 (2024)

    Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M.R.H., Amin, N., Tegmark, M.: DafnyBench: A benchmark for formal software verification. arXiv preprint arXiv:2406.08467 (2024)

    arXiv 2024

Show all 25 references
  1. [9]

    In: Proceedings of the 56th ACM Technical Symposium on Computer Science Education V

    McDanel, B., Novak, E.: Designing LLM-resistant programming assignments: In- sights and strategies for cs educators. In: Proceedings of the 56th ACM Technical Symposium on Computer Science Education V. 1. pp. 756–762 (2025)

    2025

  2. [10]

    arXiv preprint arXiv:2410.18494 (2024)

    Mirchev, M., Costea, A., Singh, A.K., Roychoudhury, A.: Assured automatic pro- gramming via large language models. arXiv preprint arXiv:2410.18494 (2024)

    2024 arXiv

  3. [11]

    Proceedings of the ACM on Software Engineering1(FSE), 812–835 (2024)

    Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards AI-assisted synthesis of verified Dafny methods. Proceedings of the ACM on Software Engineering1(FSE), 812–835 (2024)

    2024

  4. [12]

    Proceedings of the ACM on Programming Languages9(OOPSLA1), 1519–1545 (2025)

    Mugnier, E., Gonzalez, E.A., Polikarpova, N., Jhala, R., Yuanyuan, Z.: Laurel: Unblocking automated verification with large language models. Proceedings of the ACM on Programming Languages9(OOPSLA1), 1519–1545 (2025)

    2025

  5. [13]

    In: NASA Formal Methods Symposium

    Noble, J., Streader, D., Gariano, I.O., Samarakoon, M.: More programming than programming: Teaching formal methods in a software engineering programme. In: NASA Formal Methods Symposium. pp. 431–450. Springer (2022)

    2022

  6. [14]

    In: International Conference on Fundamentals of Software Engineering

    Pascoal Faria, J., Trigo, E., Abreu, R.: Automatic generation of loop invariants in Dafny with large language models. In: International Conference on Fundamentals of Software Engineering. pp. 138–154. Springer (2025) 18 C. Carreira et al

    2025

  7. [15]

    arXiv preprint arXiv:2411.15143 (2024)

    Poesia, G., Loughridge, C., Amin, N.: Dafny-Annotator: AI-assisted verification of Dafny programs. arXiv preprint arXiv:2411.15143 (2024)

    2024 arXiv

  8. [16]

    In: Proceedings of the ACM Con- ference on Global Computing Education Vol 1

    Prasad, S., Greenman, B., Nelson, T., Krishnamurthi, S.: Generating programs trivially: student use of large language models. In: Proceedings of the ACM Con- ference on Global Computing Education Vol 1. pp. 126–132 (2023)

    2023

  9. [17]

    It’s weird that it knows what I want

    Prather, J., Reeves, B.N., Denny, P., Becker, B.A., Leinonen, J., Luxton-Reilly, A., Powell, G., Finnie-Ansley, J., Santos, E.A.: “It’s weird that it knows what I want”: UsabilityandinteractionswithCopilotfornoviceprogrammers.ACMTransactions on Computer-Human Interaction31(1),...

    2023

  10. [18]

    In: Proceedings of the 2024 ACM Conference on International Computing Education Research-Volume 1

    Prather, J., Reeves, B.N., Leinonen, J., MacNeil, S., Randrianasolo, A.S., Becker, B.A., Kimmel, B., Wright, J., Briggs, B.: The widening gap: The benefits and harms of generative AI for novice programmers. In: Proceedings of the 2024 ACM Conference on International Computing ...

    2024

  11. [19]

    arXiv preprint arXiv:2304.11214 (2023)

    Qureshi, B.: Exploring the use of ChatGPT as a tool for learning and assessment in undergraduate computer science curriculum: Opportunities and challenges. arXiv preprint arXiv:2304.11214 (2023)

    2023 arXiv

  12. [20]

    Rungta,N.:AbillionSMTqueriesaday.In:InternationalConferenceonComputer Aided Verification. pp. 3–18. Springer (2022)

    2022

  13. [21]

    In: Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)

    Silva, Á.F., Mendes, A., Ferreira, J.F.: Leveraging large language models to boost Dafny’s developers productivity. In: Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE). pp. 138–142 (2024)

    2024

  14. [22]

    In: International Symposium on AI Verification

    Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: Closed-loop verifiable code generation. In: International Symposium on AI Verification. pp. 134–155. Springer (2024)

    2024

  15. [23]

    International Journal of Educational Technology in Higher Education21(1), 14 (2024)

    Sun, D., Boudouaia, A., Zhu, C., Li, Y.: Would ChatGPT-facilitated program- ming mode impact college students’ programming behaviors, performances, and perceptions? an empirical study. International Journal of Educational Technology in Higher Education21(1), 14 (2024)

    2024

  16. [24]

    In: 23rd International Conference on Software Engineering and Formal Methods (SEFM) (2025)

    Wu, V., Mendes, A., Abreu, A.: Specification-guided repair of arithmetic errors in Dafny programs using LLMs. In: 23rd International Conference on Software Engineering and Formal Methods (SEFM) (2025)

    2025

  17. [25]

    In: Proceedings of the 46th International Conference on Software Engineering: Software Engineering Education and Training

    Xue, Y., Chen, H., Bai, G.R., Tairas, R., Huang, Y.: Does ChatGPT help with introductory programming? An experiment of students using ChatGPT in CS1. In: Proceedings of the 46th International Conference on Software Engineering: Software Engineering Education and Training. pp. ...

    2024

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.