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

Consider a roboticist who needs to turn an English description into an LTL formula, an administrator who has to turn one into an access-control policy, or a developer who needs to generate a regex. These are all tasks for which they might turn to Gen(erative)AI. Suppose they ask for a regex to check whether a dd-mm-yyyy string represents a valid date. They might get a response like:¹¹1These were generated by GPT-5 on 2025-09-15 via ChatGPT.com.

along with a warning that this checks only structure but not whether specific day-month-year combinations are valid. Following up to request a regex that includes date validity produces:

Given the complexity of the generated regex, the developer is unlikely to be able to inspect it for correctness. Even if they did, they might hold misconceptions about how regexes [45, 55, 59] (or likewise for other notations like LTL [11, 23, 26]) work; these same misconceptions may also be embedded in a language model used by the GenAI. They could write tests, but will they be comprehensive? And will they catch the edge cases needed to validate a complex output they do not entirely understand?

This might just seem like a matter of “LLM quality”. However, even given a “perfect” LLM, there are many situations that call for human judgment. Suppose, for instance, we are generating a regex to categorize countries of “North America”. Exactly which countries are in and out? What about the Caribbean? How about Caribbean countries below the Equator? The exact list of the world’s countries is a fraught political matter. The list of honorific titles varies heavily by country. These are not a matter of “correctness”: these questions have no canonical answers. Generating formal outputs from prose must contend with not only ambiguous prose but also intent, regional variation, contested world knowledge, and more.

Thus, while GenAIs are powerful aids for developing formal statements and several tools use them [10, 12, 18, 19, 39, 44, 50, 61, 79, 80, 83], we must use them responsibly, taking into account the above weaknesses and ambiguities. While numerous people have sounded the alarm about over-reliance, virtually none of the tools we have cited engage with humans in any meaningful way, often using GenAI to check the output – which is of no use in case of an erroneous specification, systematic misconception, etc. (Section 6 discusses this in more detail.) Safety, privacy, personal and political sensitivity, and so on all demand caution.

We instead take the philosophical position that, instead of just piling GenAI on top of GenAI, humans must be in the loop. However, the demands of humans must necessarily be:

Meaningful

Asking humans to pass judgment on complex and abstract statements, such as those shown earlier, is unlikely to be effective. Laziness, automation bias, inability to form good judgments, and a desire to get things done will all lead to meaningless confirmation, just as we have seen for security and medical alerts [43, 70, 72].

Moderate

Asking lots of questions, no matter how simple, can be exhausting and will also lead to errors as the number of questions grows. We should try to make every human action be highly impactful and not ask users to perform too many actions.

We embody this stance in a tool-supported workflow, shown in Figure 1 (Section 2 provides details), called pick (short for Pairwise Iterative-Choice Knockout). It uses concrete examples to guide a user in choosing between plausible formalized versions of a prompt:

1. 1.

   A user provides a textual description of the desired formal expression (e.g., a regex). pick supports any formal language that is closed under negation and intersection, for which checking equality is decidable, and that supports tractable generation of instances.

2. 2.

   pick creates not one but a family of candidate formal expressions.

3. 3.

   Driven by ideas from cognitive science (Section 6), instead of asking users to wrestle with these abstract formal expressions, pick presents the user with a series of concrete scenarios (e.g., strings for regexes, traces for LTL, requests for access-control policies) that have been carefully chosen to distinguish among the candidates. The user is asked to indicate which scenarios they would accept and reject. As they classify concrete scenarios, they are actually implicitly classifying the underlying candidates. This process iterates until they have one or no candidate expressions left.

If in the end there is one candidate expression, then this is the best match with their intent. If there are no candidates left, that means either none of the expressions is a fit, or the user is not even consistent about their wishes. In either case, it would have been dangerous to take the single candidate produced by GenAI; instead, pick forces them to clarify a poor GenAI input or, more fundamentally, an inconsistency in their own thinking.

We have applied pick to three formal languages: regexes, access-control policies, and LTL. This paper addresses two research questions:

RQ1

To what extent does pick’s concrete-example–based workflow help users validate synthesized formal artifacts against their intended meaning, both alone and in contrast to direct inspection of candidate artifacts?

RQ2

What technical decisions support leveraging concrete examples and closure properties to identify correct formal artifacts from informal intent?

Sections 2 and 3 address RQ2 by presenting the design, algorithmic, and pragmatic choices underlying pick. Section 4 addresses RQ1 through controlled user studies evaluating pick across the three domains. In brief, our studies find that pick significantly improves user accuracy across regexes and access-control policies, and enables novices to match domain-trained participants on LTL. Together, these results provide strong support that the pick approach is well worthy of further consideration and use.

