Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation
2026-04-09 • Programming Languages
Programming Languages
AI summaryⓘ
The authors address the problem of unclear high-level code instructions by creating a new way to ask users simple multiple-choice questions to clarify their intent. Instead of relying on example-based feedback, their system, Socrates, presents clear behavior options that represent groups of possible programs. This approach helps the system figure out the best questions to ask and quickly narrows down the correct program. Tests show that Socrates asks easy questions and finds the intended code more reliably and efficiently than previous methods.
active learningprogram disambiguationmultiple-choice queriesHoare tripleprogram synthesissymbolic reasoningneurosymbolicquery optimizationuser intent clarification
Authors
Celeste Barnaby, Danny Ding, Osbert Bastani, Isil Dillig
Abstract
High-level specifications of code are inherently ambiguous, and prior systems have explored interactive techniques to help users clarify their intent and resolve such ambiguities. However, most existing approaches elicit supervision through labeled examples, which are often error-prone and may fail to capture user intent. This paper introduces a new active learning paradigm for program disambiguation based on multiple-choice queries. In this paradigm, the system presents a small set of high-level behaviors as multiple-choice options, and the user simply selects the intended one. Technically, each answer option corresponds to a Hoare triple that characterizes a cluster of semantically similar candidate programs. This formulation enables formal reasoning about the informativeness and interpretability of queries, and supports systematic construction of optimal queries. Building on this insight, we develop a new active learning algorithm and implement it in a tool called Socrates, which automatically synthesizes informative multiple-choice queries for program disambiguation. We evaluate Socrates across four domains spanning both symbolic and neurosymbolic settings and show that it produces intuitive, easy-to-answer queries and achieves efficient convergence. Most importantly, Socrates identifies the intended program more reliably than existing methods, while maintaining competitive runtime performance.