有好的错误吗？CEGIS的理论分析
Are There Good Mistakes? A Theoretical Analysis of CEGIS
摘要：
反例引导的归纳综合CEGIS是用来综合程序从候选空间的程序。当候选程序空间有限时，该方法保证终止并综合出正确的程序。但是，如果程序的候选空间是无限的，该技术可能会或可能不会终止于正确的程序。本文对反例引导的归纳综合技术进行了理论分析。我们调查的候选空间，正确的程序可以使用CEGIS合成的集合是否取决于在归纳合成中使用的反例，也就是说，是否有好的错误，这将增加合成功率。我们调查是否使用最小的反例，而不是任意的反例扩大了一组候选空间的程序，归纳合成可以成功地合成一个正确的程序。我们考虑两类反例：极小反例和历史有界反例。在CEGIS的任何迭代中使用的历史有界反例由在归纳综合的先前迭代中使用的示例所限定。我们研究在这两种情况下归纳综合的功率的相对变化。我们发现，使用最小的反例MinCEGIS的合成技术具有相同的合成功率CEGIS，但使用历史有界反例HCEGIS的合成技术具有不同的功率比CEGIS，但没有占主导地位的其他。
英文摘要：
Counterexample-guided inductive synthesis CEGIS is used to synthesize programs from a candidate space of programs. The technique is guaranteed to terminate and synthesize the correct program if the space of candidate programs is finite. But the technique may or may not terminate with the correct program if the candidate space of programs is infinite. In this paper, we perform a theoretical analysis of counterexample-guided inductive synthesis technique. We investigate whether the set of candidate spaces for which the correct program can be synthesized using CEGIS depends on the counterexamples used in inductive synthesis, that is, whether there are good mistakes which would increase the synthesis power. We investigate whether the use of minimal counterexamples instead of arbitrary counterexamples expands the set of candidate spaces of programs for which inductive synthesis can successfully synthesize a correct program. We consider two kinds of counterexamples: minimal counterexamples and history bounded counterexamples. The history bounded counterexample used in any iteration of CEGIS is bounded by the examples used in previous iterations of inductive synthesis. We examine the relative change in power of inductive synthesis in both cases. We show that the synthesis technique using minimal counterexamples MinCEGIS has the same synthesis power as CEGIS but the synthesis technique using history bounded counterexamples HCEGIS has different power than that of CEGIS, but none dominates the other.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
