In program synthesis, an intelligent system takes in a set of user-generated examples and returns a program that is logically consistent with these examples. The usage of Rational Speech Acts (RSA) framework has been successful in building \emph{pragmatic} program synthesizers that return programs which -- in addition to being logically consistent -- account for the fact that a user chooses their examples informatively. However, the computational burden of running the RSA algorithm has restricted the application of pragmatic program synthesis to domains with a small number of possible programs. This work presents a novel method of amortizing the RSA algorithm by leveraging a \emph{global pragmatic ranking} -- a single, total ordering of all the hypotheses. We prove that for a pragmatic synthesizer that uses a single demonstration, our global ranking method exactly replicates RSA's ranked responses. We further empirically show that global rankings effectively approximate the full pragmatic synthesizer in an online, multi-demonstration setting. Experiments on two program synthesis domains using our pragmatic ranking method resulted in orders of magnitudes of speed ups compared to the RSA synthesizer, while outperforming the standard, non-pragmatic synthesizer.

翻译：在程序合成中，智能系统接收一组用户生成的示例，并返回一个与这些示例逻辑一致的程序。理性言语行为（RSA）框架的成功应用，使得构建"实用"的程序合成器成为可能——这些合成器返回的程序除了逻辑一致外，还考虑了用户选择示例时的信息性。然而，运行RSA算法的计算负担限制了实用程序合成在可能程序数量较少的领域中的应用。本文提出一种新颖的实用程序合成摊销方法，通过利用"全局实用排名"——即对所有假设的单一全序关系。我们证明，对于使用单个演示的实用合成器，我们的全局排名方法能够精确复现RSA的排序响应。进一步通过实证表明，在在线多演示场景中，全局排名能够有效近似完整实用合成器的结果。在两种程序合成领域的实验中，与RSA合成器相比，采用我们的实用排名方法实现了数量级的加速，同时优于标准的非实用合成器。