Reproduce “Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Carolina Carreira, Álvaro Silva, Alexandre Abreu, Alexandra Mendes
Researchers from Carnegie Mellon University and the University of Porto conducted an experimental study demonstrating that Large Language Models substantially enhance master's students' performance in deductive software verification tasks using Dafny. The study revealed that while LLMs improve correctness, especially for implementation, effective use relies on specific prompting strategies and does not inherently foster deeper understanding or trust.
Key insights
- More successful students employ strategic prompting, including providing full contextual information, breaking complex problems into smaller subproblems, and strategically redirecting the LLM rather than demanding direct fixes.
- LLMs demonstrated greater effectiveness in assisting with implementation tasks compared to formal specification tasks, suggesting a disparity in their training data coverage for different aspects of verification.
- Despite significant performance gains with LLM assistance, improved objective correctness did not consistently translate into higher student confidence or a deeper conceptual understanding of the underlying formal methods.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.