While we summarize the workflow here, Figure 2 explains the tool via a concrete example.

The user provides a textual description of the desired regex, which is sent to a GenAI model. As we discuss in Section 2.1, this yields a family of candidate expressions. pick presents the user with pairs of scenarios (here, words) and asks them to classify each one: upvoting classifies the scenario as matching the intended pattern, while downvoting classifies it as violating the pattern. As scenarios are classified, candidates are either supported or eliminated, as we discuss in Section 2.2. This informs the generation of further scenarios.

Users can decide whether to see the candidate expressions from which they are actually selecting. In Figure 2, those outlined in blue remain in contention; those outlined in orange have been eliminated. Some of our studies showed the candidates while others did not; we discuss this in more detail in Section 4. pick is driven by these candidates under the hood whether or not it shows them to the user.

pick is functioning software. We have implemented it for all three languages – with essentially the same interface – to conduct user studies. We have deployed the regex version as production software as a Visual Studio Code (VSC) extension that can be easily installed from the VSC Marketplace.²²2https://marketplace.visualstudio.com/items?itemName=SiddharthaPrasad.pick-regex pick leverages VSC APIs for accessing GenAI models.

pick, as presented in Section 2, embodies many design decisions, some of which are not evident from the screenshot. They speak to RQ2: the technical choices that arise when using concrete examples and closure properties for intent validation. We discuss these below.
$▶$ How many candidate expressions should pick create?
A good default seems to be about four. This creates enough variety to provide real choices, as Section 4 shows. A good number, however, really depends on how many plausible alternatives we can create. As we mention in Section 2.1, we can use semantic mutants to create several expressions based on known misconceptions that people have.

Every extra candidate beyond a point would seem to worsen the user experience; eventually users will get bored or overwhelmed. On the other hand, it is also important to consider every reasonable candidate. Since the reasonable candidates should be related, and votes impact all candidates, the total amount of work may be tractable. We return to this issue, with some evidence, in Section 7.2.
$▶$  How much support (in terms of numbers of classified scenarios) do we want before eliminating an expression or confirming a final selection?
As Section 2 mentions, we reject a candidate after two Downvotes, and require at least one Upvote for it to be selected. We chose these numbers based on two considerations:

1. 1.

   We wanted to avoid one-off accidental selections from distorting the outcome too much. At the same time, we wanted the total number of steps to be tractable.

2. 2.

   We ran several preliminary rounds of prototype user studies with regexes (Section 4.2.2) and carefully examined the decisions made by users relative to outcomes, and also read their justifications for their choices. While early rounds used a Downvote threshold of one, we observed that large percentages of participants were eliminating all of the candidates across both the With List and Without List conditions. When we changed the Downvote threshold to two, these percentages dropped noticeably (an average of 27% across all problems in both conditions; with a min of 4% and a max of 52%). We thus used two as the threshold for the remaining studies.

However, there is nothing especially canonical about these numbers beyond the basic principle of robustness to imperfect user responses over absolute minimalism. A user with a vested interest in the output may spend more time on each classification than our experimental participants, may better recognize subtle distinctions, or may desire higher assurance; accordingly, pick allows these thresholds to be adjusted.

At the same time, the appropriate thresholds are also constrained by the semantics of the candidate space itself: when candidates overlap heavily, the amount of distinguishing evidence that can be obtained is inherently limited. For example, the regexes a* and a+ differ only on the empty string. A fixed elimination threshold of two Downvotes would therefore yield a non-terminating decision process. As a result, when the number of distinguishing scenarios is less than the elimination threshold, pick adjusts the threshold to the number of distinguishing scenarios between candidates.
$▶$ Should we show the user the candidate formulae in addition to the scenarios?
There are good arguments both for and against showing the candidate expressions in addition to the scenarios. For a user who is comfortable reading the candidates, working through the scenarios could feel tedious. Furthermore, an experienced user might calibrate the scenarios against the candidates, leading to more confidence in the final recommendation.

On the other hand, the candidates could distract a user from actually working with the examples. If the user does hold misconceptions about the language, seeing the candidates might reinforce those misconceptions and bias classification of the scenarios. In addition, while the candidates for languages like regexes and LTL tend to not be too large, for access-control policies they can be extremely large and hence simply would not fit on a screen.

