Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation

TL;DR

This paper presents Socrates, an active learning system that uses multiple-choice queries to disambiguate high-level code specifications, improving reliability and efficiency over existing methods.

Contribution

It introduces a formalized multiple-choice query paradigm and an active learning algorithm for program disambiguation, implemented in the Socrates tool.

Findings

Socrates generates intuitive, easy-to-answer queries.

Socrates achieves more reliable program identification.

The system demonstrates efficient convergence across diverse domains.

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.