Model Repair Revamped: On the Automated Synthesis of Markov Chains
本文概述了两种方法|基于反例引导的抽象精化（CEGAR）和反例引导的归纳综合（CEGIS），分别应用于有限状态概率模型和程序的自动综合。我们的CEGAR方法迭代分区的设计空间从这个空间的抽象开始，并通过一个轻量级的验证结果分析细化。CEGIS技术利用关键子系统作为反例来修剪所有在该输入上行为不正确的程序。我们展示了这些综合技术的适用性，概率方案的草图，POMDPs的控制器合成，和软件产品线。
2021-05-27 cs.PL
Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
我们考虑自动建立给定的语法引导合成（SyGuS）问题是不可实现的（即，没有解决办法）。我们制定的问题，证明一个SyGuS的问题是不可实现的一组有限的例子之一，解决一组方程：解决方案产生一个overapproximation的一组可能的输出，任何项在搜索空间可以产生的给定的例子。如果没有一个可能的输出与所有的例子一致，我们的技术已经证明了给定的SyGuS问题是不可实现的。然后，我们提出了一个算法，精确求解的方程组，导致SyGuS问题的线性整数算术（LIA）和LIA与条件（CLIA），从而表明，LIA和CLIA SyGuS问题超过100个例子是可判定的。我们在一个名为Nay的工具中实现了所提出的技术和算法。Nay可以证明70/132现有SyGuS基准测试的不可实现性，其运行时间与最先进的工具Nope相当。此外，Nay可以解决Nope无法解决的11个基准。
2020-04-02 cs.PL
Just-in-Time Learning for Bottom-Up Enumerative Synthesis
程序合成中的一个关键挑战是合成器必须探索的搜索空间的天文数字大小。为了应对这一挑战，最近的工作提出了使用学习的概率模型来指导合成。然而，对于没有高质量训练数据可用的问题域，获得这样的模型可能是不可行的。在这项工作中，我们介绍了一种替代方法，引导程序合成：而不是提前训练模型，我们展示了如何引导一个只是在时间，在合成过程中，从沿途遇到的部分解决方案的学习。为了充分利用该模型，我们还提出了一个新的程序枚举算法，我们称之为引导自自底向上的【形】的搜索，它扩展了有效的自自底向上的【形】的搜索与概率模型的指导。我们在一个名为Probe的工具中实现了这种方法，该工具针对流行的语法指导合成（SyGuS）格式中的问题。我们从文献中的基准评估探针，并表明，它实现了显着的性能增益，无论是在无指导的自自底向上的【形】的搜索和一个国家的最先进的概率引导合成器，这已经训练了现有的解决方案的语料库。此外，我们表明，这些性能的提高并不以解决方案的质量为代价：由探针产生的程序只是稍微比最短的解决方案更冗长，并没有执行不必要的情况下分裂。
2020-10-16 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
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis (Extended Version)
虽然许多主流语言（如Java、Python和C#）越来越多地采用函数式API来简化编程并提高并行化/性能，但没有有效的技术可以用于使用这些API将现有的命令式代码自动转换为函数式变体。针对这一问题，本文提出了一种基于归纳程序合成的编译方法，以实现现有代码的现代化。我们的方法是基于这样的观察，即绝大多数的源/目标程序在此设置满足一个假设，我们称之为跟踪兼容性：不仅程序共享语法相同的低级别的表达式，但这些表达式也采取相同的值在相应的执行轨迹。我们的方法利用这一观察结果来设计一种新的神经指导合成算法，该算法（1）使用一种称为同源语法网络（CGN）的新型神经架构，（2）利用一种concolic执行形式来基于计算过程中出现的中间值修剪部分程序。我们已经在一个名为NGST 2的工具中实现了我们的方法，并使用它将命令式Java和Python代码转换为分别使用Stream和functools API的函数变体。我们的实验表明，NGST 2显着优于几个基线，我们提出的神经架构和修剪技术是实现良好的结果至关重要。
2022-03-18 cs.PL
Trace-Guided Synthesis of Effectful Test Generators
Purdue University（普渡大学）；Snowflake（雪松）
本文提出利用轨迹引导合成效果测试生成器，通过捕捉效果操作的下近似行为，提升测试效率，实验表明其优于默认策略并可与高级手写方案竞争。
2026-04-06 cs.PL
Resource-Guided Program Synthesis
本文介绍了资源引导合成，一种用于合成既满足功能规范又满足符号资源约束的递归程序的技术。该技术是类型导向的，并依赖于一个新的类型系统，结合多态细化类型与自动摊销资源分析的潜在注释。类型系统支持有效的基于约束的类型检查，并可以表达精确的基于细化的资源边界。类型可靠性证明表明，合成程序是正确的。通过紧密集成程序探索和类型检查，合成器可以利用用户提供的资源绑定来指导搜索，急切地拒绝消耗太多资源的不完整程序。在资源引导合成器ReSyn的实现是用来评估递归数据结构操作的范围内的技术。实验表明，ReSyn合成的程序比由资源不可知的合成器生成的程序更有效。此外，使用ReSyn的合成比合成和资源分析的简单组合更快。ReSyn还能够生成对于固定输入大小具有恒定资源消耗的实现，这可用于减轻侧信道攻击。
2019-04-18 cs.LO cs.PL
Realizability in Semantics-Guided Synthesis Done Eagerly
针对语义引导综合的解查找问题，提出可主动分析整组候选程序的可实现性逻辑与实现逻辑，无需回溯即可得到目标程序，还给出验证条件实现方法及无锁数据结构安全内存回收场景的原型实验结果。
2024-03-08 cs.LO cs.PL
LLM-Guided Compositional Program Synthesis
针对大语言模型解决示例编程任务时易不可预测失败的问题，提出LLM引导的组合式程序合成方法，通过LLM分解并求解子任务实现失败恢复，可解决自反思方法无法处理的难例。
2025-03-12 cs.PL cs.SE
Grammar Filtering For Syntax-Guided Synthesis
George School（乔治学校）；Yale University（耶鲁大学）；Deerfield Academy（迪尔菲尔德学院）
PBE（Programming-by-Example）是一种综合范式，允许用户通过简单地提供输入输出示例来生成函数。虽然是一个很有前途的交互范例，但合成对于实时交互和更广泛的采用来说仍然太慢。PBE合成的现有方法已经使用了自动推理工具，例如SMT求解器，以及应用机器学习技术的工作。在其核心，自动推理方法依赖于程序设计语言的高度领域特定的知识。另一方面，机器学习方法利用这样的事实，即当使用程序代码时，可以生成任意大的训练数据集。在这项工作中，我们提出了一个系统，使用机器学习与自动推理技术，以解决指导合成（SyGuS）风格的PBE问题。通过用神经网络对SyGuS PBE问题进行预处理，我们可以使用数据驱动的方法来减少搜索空间的大小，然后允许基于自动推理的求解器更快地通过分析找到解决方案。我们的系统能够在现有的SyGuS PBE合成工具上运行，将2019年SyGuS竞赛的PBE Strings曲目获胜者的运行时间减少了47.65%，优于所有竞争工具。
2020-02-07 cs.LG cs.PL stat.ML
Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
递归定义的链接数据结构嵌入在一个基于指针的堆和他们的性质自然地表示在纯一阶逻辑与最少不动点定义（FO+lfp）与背景理论。这样的逻辑，不像纯粹的一阶逻辑，甚至不承认完整的程序。在本文中，我们采取了一种新的方法来综合归纳假设，以证明在这种逻辑的有效性。我们的想法是利用几种有限的一阶模型作为反例，捕捉公式的不可证明性和无效性，以指导归纳假设的搜索。我们实现我们的程序，并广泛地评估它们涉及堆数据结构的定理，需要归纳证明，并证明我们的方法的有效性。
2022-09-26 cs.LO cs.PL
FPGA Technology Mapping Using Sketch-Guided Program Synthesis
针对现有FPGA技术映射工具依赖手写规则、易出错且遗漏映射机会的问题，提出基于草图引导程序综合的Lakeroad方法，通过架构无关草图模板和HDL语义提取实现更优映射覆盖与正确性保证，性能显著优于商用及开源工具。
2024-01-29 cs.AR cs.PL
Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
IBM Research -- Tokyo（IBM研究院（东京））；Kyoto University（京都大学）
受深度神经网络（DNN）在机器学习中的最新发展的启发，我们探索了它们在PL相关主题中的应用。本文是实现这一目标的第一步;我们提出了一种无否定命题逻辑的证明合成方法，其中我们使用DNN来获得证明搜索的指南。这个想法是把证明综合问题看作是从命题到其证明的转换。我们训练seq 2seq，这是神经机器翻译中的一个流行网络，因此它生成一个编码为给定命题的$λ$ -项的证明。我们实现了整个框架，并根据经验观察到，生成的证明项在AST的树编辑距离方面接近于正确的证明。这一观察结果证明了使用经过训练的seq 2seq模型的输出作为证据搜索的指导是合理的。
2017-06-20 cs.AI cs.LO cs.PL
Gradient Descent over Metagrammars for Syntax-Guided Synthesis
UC Berkeley（加州大学伯克利分校）
语法引导的合成算法的性能高度依赖于提供良好的语法模板或语法。这种模板的提供通常留给用户手动完成，尽管在缺少这种语法的情况下，最先进的求解器将提供它们自己的默认语法，这取决于要被合成的目标程序的签名。在这项工作中，我们推测这种默认语法可以大大改善。我们建立了一套规则，或元文法，用于构造语法，并对这些元文法执行梯度下降，旨在找到一个元文法，解决更多的基准和平均更快。我们所得到的元语法使CVC 4能够在300秒的超时内解决比默认语法多26%的基准测试，并且元语法从数十个基准测试中学习到100个基准测试的性能。
2020-07-16 cs.AI cs.LG cs.PL
Neural-Guided Deductive Search for Real-Time Program Synthesis from Examples
Georgia Tech（佐治亚理工学院）；Microsoft Research India（微软研究院印度）；Microsoft Research Redmond（微软研究院雷德蒙德）
从少量的输入输出示例中合成用户预期的程序是一个具有挑战性的问题，有几个重要的应用程序，如电子表格操作，数据处理和代码重构。现有的合成系统要么完全依赖于大量手工设计的演绎逻辑技术，要么依赖于需要大量数据的纯统计模型，并且通常无法在具有挑战性的基准上提供实时的【形】合成。在这项工作中，我们提出了神经引导演绎搜索（NGDS），一种混合合成技术，结合了最好的符号逻辑技术和统计模型。因此，它生成的程序通过构造满足所提供的规范，并在看不见的示例上很好地泛化，类似于数据驱动系统。我们的技术有效地利用了演绎搜索框架，以减少学习问题的神经组件到一个简单的监督学习设置。此外，这使我们能够在有限的真实世界数据上进行训练，并仍然利用强大的递归神经网络编码器。我们证明了我们的方法的有效性，通过对真实世界的客户场景进行评估，通过合成准确的程序，与最先进的系统相比，速度高达12倍。
2018-09-09 cs.AI cs.LG cs.PL
Verifying Solutions to Semantics-Guided Synthesis Problems
研究SemGuS框架下程序验证的求解器无关方法，通过将验证问题归约为`CLP演算查询有效性，提出改进框架并实现验证器，成功解决以往无法编码和综合的实例。
2025-04-06 cs.LO cs.PL
Scaling Program Synthesis Based Technology Mapping with Equality Saturation
本文提出Churchroad技术映射器，将等价饱和与程序综合工具结合，解决FPGA映射中草图编写困难及SMT求解器乘法处理弱的问题，可处理更大更复杂的设计且无需用户提供草图。
2024-11-19 cs.AR cs.PL
Learning to Guarantee Type Correctness in Code Generation through Type-Guided Program Synthesis
Peking University（北京大学）；University of Michigan（密歇根大学）；Shanghai Jiao Tong University（上海交通大学）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；Tencent（腾讯）
TyFlow 通过内部化类型推理，提升代码生成的类型正确性与功能正确性。
2026-02-06 cs.AI cs.PL cs.SE
Duplicate-sensitivity Guided Transformation Synthesis for DBMS Correctness Bug Detection
数据库管理系统（DBMS）在从移动应用程序到网上银行的现代软件中发挥着核心作用。DBMS应该为所有应用程序提供正确的数据是至关重要的。当DBMS返回不正确的数据时，就会触发正确性错误。目前的生产级数据库管理系统仍然遭受不足的测试，由于有限的手写测试用例。最近几个作品提出了自动生成许多测试用例的查询转换，一个过程中产生一个等价的查询对和测试的DBMS，通过检查系统是否返回相同的结果集的两个查询。然而，它们仍然严重依赖于手工工作来提供转换，这在很大程度上限制了它们对有效输入查询空间的探索。本文介绍了重复灵敏度指导的变换合成，自动发现新的转换，首先合成许多候选人，然后过滤不等价的。我们的自动合成是通过变异的查询，同时保持其重复的敏感性，这是查询等价的必要条件。在候选合成之后，我们使用查询等价检查器来保持与给定查询等价的突变查询。此外，我们已经实现了我们的想法在一个工具Eqsql，并使用它来测试生产级DBMS。在两个月内，我们在MySQL、TiDB和CynosDB中总共检测到30个新确认的独特错误。
2021-07-08 cs.DB cs.PL cs.SE
Program Synthesis and Linear Operator Semantics
对于确定性和概率性的程序，我们调查的问题，程序合成和程序优化（相对于非功能属性）的一般设置的全局优化。这种方法是基于表示的语义的程序和程序片段的线性运算符，即矩阵。我们特别利用的事实，我们可以自动生成的基本块的语义表示。然后可以使用这些来组合整个程序的语义，即相应的离散时间马尔可夫链（DTMC）的生成器。我们还利用一个广义版本的抽象解释适合这个线性代数或功能分析框架，以制定语义约束（不变量）和优化目标（例如性能要求）。
2014-07-21 cs.PF cs.PL
LLM-Guided Strategy Synthesis for Scalable Equality Saturation
Peking University（北京大学）；School of Integrated Circuits（集成电路学院）
本文提出EggMind框架，通过领域特定语言EqSatL和LLM引导的代理工作流，高效合成可重用的等式饱和策略，提升资源质量平衡，减少成本和内存消耗。
2026-04-19 cs.AI cs.MA cs.PL
Program Synthesis Through Reinforcement Learning Guided Tree Search
Princeton University（普林斯顿大学）
程序合成是根据提供的规范生成程序的任务。传统上，这被程序设计语言（PL）社区视为搜索问题，最近被机器学习社区视为监督学习问题。在这里，我们提出了第三种方法，将给定程序的合成任务表示为可通过强化学习（RL）求解的马尔可夫决策过程。从部分程序的状态的观察，我们试图找到一个程序，是最佳的奖励度量对程序和状态。我们在RISC-V汇编语言的一个子集上实例化了这种方法，该语言操作于浮点数，作为PL社区基于搜索的技术的优化，我们将RL与优先级搜索树相结合。我们评估这种实例化，并证明了我们的组合方法的有效性相比，各种基线，包括纯RL消融和最先进的马尔可夫链蒙特卡罗搜索方法在这项任务上。
2018-06-08 cs.AI cs.LG cs.NE
