arXiv subjects

Iris Ma

Publications and source records attributed to Iris Ma.

6 recordsLinked to original sources

arXiv2026

Spec-Harness: Measuring and Improving Behavioral Adequacy of LLM-Synthesized Formal Specifications

Formal specifications play a central role in ensuring software reliability, yet automatically synthesizing high-quality specifications remains difficult and often requires domain expertise. Recent work has applied large language models to generate specifications in the Java Modeling Language (JML), reporting high verifier pass rates. But passing a verifier only confirms that an implementation is consistent with a specification, not that the specification is meaningful. A trivial postcondition such as ensures true satisfies any verifier while saying nothing about the code. How much behavior, then, does a verifier-accepted specification actually capture? In this work, we first compare classical and prompt-based JML synthesis approaches under a unified setup, and find that prompt optimization through verification feedback raises pass rates but reaches a clear ceiling. We then introduce Spec-Harness, a framework that measures the behavioral adequacy of a specification along four dimensions of precondition and postcondition correctness and completeness, using Hoare-triple based symbolic verification and input/output mutation. Spec-Harness reveals that many verifier-accepted specifications, including optimized ones, are behaviorally weak, over- or under-constraining inputs and outputs in ways the verifier cannot see. Finally, we show that Spec-Harness works as a feedback signal that helps coding agents synthesize specifications with higher behavioral adequacy, including general-purpose agents such as Codex CLI and Claude Code, as well as VeriAct, a JML-specialized agent we build for this study.

cs.SE↗

arXiv2025

Memorization: A Close Look at Books

To what extent can entire books be extracted from LLMs? Using the Llama 3 70B family of models, and the "prefix-prompting" extraction technique, we were able to auto-regressively reconstruct, with a very high level of similarity, one entire book (Alice's Adventures in Wonderland) from just the first 500 tokens. We were also able to obtain high extraction rates on several other books, piece-wise. However, these successes do not extend uniformly to all books. We show that extraction rates of books correlate with book popularity and thus, likely duplication in the training data. We also confirm the undoing of mitigations in the instruction-tuned Llama 3.1, following recent work (Nasr et al., 2025). We further find that this undoing comes from changes to only a tiny fraction of weights concentrated primarily in the lower transformer blocks. Our results provide evidence of the limits of current regurgitation mitigation strategies and introduce a framework for studying how fine-tuning affects the retrieval of verbatim memorization in aligned LLMs.

cs.CL↗

arXiv2024

Integrating AI Tutors in a Programming Course

RAGMan is an LLM-powered tutoring system that can support a variety of course-specific and homework-specific AI tutors. RAGMan leverages Retrieval Augmented Generation (RAG), as well as strict instructions, to ensure the alignment of the AI tutors' responses. By using RAGMan's AI tutors, students receive assistance with their specific homework assignments without directly obtaining solutions, while also having the ability to ask general programming-related questions. RAGMan was deployed as an optional resource in an introductory programming course with an enrollment of 455 students. It was configured as a set of five homework-specific AI tutors. This paper describes the interactions the students had with the AI tutors, the students' feedback, and a comparative grade analysis. Overall, about half of the students engaged with the AI tutors, and the vast majority of the interactions were legitimate homework questions. When students posed questions within the intended scope, the AI tutors delivered accurate responses 98% of the time. Within the students used AI tutors, 78% reported that the tutors helped their learning. Beyond AI tutors' ability to provide valuable suggestions, students reported appreciating them for fostering a safe learning environment free from judgment.

cs.CY↗

arXiv2024

Towards AI-Assisted Synthesis of Verified Dafny Methods

Large language models show great promise in many domains, including programming. A promise is easy to make but hard to keep, and language models often fail to keep their promises, generating erroneous code. A promising avenue to keep models honest is to incorporate formal verification: generating programs' specifications as well as code so that the code can be proved correct with respect to the specifications. Unfortunately, existing large language models show a severe lack of proficiency in verified programming. In this paper, we demonstrate how to improve two pretrained models' proficiency in the Dafny verification-aware language. Using 178 problems from the MBPP dataset, we prompt two contemporary models (GPT-4 and PaLM-2) to synthesize Dafny methods. We use three different types of prompts: a direct Contextless prompt; a Signature prompt that includes a method signature and test cases, and a Chain of Thought (CoT) prompt that decomposes the problem into steps and includes retrieval augmentation generated example problems and solutions. Our results show that GPT-4 performs better than PaLM-2 on these tasks and that both models perform best with the retrieval augmentation generated CoT prompt. GPT-4 was able to generate verified, human-evaluated, Dafny methods for 58% of the problems, however, GPT-4 managed only 19% of the problems with the Contextless prompt, and even fewer (10%) for the Signature prompt. We are thus able to contribute 153 verified Dafny solutions to MBPP problems, 50 that we wrote manually, and 103 synthesized by GPT-4. Our results demonstrate that the benefits of formal program verification are now within reach of code generating large language models...

cs.SE↗

arXiv2024

Commit Messages in the Age of Large Language Models

Commit messages are explanations of changes made to a codebase that are stored in version control systems. They help developers understand the codebase as it evolves. However, writing commit messages can be tedious and inconsistent among developers. To address this issue, researchers have tried using different methods to automatically generate commit messages, including rule-based, retrieval-based, and learning-based approaches. Advances in large language models offer new possibilities for generating commit messages. In this study, we evaluate the performance of OpenAI's ChatGPT for generating commit messages based on code changes. We compare the results obtained with ChatGPT to previous automatic commit message generation methods that have been trained specifically on commit data. Our goal is to assess the extent to which large pre-trained language models can generate commit messages that are both quantitatively and qualitatively acceptable. We found that ChatGPT was able to outperform previous Automatic Commit Message Generation (ACMG) methods by orders of magnitude, and that, generally, the messages it generates are both accurate and of high-quality. We also provide insights, and a categorization, for the cases where it fails.

cs.SE↗

arXiv2023

Improving the Quality of Commit Messages in Students' Projects

Commit messages play a crucial role in collaborative software development. They provide a clear and concise description of the changes made to the source code. However, many commit messages among students' projects lack useful information. This is a concern, as low-quality commit messages can negatively impact communication of software development and future maintenance. To address this issue, this research aims to help students write high-quality commit messages by "nudging" them in the right direction. We modified the GitHub Desktop application by incorporating specific requirements for commit messages, specifically "what" and "why" parts. To test whether this affects the quality of commit messages, we divided students from an Information Retrieval class into two groups, with one group using the modified application and the other using other interfaces. The results show that the quality of commit messages is improved in terms of informativeness, clearness, and length.

cs.SE↗