我们提出了一种新颖的算法，该算法合成初级编程课程的命令式程序，基于枚举程序合成和静态分析相结合的关键思想，我们的算法在平均6.6秒内能够解决基准问题。

Feb, 2017

本研究介绍了一种利用学习指导自下而上程序搜索的新兼并方法，以中间的程序为基础，通过输入输出示例进行搜索，从而构建程序，该方法在程序综合方面非常有效。

Jul, 2020

我们提出了一种自学习方法，用于从整数序列合成程序。我们的系统测试了在OEIS表格上，通过基本操作并在没有人工训练例子的情况下，自主发现了27987个序列的解决方案。

Feb, 2022

通过预测给定问题所需的指令子集，本文构建了一种高度可行的编程语言指令共现模型，支持Zoea分布式归纳编程系统的搜索空间划分，可以并行探索搜索空间的不同部分，并显著减小搜索空间的总大小。

Feb, 2023

介绍了一种通用方法，用于合成给定离散系统状态转换的程序化模型。

Jul, 2023

该论文通过引入一种名为Bee Search的新的最佳优先从底向上搜索算法，解决了现有的基于成本指导的底向上搜索算法在信息损失和成本函数排序方面的问题。实证结果表明，Bee Search在更复杂的领域特定语言（DSLs）中优于现有的成本指导的BUS算法，在简单的DSLs中与先前的方法表现相当好。此外，我们的新成本函数在字符串操作任务上优于先前的成本函数。

Oct, 2023

利用大型语言模型合成归纳循环不变量是自动化程序验证的基础。本研究观察到，大型语言模型（如gpt-3.5或gpt-4）能够在0-shot设置下为一类程序合成循环不变量，但需要多个样本来生成正确的不变量，这可能导致大量调用程序验证器以建立不变量。为解决这个问题，我们提出了一种对生成结果进行重新排名的方法，设计了一个能够根据问题定义区分正确的归纳不变量和错误尝试的排名器，该排名器被优化为对比排名器。实验结果表明，这种重新排名机制显著提高了正确不变量在生成的候选项中的排名，从而显著减少了对验证器的调用次数。

Oct, 2023

本文评估了预训练大型语言模型在解决正式综合基准测试中的能力，并提出了一种将语言模型与枚举综合算法相结合的新颖算法，结果显示该方法在性能上明显优于独立使用语言模型或枚举综合器，以及在SyGuS竞赛中取胜的工具。

Mar, 2024

LOOPer是第一个使用基于深度学习的代价模型的多面体自动调度器，覆盖了大量的仿射变换和程序。它支持探索大量的仿射变换序列，并且支持具有多个循环嵌套和矩形/非矩形迭代域的程序的优化。我们实现和评估了LOOPer，并展示其比现有技术获得了加速。在Polybench基准测试中，LOOPer相对于Tiramisu获得了1.59倍的几何平均加速度，以及相对于Pluto获得了1.34倍的几何平均加速度，Pluto是一个不使用基于机器学习的代价模型的多面体编译器。

Mar, 2024

LambdaBeam是一种具有高阶函数、lambda函数和迭代循环的程序综合的最先进的执行引导算法，而AbstractBeam是一种新颖的程序综合框架，通过图书馆学习识别程序重复、将其整合到DSL中，从而利用其潜力提高LambdaBeam的性能。

May, 2024