程序综合简介

自动化软件开发的梦想从计算机时代的早期就已经存在。早在 1945 年，作为他对自动计算引擎愿景的一部分，艾伦图灵就认为指令表必须由具有计算经验和一定的解谜能力的数学家组成......构建指令表的过程应该是非常迷人。它不需要成为苦力的真正危险，因为任何非常机械的过程都可能转交给机器本身。 copland2012alan 传统上，自动化被纳入软件开发的方式是通过使用编译器和高级语言。当第一个 FORTRAN 编译器被开发出来时，它被吹捧为“FORTRAN 自动编码系统”，它的目标无非是让 IBM 704 为自己编码问题并产生与人类编码器一样好的程序（但没有错误）巴科斯： 1957 年。编译和综合就其目标而言非常密切相关，它们都旨在支持从对其行为的高级描述中生成软件。但是，一般来说，我们期望合成器不仅仅像传统编译器那样将程序从一种表示法转换为另一种表示法；我们期望它发现如何执行所需的任务。这条线可能很模糊，因为一些激进的优化编译器可能会被争论为实际发现如何执行在高级抽象中指定的计算（并行编译器是一个很好的例子）。编译器和合成器之间的一个区别特征是搜索元素。在编译器中，根据预定义的时间表应用转换规则，将计算的输入描述转换为程序。相比之下，合成器通常被理解为涉及对满足规定要求的程序的搜索。同样，这条线是模糊的，因为一些现代研究编译器积极搜索转换空间，以在称为自动调整的过程中找到最佳实现。与综合密切相关的另一类技术是声明式编程，尤其是逻辑编程。逻辑编程的梦想是程序员能够以逻辑形式表达他们的计算需求，当给定输入时，运行时系统将通过搜索和推导的组合得出满足逻辑约束的输出。所以目标也与程序综合密切相关，但有一些重要的区别。首先，逻辑编程系统不是试图找到解决特定问题的算法，而是依赖通用算法来搜索每个问题的解决方案。 Thins 意味着对于许多问题，它们可能比解决特定任务的专门程序慢得多。此外，如果问题未详细说明，用户可能会在运行时得到与程序预期的解决方案相去甚远的解决方案。最后，机器学习对应于与程序合成密切相关的第三类方法。机器学习中的典型问题是找到一个行为与给定数据集非常匹配的函数。所以机器学习问题可以被认为是程序综合问题的一个特例，其中规范以数据的形式出现。程序合成和机器学习的最大区别在于，在机器学习中，算法考虑的函数空间是非常严格的。例如，线性分类器、决策树和神经网络是已经被很好研究的函数类的一些例子，这些类中的每一个都有自己的专门的算法集，用于推导与数据集匹配的函数。相比之下，在程序综合中，我们对可以与更通用的程序类一起工作的通用算法感兴趣，对支持递归或其他形式迭代的程序特别感兴趣。传统上，程序综合的第二个重要区别在于，通常希望发现与规范精确匹配的程序，而在机器学习中，从噪声数据中学习的概念在所有算法中都根深蒂固。这种区别在今天不太重要，因为人们对对噪声具有鲁棒性或在存在不完整规范时表现良好的算法的综合共性有浓厚的兴趣。因此，如果程序综合不是编译，不是逻辑编程，也不是机器学习，那么什么是程序综合？ 如前所述，社区中不同的人对他们所描述的程序综合有不同的工作定义，但是我相信下面的定义既包含了今天我们所理解的程序综合的大部分内容，也排除了上述一些类别的方法。程序综合对应于能够从为生成的代码建立语义和句法要求的工件集合生成程序的一类技术。这个定义有两个重要的元素。第一个是强调程序的生成；我们期望合成器生成解决我们问题的代码，而不是像逻辑编程系统那样依赖运行时的广泛搜索来为特定输入找到解决方案。二是强调支持语义和句法要求的规范。我们期望综合算法为我们提供对将要考虑的程序空间的一些控制，而不仅仅是它们的预期行为。需要强调的是，单个合成系统本身可能无法提供这种灵活性；事实上，迄今为止合成的最大成功是在专业领域，在这些领域中，对程序空间的限制已经“融入”到合成系统中。尽管如此，即使没有向用户展示灵活性，底层综合算法在如何定义程序空间方面确实具有很大的灵活性，这在编译和机器学习方面都是一个很大的区别。一般来说，这两个要求都意味着我们的综合程序将依赖于某种形式的搜索，尽管综合的成功在很大程度上取决于我们是否有能力避免对即使是相对简单的综合而出现的指数级大程序空间进行彻底搜索问题。 Lecture1:Slide14;Lecture1:Slide15这些天，程序合成是一个活跃的研究领域，研究论文每年都会在所有主要的编程系统会议（PLDI、POPL、OOPSLA）以及形式方法（CAV、TACAS）和机器学习（NeurIPS、ICLR、ICML）。综合研究的一个重要分支是在我们从非常高级的工件中自动生成非平凡算法的能力方面推动包络。今天，我们能够合成有趣的算法，例如 Karatsuba 大整数乘法草图、Strassen 的矩阵乘法 Srivastava:2010，或者 Barron 和 C. Strachey 的函数笛卡尔积算法，这被认为是第一个函数珍珠 Feser:2015。当涉及到从形式规范合成程序时，我们现在能够合成相当复杂算法的可证明正确的实现；几年后，我们已经能够从排序和列表反转等操作转向算法和数据结构操作，例如插入红黑树或二叉堆 Polikarpova:2016。另一个合成相当先进的领域是位向量操作的合成。最近一次合成比赛的获胜者能够合成组织者投入的每一个位向量操作。合成研究的另一个重要分支集中在合成技术在广泛类别问题中的应用。例如，程序合成特别成功的一个领域是“Data Wrangling”，即对数据的操作，尤其是没有编程经验的人。程序合成的第一个商业应用是 FlashFill gulwani:2011:flashfill ，该功能首次集成到 Excell 2013 中，允许用户通过提供几个示例进行数据操作，并自动从示例中导出一个小程序并将该程序应用于您的其余数据。从示例 Wang:2017 或自然语言查询 Yaghmazadeh:2017 中合成相当复杂的数据库查询的能力的进步。这一领域已被证明非常适合我们目前的合成能力，因为一方面，有一个强大的需要让非程序员也可以进行数据分析和清理，另一方面，所讨论的程序通常很小且易于描述通过例子或其他形式的自然互动来表达。 Lecture1:Slide27;Lecture1:Slide28;Lecture1:Slide29;Lecture1:Slide33;另一个引起人们关注的领域是代码的逆向工程。传统上，我们认为综合是从规范开始，然后从中生成实现。但在这种情况下，该范式被颠覆了：从一个实现开始，目标是推断一个描述给定实现行为特征的规范。这个想法首先由 Susmit Jha、Sumit Gulwani、Sanjit Seshia 和 Ashish Tiwari Jha 提出：2010。它最近被 Alvin Cheung 以一种称为验证提升的方法推广，其目标是发现一个高级表示可证明等效于一个实现，可用于生成更高效的代码版本。这个想法首先应用于生成相当于一段命令式代码的 SQL 查询的问题，但最近被应用于各种问题，从现代化遗留 HPC 应用程序 Kamil:2016 到优化 Map Reduce 程序 Ahmad:2018。另一个最近使用综合进行逆向工程的例子涉及创建复杂代码模型以进行程序分析。例如，Jinseong Jeon 等人最近发表的一篇论文。 Jeon:2016 表明，通过记录框架和测试应用程序之间交互的跟踪，然后强制合成器生成符合该跟踪和遵循已知的设计模式。在 JavaScript Heule:2015 中，Heule、Sridharan 和 Chandrato 使用了类似的想法合成数组操作例程的模型。 Lecture1:Slide41;Lecture1:Slide43;Lecture1:Slide44一个特别有趣的研究重点是综合技术在看似与自动编程无关的问题上的应用；人们越来越意识到程序合成技术实际上可以应用于许多传统上被认为是人工智能的领域。例如，早在 2013 年，我们就证明可以将程序综合应用于为编程作业提供反馈的问题 Singh:2013；类似的想法已被用于其他形式的自动辅导，从教授自动机理论 D'antoni:2015 到教学演绎 AhmedGK13。更广泛地说，围绕程序合成的更令人兴奋的研究方向之一是合成与机器学习之间的交互。一方面，最近人们对将机器学习技术应用于综合问题产生了很多兴趣，例如能够学习如何使用复杂的 API MuraliCJ17a。但是，将程序综合中的想法应用于机器学习问题也引起了人们的极大兴趣，例如，为了让您使用更少的数据进行学习或生成可解释的模型。例如，在最近的工作中，我们表明可以从少量示例中学习语言形态规则，或者比传统的机器学习 EllisST15 更有效地学习视觉概念。一般来说，在使用程序综合时必须解决三个主要挑战。在最近的一篇论文中，我们将这些称为机器编程的三大支柱 GottschlichSTCR18。意图。第一个挑战是我们所说的意图挑战：用户如何告诉你他们的目标？综合的定义涉及语义和句法约束，但这些的确切形式将影响关于综合系统的所有后续决策。 FlashFill gulwani:2011:flashfill 系统的成功普及了使用输入-输出示例作为规范手段，但输入-输出示例并不适合每项任务。在我们自己的故事板编程工作中，我们提倡采用多模态合成的方法，将具体示例与抽象示例和逻辑规范相结合，以便它们共同提供有关预期行为的足够信息，以生成数据的有效实现-结构操作 SinghS12。意图挑战的一大方面是如何应对规格不足的问题。如果有多个程序满足要求，我们如何判断用户真正想要的是哪一个？当然，一种解决方案是简单地忽略这个问题，如果用户提供了部分规范，如果他们得到的程序与他们想要的程序不同，他们无权抱怨。然而，在实践中，做出一个好的选择可以区分一个有用的系统和一个没有用的系统。发明。一旦我们知道用户想要什么，第二个挑战就是实际发现一段代码来满足这些需求。可以说这是综合的核心挑战，因为它可能涉及为问题发明新的算法解决方案。我们将在本课程中处理的关键问题之一是社区为解决此任务固有的复杂性而开发的不同技术。适应性综合的规范观点是，用户正在从头开始创建一个全新的算法，并希望利用合成器来创建所需算法的正确实现。然而，大多数软件开发涉及在现有软件系统的上下文中工作、修复错误、优化代码以及执行其他类型的维护任务。该支柱在更广泛的背景下处理综合问题，以及将综合思想应用于新领域软件创建之外的更广泛软件开发任务。正如我们稍后将看到的，有许多引人注目的程序综合应用程序来支持更广泛的软件开发过程。