本文介绍了一种面向编程求解的领域特定语言TerpreT，它能够通过四种不同的后端进行推理，探索了不同领域、程序表示和解释模型的应用，并将模型说明与推理算法分离，提供了比较不同推理方法的基础。通过对多种程序模型的若干解释器模型进行广泛的经验比较，本文认为约束求解器优于基于梯度下降和基于LP松弛的方法。

Dec, 2016

提出一种基于MAKESPEARE简单推迟接受式爬山法的归纳编程综合方法，该方法可以从输入/输出示例中合成低级循环程序，成功解决了之前未解决的“Collatz Numbers”程序合成问题，并在一些基准测试中表现出色，在整数数组的快速排序问题中观察到组合排序的出现。

Nov, 2018

本文研究了语法引导综合中的过拟合现象，提出了针对性地选择合适语法以增加合成器性能的方法，并最终通过提出的混合枚举算法达到了比2018年SyGuS竞赛获胜者更高的速度和效率。

May, 2019

该论文提出了一种神经程序合成方法，该方法使用读取-执行-打印循环(REPL)集成组件来定位可能程序的搜索空间，并通过训练政策模型和价值函数模型，能够合成文本编辑和2D、3D图像程序。

Jun, 2019

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

Jul, 2020

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

Oct, 2023

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

Oct, 2023

基于神经网络的机制可解释性自动合成方法MIPS，将学习到的算法自动转化为Python代码，解决了62个可以由RNN学习的算法任务中的32个问题，并对GPT-4的补充具有高度互补性，且不使用人工训练数据。

Feb, 2024

在本文中，我们提出了一种使用语义空间进行程序策略综合的替代方法，通过学习一组具有不同代理行为的程序库来定义语义空间，并通过在当前候选程序中替换程序库中的程序来近似语义空间，实验证明在语义空间中搜索比在基于语法的空间中搜索更加高效。

May, 2024

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

May, 2024