“What should my system do?”

Programmers increasingly rely on GenAI to translate informal requirements into logical formulae, security policies, and other formal specifications. This is convenient but risky: natural language is ambiguous, relevant domain knowledge is often unstated, and repeated prompts can yield different plausible outputs. PICK is a system for building confidence in these generated specifications by taking advantage of that variability. Rather than ask a model for a single answer, it collects several candidates and guides the programmer through an interactive process to determine which, if any, captures their intended behavior. For that interaction to be worthwhile, it must ask programmers questions they can understand, and it must not ask too many of them.

PICK’s design rests on two observations. First, many of these specification languages are closed under negation and intersection, or have good heuristics for approximating these operations. This lets PICK compute the semantic differences between candidates and sample from them, so every scenario it shows is one on which plausible interpretations actually disagree. The questions stay few, and each one is decisive. Second, cognitive science shows that people reason more effectively about concrete instances than about abstract rules. So instead of comparing abstract formulae, programmers upvote and downvote these concrete scenarios. It is easier to decide whether a string should be accepted by your parser than to compare two complex grammars.

Across studies on regular expressions and access-control policies, PICK users identified the correct candidate, or recognized that none was correct, more accurately than those choosing among candidates directly. Even more strikingly, novices using PICK for Linear Temporal Logic performed as well as experts not using the tool.