一句话：提出基于多选查询的主动学习范式，通过合成 Hoare 三元组选项实现高效的程序消歧。
高层代码规约天然具有歧义，现有交互式消歧方法多依赖用户提供带标签的示例，这种方式容易出错且未必能准确反映用户意图。本文提出一种新的主动学习范式：系统向用户呈现一小组高层行为作为多选选项，用户只需选出符合意图的一项。其关键技术洞察在于，每个选项对应一个刻画语义相似候选程序簇的 Hoare 三元组，从而使查询的信息量与可解释性可以被形式化推理，并支持最优查询的系统化构造。作者据此设计了新的主动学习算法并实现工具 Socrates，能自动合成信息量大的多选查询。在涵盖符号与神经符号设置的四个领域上的评估表明，Socrates 生成的查询直观易答、收敛高效，且比现有方法更可靠地识别出用户想要的程序，同时运行时间具有竞争力。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2604-08792,
title = {Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation},
author = {Celeste Barnaby and Danny Ding and Osbert Bastani and Işıl Dillig},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808279}
}