Algorithmic paradigms such as divide-and-conquer (D&C) are proposed to guide the design of efficient algorithms, but applying them to optimize existing programs is difficult. Therefore, many research efforts have been devoted to the automatic application of algorithmic paradigms. However, most existing approaches to this problem are based on deductive methods and thus put significant restrictions on how the original program is implemented. To overcome this limitation, we study the automatic application of paradigms as an oracle-guided inductive synthesis problem, where the synthesizer only invokes the original program as a black-box oracle or uses a given verifier to verify the correctness of candidate programs. Such a synthesizer puts no restriction on the original program and thus overcomes the limitation of deductive approaches. We notice that the application tasks of various paradigms have a similar form as that of D&C. We denote these paradigms as D&C-like paradigms, unify their application tasks into a novel type of synthesis problems, named lifting problems, and propose an efficient inductive synthesizer AutoLifter for lifting problems. The main challenge of solving lifting problems is from the usually large scale of efficient algorithms. To overcome this challenge, we divide and conquer lifting problems. We devise two novel decomposition methods, component elimination and variable elimination, to soundly divide a lifting problem into simpler subtasks, each tractable with existing inductive synthesizers. We evaluate AutoLifter on 96 programming tasks related to 6 different algorithmic paradigms. AutoLifter solves 82/96 tasks with an average time cost of 6.53 seconds, significantly outperforming existing approaches.

翻译：算法范式（如分而治之，D&C）旨在指导高效算法的设计，但将其应用于优化现有程序十分困难。因此，大量研究工作致力于算法范式的自动应用。然而，现有方法大多基于演绎方法，对原始程序的实现方式施加了显著约束。为突破这一局限，我们将范式自动应用问题建模为预言引导的归纳综合问题：综合器仅将原始程序作为黑盒预言调用，或利用给定验证器验证候选程序的正确性。此类综合器不对原始程序施加任何约束，从而克服了演绎方法的局限性。我们注意到，多种范式的应用任务与分治范式具有相似形式。我们将这些范式统称为分治类范式，将其应用任务统一为一类新型综合问题（称为提升问题），并提出高效归纳综合器AutoLifter。解决提升问题的主要挑战源于高效算法通常规模庞大。为应对这一挑战，我们对提升问题采用分治策略：设计两种新颖的分解方法（分量消除与变量消除），将提升问题可靠地划分为更简单的子任务，每个子任务均可通过现有归纳综合器求解。我们在与6种不同算法范式相关的96项编程任务上评估AutoLifter。AutoLifter以平均6.53秒的时间成本解决了82/96项任务，显著优于现有方法。