DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2026.22

Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages

Authors: Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract

Developers routinely use GenAI tools (large language models enriched in various ways) to generate useful components of programs, such as regular expressions. While pleasant and often effective, this can easily lead to subtle bugs. The developer may have been unclear in their specification, they may not fully understand the language of the output, there may be systematic misconceptions suffered by the user and perhaps even embedded in the language model, and so on. Responsible use of GenAI requires humans in the loop. To be effective, the human interaction must be both meaningful and moderate. We accomplish this as follows. First, we generate multiple candidate expressions instead of one. We then use formal language containment properties to generate distinguishing concrete scenarios that illustrate the differences between the candidates. We then have users rate these concrete scenarios. This process converges in a few steps, while also giving the user insight into any lack of clarity on their part. We have built a tool, pick, that implements this iterative process. We apply it to three formal languages with the necessary properties: regexes, linear temporal logic, and access-control policies. We show through experiments that pick is a significant improvement over showing users the candidate expressions, and also helps catch situations where no output is a match.

Cite as

Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi. Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 22:1-22:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{prasad_et_al:LIPIcs.ECOOP.2026.22,
  author =	{Prasad, Siddhartha and Austen, Skyler and Fisler, Kathi and Krishnamurthi, Shriram},
  title =	{{Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{22:1--22:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.22},
  URN =		{urn:nbn:de:0030-drops-261181},
  doi =		{10.4230/LIPIcs.ECOOP.2026.22},
  annote =	{Keywords: Regex, LTL, Access Control, Generative AI, Human-in-the-Loop}
}

Document

Artifact

DOI: 10.4230/DARTS.12.1.7

Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact)

Authors: Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract

This artifact accompanies the paper Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages. It provides (1) the pick VS Code extension for regex synthesis with human-in-the-loop validation, and (2) anonymized user-study data and Docker images that reproduce the study interfaces and statistical analyses reported in the paper.

Cite as

Siddhartha Prasad, Skyler Austen, Kathi Fisler, and Shriram Krishnamurthi. Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 7:1-7:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{prasad_et_al:DARTS.12.1.7,
  author =	{Prasad, Siddhartha and Austen, Skyler and Fisler, Kathi and Krishnamurthi, Shriram},
  title =	{{Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact)}},
  pages =	{7:1--7:9},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Prasad, Siddhartha and Austen, Skyler and Fisler, Kathi and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.7},
  URN =		{urn:nbn:de:0030-drops-261445},
  doi =		{10.4230/DARTS.12.1.7},
  annote =	{Keywords: Regex, LTL, Access Control, Generative AI, Human-in-the-Loop}
}

Search Results

Documents authored by Austen, Skyler

Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages

Abstract

Cite as

Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message