The production version of pick lets the user choose. From a research perspective, the question is whether showing or not showing the candidates affects the quality of the decisions. We therefore put this question to the test experimentally as part of our user studies (Sections 4.2.2 and 4.3.2), and found it made no difference.
$▶$  What happens if a user runs out of candidates, or doesn’t like the examples they’re seeing?
In such a situation, the user needs to revise the prompt. In principle, they can just start over with a revised version. However, doing so would throw away all the classification work they have already done. Therefore, pick instead provides a notion of revising the statement (① in Figure 2). At a basic level, it provides the current prompt in editable form. Much more importantly, it retains all prior classifications and automatically re-applies them to each of the newly generated candidates. In practice, we have found this immensely valuable when refining prompts; without it, the tool can sometimes feel extremely frustrating. This is also a form of robustness: rather than forcing a selection from a bad candidate set, pick tolerates the zero-candidate outcome (illustrated by the Dates question in Section 4.2.2).
$▶$ What happens to semantically equivalent candidates?
pick clusters candidates by semantic equivalence. In principle, for the purpose of generating scenarios, it can throw away all but one per cluster. However, the different syntactic forms may be perceived differently by the user. They may prefer one over another because it’s shorter, clearer, has better redundancy, etc. That is: syntax matters! Therefore, pick keeps all the clustered formulae. At any point (especially when a cluster emerges as the winner), the user can look at all cluster members and decide which best meets their needs.
$▶$ What about additional information provided by GenAI systems?
Modern GenAI systems will often not only generate candidates but will also provide descriptive text about them: both a textual description of what the candidate is capturing, as well as a confidence score. While these are not necessarily reliable, they may be useful. Therefore, pick retains this information, which can be viewed at any time.

In some cases, this auxiliary information takes the form of warnings. Because GenAI systems are trained across a wide range of programming tasks and formalisms, they can sometimes recognize when a task exceeds a given language’s expressive power. For example, they may note that regular expressions cannot capture context-free patterns such as parsing HTML. When this occurs, pick passes the warning on to the user.
$▶$ Can we make richer use of scenarios?
So far, scenarios are disconnected from the GenAI, which only produces candidates. When refining a prompt, however, pick sends back the classifications the user has performed so far to the GenAI system. This additional guidance has the potential to improve the quality of subsequently generated candidates.

Of course, there is no guarantee the GenAI will accurately take these scenarios into account; however, as noted above, pick immediately repeats the classification of new candidates, so any failures in this regard will be caught. pick for regexes also provides a text box where users can write sample scenarios to accompany even the initial prompt.

pick also uses other ways to obtain better scenarios. One is to ask the GenAI to also provide some interesting scenarios, which are added to the ones generated mechanically. The other is to allow users to edit the scenarios it is showing. Sometimes, seeing a machine-generated scenario inspires the user to amend it slightly to make it much more interesting. These are then also used during prompt revision, etc.
$▶$ How do we balance information gain against responsiveness when generating scenarios?
Because scenarios are drawn from the disagreement region between currently live candidates, every scenario is informative by construction: each classification necessarily rules on at least one live candidate. In practice, however, there is a tension between finding ideal distinguishing examples and maintaining a productive interaction. Generating a theoretically optimal scenario can sometimes be computationally expensive, and waiting for such scenarios risks breaking the interactive flow of the tool.

This tradeoff is further justified by the structure of the candidate space itself. Heavy semantic overlap or containment among candidates can reduce the practical value of even theoretically distinguishing scenarios: a “good” example may simultaneously confirm many undesirable candidates. In such cases, perfect separation is less important than sustaining an interaction in which each classification contributes to clarifying the user’s intent.

Accordingly, pick favors timely progress over perfect coverage of the live candidate set. Informed by interaction design principles [53], scenario generation is capped at about one second in practice; beyond that point, the system prioritizes making forward progress over continuing to search for an optimal partition.
$▶$ Why have an Unsure option?
The Unsure option supports non-blocking exploration of the candidate space. Rather than requiring an immediate classification, pick allows users to move past an example when they are uncertain, continue exploring other classifications, and return to it later if desired. Selecting Unsure marks the example as seen but does not affect candidate votes. As observed in our studies (Section 4), participants did make use of this option in practice.
$▶$ How can pick make differences between similar scenarios salient?
pick includes a diff mode (accessible via the gear icon beside ② in Figure 2) that highlights differences between scenario pairs. This is particularly useful when distinguishing scenarios that differ by only a small number of characters.

We have described pick and its many components. However, we have not demonstrated that the pick idea is actually useful. We therefore conducted controlled studies to address RQ1: to what extent does pick’s workflow help users validate synthesized formal artifacts? The most natural question is whether pick is actually effective. A particularly interesting special case is whether it helps in situations where the GenAI does not produce any correct answers. In addition, an important user interface element to examine is the impact of showing the candidate expressions, as discussed in Section 2.

