分而治之的归纳综合方法用于D&C类算法范式
摘要：自动提升程序性能的算法范型称为分治法（D&C）。然而，将这些范型应用于优化现有程序是困难的。因此，许多研究工作致力于自动应用算法范型。然而，大多数现有的方法都基于演绎方法，因此对原始程序的实现方式有很大的限制。为了克服这个限制，我们将自动应用范型的研究作为一种由oracle引导的归纳合成问题进行研究，其中合成器仅将原始程序作为黑盒oracle调用或使用给定的验证器来验证候选程序的正确性。这样的合成器对原始程序没有限制，因此克服了演绎方法的限制。 我们注意到各种范型的应用任务与D&C的形式相似。我们将这些范型称为D&C-like范型，将它们的应用任务统一到一种新的合成问题类型中，称为lifting问题，并提出了一种高效的归纳合成器AutoLifter来解决lifting问题。解决lifting问题的主要挑战来自通常大规模的高效算法。为了克服这个挑战，我们采用分治法来解决lifting问题。我们设计了两种新的分解方法，即组件消除和变量消除，将lifting问题合理地分解为更简单的子任务，每个子任务都可使用现有的归纳合成器进行处理。 我们对96个与6种不同算法范型相关的编程任务测试了AutoLifter。AutoLifter解决了82/96个任务，在平均耗时6.53秒的情况下表现出色，明显优于现有的方法。
作者：Ruyi Ji, Yuwei Zhao, Yingfei Xiong, Di Wang, Lu Zhang, Zhenjiang Hu
论文ID：2202.12193
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-11