Synthesis in Uclid5
我们描述了一个集成的程序合成到UCLID 5，一个正式的建模和验证工具。据我们所知，Uclid 5的新版本是唯一的工具，支持程序合成有界模型检验，k-归纳，顺序程序验证，和超属性验证。我们使用集成来生成25个程序合成基准，这些基准具有简单的、已知的解决方案，这些解决方案是当前合成引擎无法实现的，我们将基准发布给社区。
2020-07-17 cs.PL
Relational Program Synthesis
本文提出了关系程序合成，一个新的问题，涉及合成一个或多个程序，集体满足关系规范。关系程序合成作为关系程序验证的对偶，是一个重要的问题，具有许多实际应用，如自动程序求逆和比较器的自动生成。然而，这种关系合成问题引入了新的挑战，其非关系的副本，由于组合更大的搜索空间。作为解决这个问题的第一步，本文提出了一种合成技术，结合了反例引导归纳合成框架与一种新的归纳合成算法，是基于关系版本空间学习。我们已经实现了所提出的技术，在一个框架称为Relish，它可以通过提供一个合适的特定于域的语言和相关的关系规范实例化到不同的应用领域。我们使用Relish框架来构建关系合成器，以自动生成字符串编码器/解码器以及比较器，并且我们根据之前的工作和在线论坛中的几个基准来评估我们的工具。我们的实验结果表明，所提出的技术可以解决几乎所有这些基准，它显着优于EUSolver，通用的合成框架，赢得了一般的轨道最近的SyGuS竞争。
2018-09-11 cs.PL
Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation
证明了程序合成和可达性的某些公式是等价的。具体来说，我们的建设性证明显示基于模板的合成问题，它生成一个程序在一个预先指定的形式，和可达性问题，这决定了可达性的程序位置之间的减少。这在两个研究领域之间建立了联系，并允许在它们之间转移技术和成果。为了证明等价性，我们使用可达性工具开发了一个程序修复原型。我们将一个有缺陷的程序和它所需的规格到一个特定的程序，包含一个位置可达只有当原始程序可以修复，然后应用现成的测试输入生成工具上的转换程序，找到测试值，以达到所需的位置。这些测试值对应于原始程序的修复。初步结果表明，我们的方法与其他修复方法相比是有利的。
2019-03-28 cs.PL
Bottom-up Synthesis of Recursive Functional Programs using Angelic Execution
提出了一种新的自自底向上的【形】的函数递归程序综合方法。虽然自自底向上的【形】的合成技术在某些情况下比自顶向下的方法工作得更好，但没有一种技术可以以纯粹的自自底向上的【形】的方式从逻辑规范合成递归程序。主要的挑战是，有效的自自底向上的【形】方法需要执行正在合成的代码的子表达式，但不可能执行尚未完全构造的程序的递归子表达式。在本文中，我们使用天使语义的概念来解决这一挑战。具体来说，我们的方法找到一个程序，满足规范下天使的语义（我们称之为天使合成），分析其天使执行过程中所作的假设，使用这种分析，以加强规范，并最终重新尝试合成与加强规范。我们提出的天使合成算法是基于版本空间学习，因此有效地处理许多增量合成调用整个算法。我们已经实现了这种方法在一个原型称为突发和评估它的合成问题，从以前的工作。我们的实验表明，突发是能够合成的解决方案，94%的基准在我们的基准套件，优于以前的工作。
2021-12-08 cs.PL
Program Synthesis Using Example Propagation
我们提出了Scrybe，一个基于示例的静态类型的函数式程序设计语言的合成工具，它结合了自顶向下的演绎推理风格的$λ^2$与Smyth-style活双向评价。在合成过程中，示例约束通过草图传播，以修剪和引导搜索。这使得Scrybe能够更有效地使用上下文中提供的函数。为了评估我们的工具，它运行在$λ^2$和Myth的组合基准上，这些基准在很大程度上是不相交的。Scrybe能够合成大多数组合基准任务。
2022-10-25 cs.PL
Modular System Synthesis
本文提出利用模块化，由小程序逐层综合大程序，并通过保持各层综合子问题与搜索空间性质相似来提升程序综合的可扩展性。
2023-08-14 cs.PL
Synthesis through Unification
给定一个规格说明和一组候选程序（程序空间），程序合成问题是找到一个满足规格说明的候选程序。我们提出的综合通过统一（STUN）的方法，这是一个扩展的反例引导归纳综合（CEGIS）的方法。在CEGIS中，合成器维护输入的子集S和对于S正确的候选程序Prog。合成器反复检查是否存在反例输入c，从而导致Prog在c上的执行不正确。如果是，合成器将S放大到包括c，并从节目空间中挑选一个对新集合S正确的节目。STUN方法扩展了CEGIS的思想，即给定一个对输入子集正确的程序Prog，合成器可以尝试找到一个对其余输入正确的程序Prog'。如果Prog和Prog'可以统一到程序空间中的一个程序中，那么解决方案已经找到。我们提出了一个通用的综合过程的基础上STUN的方法，并专门为三个不同的域提供适当的统一运营商。我们实现了这些专业化的原型工具，我们表明，我们的工具往往表现形式显着优于标准的基准测试工具的基础上一个纯粹的CEGIS方法。
2015-05-21 cs.PL
Quantitative Synthesis for Concurrent Programs
我们提出了一种算法方法的定量，性能感知的并发程序的合成。输入包括一个不确定的部分程序和一个参数性能模型。不确定性允许程序员忽略在特定程序位置使用哪个（如果有的话）同步构造。指定为加权自动机的性能模型可以通过为锁定、上下文切换以及内存和缓存访问等操作分配不同的成本来捕获系统架构。定量综合问题是自动解决部分程序的不确定性，从而保证正确性和性能最优。作为共享内存并发的标准，正确性被形式化为“规范自由”，特别是竞争自由或死锁自由。对于最坏情况（平均情况下）的性能，我们表明，这个问题可以减少到2玩家的图形游戏（概率转换）与定量目标。虽然我们表明，使用博弈论的方法，合成问题是NEXP完成，我们提出了一种算法方法和实现，有效地为并发程序和性能模型的实际利益。我们实现了一个原型工具，并使用它来合成表现出不同编程模式的有限状态并发程序，用于代表不同体系结构的几个性能模型。
2011-04-21 cs.PL
Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation
针对示例驱动程序综合的庞大搜索空间问题，提出迭代交替的前向与后向抽象解释方法，用于剪枝部分程序并应用于SyGuS，实验表明其显著优于现有方法。
2023-04-21 cs.PL
Interactive Program Synthesis
从不完整的规范（例如输入输出示例）的程序合成已经得到普及，并找到了现实世界的应用，主要是由于其易于使用。由于该技术通常用于交互式环境，因此效率和正确性通常是基于此类技术的系统的关键用户期望。确保效率是具有挑战性的，因为程序合成算法的高度组合性质不适合面向用户的系统的1-2秒响应期望。满足正确性的期望也是困难的，因为提供的规范是不完整的，并且这些系统的用户通常不是程序员。在本文中，我们描述了如何利用交互性来开发高效的合成算法，以及减少认知负担，用户忍受试图确保系统产生所需的程序。我们沿着三个维度建立了一个正式的用户交互模型：增量算法，基于步骤的问题制定和基于反馈的意图细化。然后，我们说明了每一个这些形式的互动合成性能和正确性方面的一组现实世界的案例研究的有效性。
2017-03-10 cs.PL
Program Synthesis from Polymorphic Refinement Types
我们提出了一种方法，用于合成递归函数，证明满足给定的规范的形式的多态细化类型。我们观察到，这样的规范是特别适合于程序合成的原因有两个。首先，他们提供了一个独特的组合的表达能力和可判定性，这使得自动验证-因此合成-非平凡的程序。第二，一个基于类型的规范的程序往往可以有效地分解成独立的规范，其组件，使合成器考虑更少的组件组合，并导致组合的搜索空间的大小减少。在我们的合成过程的核心是一个新的算法，细化类型检查，支持规格分解。我们已经评估了我们的原型实现的一个大的合成问题，发现它超过了最先进的可扩展性和可用性方面。该工具能够合成比以前的工作（几个排序算法和平衡搜索树上的操作），以及现有的合成器处理的大多数基准更复杂的程序，通常从更简洁和直观的用户输入开始。
2016-04-21 cs.PL
Web Question Answering with Neurosymbolic Program Synthesis
本文提出了一种基于程序合成的网页信息抽取技术。给定一个自然语言查询和一些标记的网页，我们的方法合成一个程序，可以用来提取类似类型的信息，从其他未标记的网页。为了处理具有不同结构的网站，我们的方法采用了神经符号DSL，该DSL结合了神经NLP模型以及用于树导航和字符串操作的标准语言结构。我们还提出了一个最佳的合成算法，生成所有的DSL程序，达到最佳的F1分数的训练样本。我们的合成技术是合成的，修剪的搜索空间利用DSL的单调性，并使用转导学习选择具有良好的泛化能力的程序。我们已经在一个名为WebQA的新工具中实现了这些想法，并在多个领域的25个不同任务中对其进行了评估。我们的实验表明，WebQA显着优于现有的工具，如国家的最先进的问答模型和包装归纳系统。
2021-04-14 cs.PL
Program Synthesis using Abstraction Refinement
提出了一种基于反例引导的抽象求精的示例引导程序合成方法。我们的方法使用的抽象语义的底层DSL找到一个程序$P$的抽象行为满足的例子。然而，由于程序$P$可能是虚假的具体语义，我们的方法迭代地细化抽象，直到我们找到一个程序，满足的例子或证明没有这样的DSL程序存在。由于许多程序在其抽象语义方面具有相同的输入-输出行为，因此与使用纯具体语义的现有技术相比，这种合成方法显著地减小了搜索空间。虽然合成使用抽象细化（SYNGAR）可以在不同的设置中实现，我们提出了一个基于细化的合成算法，使用抽象有限树自动机（AFTA）。我们的技术使用一个粗略的初始程序抽象来构建一个初始的AFTA，这是迭代完善，通过构建任何虚假程序的不正确性证明。除了排除以前的AFTA所接受的虚假程序外，不正确性的证明也有助于排除许多其他虚假程序。我们在一个名为\tool的框架中实现了这些想法。我们使用BLAZE框架来构建字符串和矩阵变换的合成器，并将BLAZE与现有技术进行比较。我们对字符串域的研究结果表明，BLAZE与FlashFill（一种现在部署在Microsoft PowerShell中的特定于域的合成器）相比毫不逊色。在矩阵操作的背景下，我们比较BLAZE对散文，一个国家的最先进的通用VSA为基础的合成器，并表明BLAZE结果在一个90倍的速度超过散文。
2017-10-21 cs.PL
Using human-in-the-loop synthesis to author functional reactive programs
响应异步事件的程序编写起来很有挑战性;它们很难推理，测试和调试也很棘手。因为这些程序可能有一个巨大的输入时间和交错空间，程序员可能很容易错过角落的情况。我们建议应用合成，以帮助程序员更容易地创建程序，并在其正确性有更高的信心。我们已经写了一个有效的编码的功能反应式编程（FRP）语义的基础上的功能编程在玫瑰解除列表。我们证明，这种技术是最先进的，首先比较其性能对现有的两个合成工具，产生列表操作程序，然后通过合成一套基准完整的规格。我们还提出了一个交互式工具，在该工具中，程序员以输入/输出示例或不变量的形式提供一些初始部分规范;该工具通过合成两个候选程序来发现规范中的歧义，并给用户一个区分它们的输入;用户更新规范并继续迭代直到找到正确的程序。作为评估，我们展示了使用该工具的一套基准测试，从网络编程和物联网领域，走查一个现实的网络基准测试的样本交互，表明我们可以收敛到目标程序与易处理的互动数量。作为未来的工作，我们讨论对其他FRP语言进行编码，以探索元语言特征、允许合成更大程序的分解策略以及改进的程序员工具（例如GUI），以更容易地得出规范。
2019-09-24 cs.PL
Human-Centric Program Synthesis
程序合成技术在搜索满足高级规范的程序方面提供了重要的新能力。虽然合成已被彻底探讨输入/输出对规范（编程的例子），本文问：什么样的程序合成看起来像超越的例子？日常发展中的哪些实际问题将从综合中获益最大？以人为中心的观点如何为合成的替代规约语言的探索提供信息？我为程序合成勾画了一个以人为中心的愿景，程序员在合成工具的帮助下探索和学习语言和API。
2019-09-26 cs.HC cs.PL
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
本文提出在通用SemGuS框架下，利用语言语义的单调性属性，自动从具体语义获取基于区间的抽象语义以实现自动化剪枝，无需手动设计抽象域，有效提升了程序综合的搜索效率。
2024-08-28 cs.PL
From Provable Correctness to Probabilistic Generation: A Comparative Review of Program Synthesis Paradigms
本文综述程序合成的五大核心范式，分析各方法的原理、系统与应用及关键权衡，梳理从符号到神经符号混合的演进脉络，指明可靠可扩展程序合成的未来方向。
2025-07-21 cs.PL
Semantics-Guided Synthesis
本文提出了一种新的程序合成框架，称为语义引导合成（SemGuS），它允许用户提供语法和语义的语言中的结构。SemGuS接受递归定义的大步语义，这允许它用于指定和解决命令式程序设计语言上的合成问题，该命令式编程语言可能包含具有无限行为的循环。SemGuS的可定制性质还允许在非标准语义（例如抽象语义）上定义合成问题。除了SemGuS框架，我们开发了一种算法，用于解决SemGuS问题，能够合成程序和证明不可实现性，通过编码SemGuS问题作为一个证明搜索约束角子句：特别是，我们的方法是第一个，我们知道，可以证明不可实现性的合成问题，涉及的强制性程序与无界循环，在一个无限的语法搜索空间。我们在一个名为MESSY的工具中实现了该技术，并将其应用于两个SyGuS问题（即，在表达式上）和在命令式程序设计语言上的合成问题。
2020-11-11 cs.PL
FrAngel: Component-Based Synthesis with Control Structures
在基于组件的程序合成中，合成器生成给定组件（函数）库的程序。现有的基于组件的合成器很难合成循环和其他控制结构，并且它们通常需要组件的正式规范，这可能是昂贵的生成。我们提出了FrAngel，一种新的方法，基于组件的合成，可以合成短的Java功能与控制结构时，给定一个所需的签名，一组输入输出的例子，和一个集合的库（没有正式的规范）。FrAngel旨在通过结合两个主要思想来发现具有许多不同行为的程序。首先，它从只通过某些示例的部分成功的程序中挖掘代码片段。由于我们称之为特殊情况相似性的性质，这些提取的片段通常对合成有用。第二，FrAngel使用天使的条件作为占位符的控制结构的条件和乐观地评估所产生的程序草图。天使条件分解合成过程：FrAngel首先找到有希望的部分程序，然后填充它们缺少的条件。我们证明了FrAngel可以在几秒钟内合成各种有趣的程序与控制结构的组合，显着优于现有的最先进的。
2018-11-24 cs.PL
Model Repair Revamped: On the Automated Synthesis of Markov Chains
本文概述了两种方法|基于反例引导的抽象精化（CEGAR）和反例引导的归纳综合（CEGIS），分别应用于有限状态概率模型和程序的自动综合。我们的CEGAR方法迭代分区的设计空间从这个空间的抽象开始，并通过一个轻量级的验证结果分析细化。CEGIS技术利用关键子系统作为反例来修剪所有在该输入上行为不正确的程序。我们展示了这些综合技术的适用性，概率方案的草图，POMDPs的控制器合成，和软件产品线。
2021-05-27 cs.PL
Type-Directed Program Synthesis for RESTful APIs
随着软件即服务和微服务架构的兴起，RESTful API现在在移动和Web应用程序中无处不在。一个服务可能有几十个或几百个API方法，这使得程序员很难找到正确的方法组合来解决他们的任务。我们提出了APIphany，一个基于组件的合成器，用于编写对RESTful API的调用。APIphany背后的主要创新是使用精确的语义类型，既可以指定用户意图，也可以指导搜索。APIphany提供了三种新的机制来克服在REST领域中适应基于组件的合成的挑战：（1）一种类型推断算法，用于使用语义类型来增强REST规范;（2）一种有效的合成技术，用于“处理”半结构化数据，这在使用RESTful API时通常需要;以及（3）一种新形式的模拟执行，以避免在合成期间执行API调用。我们在三个真实世界的API和从GitHub存储库和StackOverflow中提取的32个任务上评估APIphany。在我们的实验中，APIphany找到了29个任务的正确解决方案，其中23个报告了前十名的合成结果。
2022-04-05 cs.PL
Programming-By-Example by Programming-By-Example: Synthesis of Looping Programs
程序合成近年来有了许多新的应用，这在很大程度上要归功于SyGuS的引入。然而，现有的SyGuS求解器都不支持合成递归函数。我们介绍了一个多阶段的算法，在SyGuS中的递归“loolike”程序的合成编程的例子。我们单独解决约束，并将其视为递归程序如何行为的“展开”示例，并求解广义递归解。我们的方法是模块化的，支持任何SyGuS求解器。
2021-08-19 cs.LO cs.PL
Using Program Synthesis for Program Analysis
在本文中，我们确定了一个片段的二阶逻辑与限制量化，是表现力足以捕捉众多的静态分析问题（如安全证明，错误发现，终止和非终止证明，超优化）。我们将该片段称为{ \it合成片段}。合成片段中公式的可满足性在有限域上是可判定的;具体地说，判定问题是NEXPTIME完全的。如果这个片段中的公式是可满足的，则解由从二阶变量到\emph{functions over finite domains}的满足赋值组成。为了具体地找到这些解决方案，我们合成了计算函数的\emph{programs}。我们的程序合成算法对于有限状态程序是完全的，即有限域上的每个\emph{function}都是由我们可以合成的\emph{program}计算的。因此，我们可以使用我们的合成器作为二阶逻辑合成片段的决策过程，这反过来又允许我们使用它作为许多程序分析任务的强大后端。为了显示我们的方法的易处理性，我们评估了几个静态分析问题的程序合成器。
2015-08-31 cs.LO cs.PL
Program Synthesis from Visual Specification
University of Wisconsin-Madison（威斯康星大学麦迪逊分校）
程序合成是自动地将规范翻译成计算机代码的过程。传统的合成设置需要一个正式的，精确的规范。出于计算机教育应用程序的学生学习代码简单的海龟风格的绘图程序，我们研究了一种新的合成设置，只有一个嘈杂的用户意图绘图指定。这使得学生能够绘制他们想要的输出，可选地与他们自己的未完成的程序一起，以自动生成完整的程序。我们制定这个综合问题的搜索空间的程序，与得分的状态之间的Hausdorff距离的程序输出和用户绘图。我们比较了几种搜索算法的语料库组成的真实用户图纸和相应的程序，并证明我们的算法可以合成最佳满足规范的程序。
2018-06-04 cs.AI cs.PL
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended Version
在程序合成中，在简洁和强大的规范之间有一个众所周知的权衡：如果一个规范太冗长，它可能比程序更难写;如果它太弱，合成的程序可能不符合用户的意图。在这项工作中，我们探讨使用注释限制内存访问权限的程序合成，并表明，他们可以使规范更强大，同时保持令人惊讶的简洁。具体来说，我们增强了合成分离逻辑（SSL），一个框架，用于合成堆操作程序，只读借用的逻辑机制。我们观察到，这种简约和保守的SSL扩展在几个方面有利于合成，使其更具（a）表达性（以适度的注释开销实现更强的正确性保证），（b）有效（它产生更简洁和更易于阅读的程序），（c）高效（更快的合成），（d）鲁棒性（合成效率受搜索启发式选择的影响较小）。我们解释的直觉，并提供正式的治疗只读借用。我们证实了索赔（a）-（d）通过描述我们的量化评估的一系列标准的基准规格的各种堆操纵程序的感知合成实现。
2020-01-29 cs.LO cs.PL
Toward Neural-Network-Guided Program Synthesis and Verification
The University of Tokyo（东京大学）；National Institute of Informatics（国立情报学研究所）；SOKENDAI（综合研究大学院大学）；University of Tsukuba（筑波大学）；RIKEN AIP（理化学研究所革新智能统合研究中心）
我们提出了一个新的框架的程序和不变量的合成称为神经网络指导合成。我们首先表明，通过适当的设计和训练神经网络，我们可以从训练好的神经网络的权重和偏差中提取整数上的逻辑公式。基于这一思想，我们实现了一个从正例/反例和蕴涵约束合成公式的工具，并获得了令人满意的实验结果。我们还讨论了我们的合成方法的两个应用。一个是使用我们的工具，限定符发现的框架ICE学习为基础的CHC解决，这反过来又可以应用于程序验证和归纳不变的合成。另一个应用是一个新的程序开发框架，称为基于甲骨文的编程，这是一个神经网络引导的变化Solar-Lezama的程序合成的草图。
2021-08-25 cs.LG cs.PL
Optimal Neural Program Synthesis from Multimodal Specifications
The University of Texas at Austin（德克萨斯大学奥斯汀分校）
多模态程序合成利用不同类型的用户输入来合成所需的程序，是将程序合成扩展到具有挑战性的设置的有吸引力的方式;然而，它需要整合来自用户的噪声信号，如自然语言，对程序的行为有严格的约束。本文提出了一种最佳的神经合成方法，其目标是找到一个程序，满足用户提供的约束，同时也最大限度地提高程序的得分相对于神经模型。具体来说，我们专注于多模态合成任务，其中用户意图表示使用组合的自然语言（NL）和输入输出的例子。我们方法的核心是一个自上而下的递归神经模型，它将分布放置在以NL输入为条件的抽象语法树上。该模型不仅允许有效的搜索空间的语法有效的程序，但它允许我们利用自动化的程序分析技术修剪的搜索空间的基础上不可行的部分程序相对于用户的约束。在多模态合成数据集（StructuredRegex）上的实验结果表明，我们的方法在准确性和效率方面大大优于现有的最先进的技术，并且更频繁地找到模型最优程序。
2021-09-14 cs.CL cs.PL
Genetic Algorithm for Program Synthesis
一种演绎程序合成工具将规范作为输入并导出满足该规范的程序。这种方法的缺点是，这种正确程序的搜索空间往往是巨大的，使得难以在实际超时内导出正确的程序。为了加快这样的程序推导，我们改进了搜索策略的演绎程序合成工具，SuSLik，使用演化计算。我们的交叉验证表明，改进所带来的演化计算概括到不可预见的问题。
2023-01-19 cs.AI cs.NE cs.PL
Relational program synthesis with numerical reasoning
University of Oxford（牛津大学）
程序合成方法努力学习具有数值的程序。一个特别困难的问题是在多个示例中学习连续值，例如区间。为了克服这个限制，我们引入了一个归纳逻辑程序设计方法，它结合了关系学习与数值推理。我们的方法，我们称之为NUMSYNTH，使用可满足性模理论求解器，有效地学习程序的数值。我们的方法可以识别线性算术片段中的数值，如实数差分逻辑，以及无穷域中的数值，如实数或整数。我们在四个不同领域的实验，包括游戏和程序合成，表明我们的方法可以（i）学习程序的数值线性算术推理，（ii）优于现有的方法在预测精度和学习时间。
2022-10-04 cs.LG cs.PL
Recent Advances in Neural Program Synthesis
UC Berkeley（加州大学伯克利分校）
近年来，深度学习在许多以前人工智能无法触及的领域取得了巨大进展。在这些问题上的成功使研究人员开始考虑智能系统解决人类最近才考虑的问题的可能性：程序合成。这一挑战与其他挑战不同，例如对象识别和语音翻译，因为其抽象性和对严格性的要求使得即使是人类也很难尝试。虽然神经程序合成还远未被解决，甚至与大多数现有的方法竞争，但它是一门迅速发展的学科，如果完全实现，它将有很大的希望。在本文中，我们从探索程序合成的问题陈述和挑战开始。然后，我们研究了程序归纳模型的迷人演变，以及它们是如何成功的，失败的和被重新想象的。最后，我们得出结论，对比看程序合成和未来的研究领域的建议。
2018-02-07 cs.AI cs.PL
Informal proceedings of the 32nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2022)
本卷是第32届基于逻辑的程序合成和转换国际研讨会的非正式会议录（LOPSTR 2022），于2022年9月21日至23日举行，作为混合（混合）会议，（在格鲁吉亚第比利斯的Ivane Javakhishvili Tbilisi State University -TSU）和虚拟，并与第24届声明式编程原理与实践国际研讨会（PPDP 2022）共同举办，作为2022年计算逻辑秋季峰会（CLAS 2022）的一部分。
2022-07-29 cs.LO cs.PL
Pre-proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017)
本卷是2017年10月10日至12日在比利时那慕尔举行的第27届基于逻辑的程序合成和转换国际研讨会（LOPSTR 2016）的预录，并与第19届声明式编程原理和实践国际研讨会（PPDP 2017）共同举办。在研讨会讨论后，论文将通过第二轮评审和选择的正式程序。
2017-08-31 cs.LO cs.PL
A Coq-based synthesis of Scala programs which are correct-by-construction
本文介绍了一个新的编译器，允许一个基于Coq的合成的Scala程序是“正确的建设”。一个典型的工作流程的特点是用户实现一个Coq函数程序，证明这个程序的正确性，并利用Scala-of-Coq来合成一个可以无缝集成到现有工业Scala或Java应用程序中的Scala程序。
2017-06-16 cs.LO cs.PL
Scaling Program Synthesis Based Technology Mapping with Equality Saturation
本文提出Churchroad技术映射器，将等价饱和与程序综合工具结合，解决FPGA映射中草图编写困难及SMT求解器乘法处理弱的问题，可处理更大更复杂的设计且无需用户提供草图。
2024-11-19 cs.AR cs.PL
Modelling Program Spaces in Program Synthesis with Constraints
TU Delft（代尔夫特理工大学）
针对程序合成中候选程序空间过大的问题，提出利用语法约束建模程序空间的方法，开发求解器BART，实验显示其最多可削减99%的程序空间，显著缩短枚举时间。
2025-07-10 cs.AI cs.PL
Autoencoders as Tools for Program Synthesis
Eindhoven University of Technology（埃因霍温理工大学）
近年来，源代码语言建模的研究取得了许多进展。应用范围从代码建议和完成到代码摘要。然而，工业级程序设计语言的完全程序合成仍然是一个悬而未决的问题。在这项工作中，我们介绍和实验验证变分自编码器模型的程序合成的工业级程序设计语言。该模型利用了代码固有的树结构，并可与无梯度优化技术（如进化方法）结合使用，以生成最大化给定适应度函数的程序，例如，通过一组测试用例。可在https://tree2tree.app上获得演示
2021-09-05 cs.AI cs.PL
Multi-modal Program Inference: a Marriage of Pre-trainedLanguage Models and Component-based Synthesis
Purdue University（普渡大学）；Microsoft（微软）
多模态程序合成是指根据以不同形式给出的程序规范（代码）（例如自然语言和示例的组合）来合成程序（代码）的任务。示例提供了精确但不完整的规范，而自然语言提供了模糊但更“完整”的任务描述。机器学习的预训练模型（PTM）擅长处理模糊的自然语言，但难以生成语法和语义精确的代码。程序合成技术可以生成正确的代码，甚至经常从不完整但精确的规范，如例子，但他们无法与自然语言的歧义。我们提出了一种方法，结合PTM和基于组件的合成（CBS）：PTM是用来产生候选程序从自然语言描述的任务，然后用来指导CBS过程中找到的程序，匹配精确的基于实例的规格。我们使用我们的组合方法来实例化多模态合成系统的两个编程域：域的正则表达式和域的CSS选择器。我们的评估表明，我们的域不可知的方法相比，一个国家的最先进的专门系统的有效性，我们的方法在提供多模态程序合成从自然语言和例子在不同的编程域的一般性。
2021-09-03 cs.AI cs.PL
Data Migration using Datalog Program Synthesis
本文提出了一种新的技术迁移数据之间的不同模式。我们的方法表示的模式映射作为一个数据库程序，并自动合成一个数据库程序从简单的输入输出的例子来执行数据迁移。这种方法可以在不同类型的模式之间转换数据（例如，关系到图形，文档到关系），并通过利用Datalog的语义有效地执行合成。我们实现了所提出的技术作为一个工具，称为Dynamite，并通过评估Dynamite对28个现实的数据迁移方案显示其有效性。
2020-03-03 cs.DB cs.PL
Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)
本卷是2016年9月6日至8日在英国苏格兰爱丁堡举行的第26届基于逻辑的程序合成和转换国际研讨会（LOPSTR 2016）的预录，与第18届声明式编程原理与实践国际研讨会（PPDP 2016）和第23届静态分析研讨会（SAS 2016）位于同一地点。在研讨会讨论后，论文将通过第二轮评审和选择的正式程序。
2016-09-01 cs.LO cs.PL
Transformer-based Program Synthesis for Low-Data Environments
大型预训练的Transformer模型（GPT 2/3，T5）的最新进展已经在程序合成中找到了用途，以生成满足一组输入/输出示例的程序。然而，这些模型在长时间和低数据任务上表现不佳，并且通常似乎不理解它们生成的语言的语义。我们调查的方法，解决这两个问题，通过使用属性上下文无关文法的程序设计语言生成的程序，然后分析生成的程序，使他们可以注释编译和运行时属性，如类型，使有关程序的信息可以记住在长期的地平线一代。我们首先发现，合成数据集可以有效地，可以提供Transformer模型与足够的数据，以执行一些合成任务。我们还发现，让模型访问程序属性在低数据环境中特别有效，并且倾向于提高transformer生成程序的质量并减少错误。
2022-05-18 cs.LG cs.PL
Towards Algorithmic Synthesis of Synchronization for Shared-Memory Concurrent Programs
我们提出了一个框架，需要一个并发程序组成的不同步的进程，随着其全球并发行为的时间规范，并自动生成一个并发程序同步，确保正确的全球行为。我们的方法支持有限状态的并发程序组成的进程，可能有本地和共享变量，可能是直线或分支程序，可能正在进行或终止，并可能有程序初始化或用户初始化的变量。规约语言是命题计算树逻辑（CTL）的扩展，其使得能够容易地对控制和数据变量的安全性和活性属性进行规约。该框架还支持在不同的抽象和粒度级别上合成同步。
2012-07-04 cs.LO cs.PL
Decidable Synthesis of Programs with Uninterpreted Functions
我们确定了一个可判定的合成问题的一类程序的无限大小的条件和迭代工作在无限的数据域。我们类中的程序使用未解释的函数和关系，并遵守最近确定的产生可判定验证的称为一致性的限制。我们制定了一个功能强大的语法限制（语法指导）的合成问题，连贯的未解释的程序，我们的问题是可判定的，确定其精确的复杂性，并研究了几个变种的问题。
2020-07-22 cs.FL cs.LO cs.PL
Pre-proceedings of the 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021)
本卷构成了第31届基于逻辑的程序合成和转换国际研讨会的预录（LOPSTR 2021），于2021年9月7日至8日举行，作为混合（混合）会议，双方都亲自参加（在爱沙尼亚塔林的教师之家）和虚拟，并与第23届声明式编程的原则和实践国际研讨会（PPDP 2021）共同举办。在研讨会讨论后，论文将通过第二轮评审和选择的正式程序。
2021-08-31 cs.LO cs.PL
Geometry of Program Synthesis
University of Melbourne（墨尔本大学）
我们重新评估通用计算的基础上综合的图灵机。这导致了一种观点的程序作为奇点的分析品种，或等价地，作为阶段的贝叶斯后综合问题。这种新的观点揭示了程序合成的研究方向，其中神经网络是一个子集，例如在相变，复杂性和概括。我们也奠定了这些新方向的经验基础，报告我们的代码中的一些简单的实验实施。
2021-03-30 cs.AI cs.LG cs.PL
Program Synthesis and Linear Operator Semantics
对于确定性和概率性的程序，我们调查的问题，程序合成和程序优化（相对于非功能属性）的一般设置的全局优化。这种方法是基于表示的语义的程序和程序片段的线性运算符，即矩阵。我们特别利用的事实，我们可以自动生成的基本块的语义表示。然后可以使用这些来组合整个程序的语义，即相应的离散时间马尔可夫链（DTMC）的生成器。我们还利用一个广义版本的抽象解释适合这个线性代数或功能分析框架，以制定语义约束（不变量）和优化目标（例如性能要求）。
2014-07-21 cs.PF cs.PL
Program Synthesis Over Noisy Data with Guarantees
Massachusetts Institute of Technology（麻省理工学院）
我们探索和形式化的任务，合成程序在嘈杂的数据，即，可能包含损坏的输入输出示例的数据。通过形式化噪声源、输入源和程序上的先验分布的概念，我们形式化了构造噪声数据集的概率过程。这种形式主义使我们能够定义一个合成算法的正确性，在它的能力来合成隐藏的底层程序。合成算法正确的概率取决于噪声源与合成算法的优化过程中使用的损失函数之间的匹配。我们形式化的概念，最佳的损失函数给定先验信息的噪声源。我们提供了一种技术来设计最佳的损失函数给定的完美和不完美的信息的噪声源。我们还形式化的概念和收敛所需的条件，即，合成算法产生正确程序的概率随着噪声数据集的大小增加而增加的条件。本文给出了最优损失函数概念的第一种形式化，最优损失函数的第一种封闭形式定义，以及保证噪声综合算法具有收敛保证的第一个条件。
2021-04-27 cs.LG cs.PL
Program Synthesis is $Σ_3^0$-Complete
本文证明程序合成在算术层级中是 $Σ_3^0$-完备的，通过构造性编码为一阶公式并归约COF问题，首次给出其一般一阶刻画，并分析变体难度。
2024-05-27 cs.CC cs.LO cs.PL
A Case for Synthesis of Recursive Quantum Unitary Programs
本文提出首个量子程序综合框架 QSynth，通过归纳量子语言、可靠推理逻辑和 SMT 编码，自动生成可跨平台执行的递归量子酉程序。
2023-12-05 cs.PL quant-ph
Resource-Guided Program Synthesis
本文介绍了资源引导合成，一种用于合成既满足功能规范又满足符号资源约束的递归程序的技术。该技术是类型导向的，并依赖于一个新的类型系统，结合多态细化类型与自动摊销资源分析的潜在注释。类型系统支持有效的基于约束的类型检查，并可以表达精确的基于细化的资源边界。类型可靠性证明表明，合成程序是正确的。通过紧密集成程序探索和类型检查，合成器可以利用用户提供的资源绑定来指导搜索，急切地拒绝消耗太多资源的不完整程序。在资源引导合成器ReSyn的实现是用来评估递归数据结构操作的范围内的技术。实验表明，ReSyn合成的程序比由资源不可知的合成器生成的程序更有效。此外，使用ReSyn的合成比合成和资源分析的简单组合更快。ReSyn还能够生成对于固定输入大小具有恒定资源消耗的实现，这可用于减轻侧信道攻击。
2019-04-18 cs.LO cs.PL
HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis
UC San Diego（加利福尼亚大学圣迭戈分校）
针对纯神经方法在陌生DSL下程序合成准确率低、纯符号方法扩展性差的问题，提出HYSYNTH混合方法，用LLM补全学习任务特定上下文无关代理模型指导合成，在三个领域性能优于现有方法。
2024-11-01 cs.AI cs.PL
AbstractBeam: Enhancing Bottom-Up Program Synthesis using Library Learning
University of Mannheim（曼海姆大学）
针对现有程序合成算法LambdaBeam未利用重复程序结构的问题，提出集成库学习的AbstractBeam框架，将重复结构融入DSL，在整数列表操作领域显著提升合成效果与效率，拓展了库学习的适用范围。
2024-09-12 cs.AI cs.PL cs.SE
NAPS: Natural Program Synthesis Dataset
NEAR
我们提出了一个面向程序合成的数据集，由人类编写的问题陈述和解决方案，这些问题。问题陈述是通过众包收集的，程序解决方案是从编程竞赛中的人类书面解决方案中提取的，并附有输入/输出示例。我们建议使用此数据集的程序合成任务，旨在与真正的用户生成的数据。作为基线，我们提出了几个模型，最好的模型达到8.8%的准确率，展示了数据集的复杂性和未来研究的巨大空间。
2018-07-06 cs.AI cs.LG cs.PL
Hierarchical Neural Program Synthesis
USC（南加州大学）；KAIST（韩国科学技术院）；Naver AI Lab（Naver人工智能实验室）；National Taiwan University（国立台湾大学）
程序合成的目标是自动构造满足给定任务规范的人类可读程序，例如输入/输出对或演示。最近的工作已经证明了令人鼓舞的结果，在各种领域，如字符串变换，张量操纵，并描述具体代理的行为。大多数现有的程序合成方法被设计成从头开始合成程序，逐行逐标记地生成程序。这从根本上阻止了这些方法扩展到合成更长或更复杂的程序。在这项工作中，我们提出了一个可扩展的程序合成框架，而不是合成一个程序的层次结构组成的程序。具体来说，我们首先学习一个任务嵌入空间和一个程序解码器，它可以解码嵌入到程序中的任务。然后，我们训练一个高级模块来理解任务规范（例如，输入/输出对或演示），并产生任务嵌入序列，然后由程序解码器解码并合成以产生合成程序。我们广泛地评估我们提出的框架中的字符串变换域的输入/输出对。实验结果表明，所提出的框架可以合成的程序是显着更长，更复杂的程序比以前的程序合成工程。网址：https://thoughtp0lice.github.io/hnps_web/
2023-03-09 cs.AI cs.LG cs.PL
Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability
IIT Bombay（印度理工学院孟买分校）；The Institute of Mathematical Sciences, Chennai（金奈数学科学研究所）；Homi Bhabha National Institute（霍米·巴巴国立研究所）；University of California at Berkeley（加州大学伯克利分校）
研究从任意非线性实数算术规范中合成程序的问题，提出在规范不可实现时仍能输出满足规范或报告无解的程序，并给出单输出变量的完备算法和一般情况下的不完备算法。
2026-05-22 cs.LO cs.PL