We ran user studies with three formal languages: regexes, linear temporal logic [60] (LTL), and attribute-based access control [34, 29] (ABAC). We chose them because they not only enjoy the formal language properties we want, but also offer interesting contrasts:

• $\mathrm{■}$

  Regexes are widely used and can easily become quite complicated, even for seemingly simple patterns (as we showed in Section 1). The literature [45, 55, 59] also shows their potential to confuse.

• $\mathrm{■}$

  LTL formulae are used in settings as diverse as program analysis, verification, planning, and robotics. They have subtle semantics, as prior studies have established even with experienced LTL users [23, 26]. Using these results to generate candidate formulae provides a form of validity to our work. Furthermore, we can benchmark the performance of our users against those encountered in those studies.

• $\mathrm{■}$

  Access-control policies are interesting because their formal statements tend to be longer and more complex than for regexes or LTL. Whereas regexes and LTL entail reasoning about sequences or traces with limited information at each point, access control requires reasoning about multi-faceted relationships and attributes about entities, resources, and permissions. There is a risk that these aspects can challenge pick.

We summarize what we learned in Section 4.5. Links to the online versions of the three studies are provided in Supplement Section 1.

We now discuss threats to two kinds of validity: both of the findings of this paper and, more importantly, the ability for pick to be used in production.

Our study was conducted via crowdsourcing, which raises standard concerns about participant motivation, expertise, and engagement. We mitigated these risks by running test rounds to calibrate compensation (Section 4.1), using both Prolific and additional screening mechanisms, and collecting post-study familiarity surveys. These surveys indicate that many participants had relevant domain knowledge; several responses used technical terminology (e.g., references to Apache access files in the ABAC study). In both test and final rounds, we used completion times and written answers as signals of meaningful engagement.

For instance, we cannot rule out that participants may have used LLMs to assist their performance on the tasks. However, we ameliorated these concerns in two ways. The engagement signals just described (completion times and written responses) help flag participants who may have been outsourcing the task; during testing of the ABAC Control condition, for example, unusually short completion times suggested copying, and we addressed this by embedding policies as images. For the same reason, we presented LTL traces as images. Even if participants had leaned on LLMs, however, the error rates reported in Tables 2 and 4 would reinforce rather than undermine the motivation for pick.

Next, there is the threat from the size and variety of problems we gave. In the LTL case (Section 4.4), we were able to rely on a validated multi-year body of work. For regexes and ABAC, we chose what we hoped would be a usefully representative set of examples. In the ABAC case, however, these are only “textbook” examples; real policies are often significantly larger [57, 66]. However, we think this only benefits pick: if a policy is hundreds of lines long, nobody is going to meaningfully look through several alternatives – even armed with a syntactic differencer – and make meaningful judgments. They are likely to want to resort to semantic differencing tools anyway (Section 6). However, even a generic semantic differencing tool might not zero in on instances designed for multi-way classification, so the user would have to manually perform what pick does automatically.

That said, one significant threat in our Control and With List conditions is that the candidate expressions are presented as generic text. A user may well have sophisticated tools for navigating these. These tools may even help negotiate the large sizes of ABAC policies. Given such tools, the performances may improve. However, this is not inherently a problem: a user who has access to these tools and still wants to use pick clearly finds benefit to our workflow, and if they can use it in conjunction with other tools to make better and faster decisions, we should rejoice!

Because we rely on decision procedures to generate scenarios, the time it takes to generate one could be problematic. In our studies, both regex and LTL generated new scenarios almost instantaneously, but ABAC uses a rough prototype that takes a few seconds. We did not expect crowdsourced participants to have the patience to wait that long, so we precomputed the scenarios. This would not be possible in a deployed system (and this precomputation inflates the pleasantness of the experience of the With List and Without List conditions). However, in this specific case, we were not engineering for speed, but rather used a system we were comfortable with; there may be other much more efficient systems. In general, however, we believe that a user who finds value in pick would not mind waiting a few seconds for new scenarios. In particular since it takes several seconds to form a judgment, a production tool can just compute the next pairs while the user is judging, thereby eliminating the perception of this lag in most cases.

In this paper, we have tried to bring together three different ideas. We start with the utility but insufficiency of GenAI, and want to put humans back in the loop. To do so, we draw from the cognitive science literature on what they can most meaningfully do. To implement these ideas, we draw on formal language theory with a generic algorithmic framework that applies to a large family of in-use languages. Through a series of experiments across a broad range of domains – regexes, LTL, and ABAC – we show that there is real value in the pick framework. We believe that the net result is a framework for the responsible use of GenAI, leveraging its strengths while using humans in targeted ways to compensate for its weaknesses.