从混合量词属性中递归程序合成
Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties
AI总结：
本文提出了一种基于反例引导和预防性剪枝的递归程序合成方法，通过斯科伦化将混合量词问题转化为$\forall^*$-合成问题，提升合成效率。
摘要：
我们提出了一种新的方法，用于自动从混合量词一阶逻辑属性中合成递归程序。我们的方法利用斯科伦化将混合量词合成问题转化为$\forall^*$-合成问题，在合成目标程序的同时，合成引入的斯科伦符号的见证生成函数。我们通过基于草图的枚举、反例引导方法来处理$\forall^*$-合成。我们的算法从反例中学习语法约束以剪枝候选空间，并采用预防性剪枝技术以避免枚举无效候选。我们在42个基准上评估了我们的技术，证明反例泛化和预防性剪枝显著提高了性能。
英文摘要：
We present a novel approach for the synthesis of recursive programs from mixed-quantifier first-order logic properties. We solve this problem using a sketching-based, enumerative, counterexample-guided approach. Our algorithm learns syntactic constraints from counterexamples to prune the candidate space and employs a prophylactic pruning technique to avoid enumerating invalid candidates altogether. We implement our technique in a tool called Cataclyst and evaluate it on a suite of 60 benchmarks. We demonstrate that both counterexample generalization and prophylactic pruning significantly improve performance. Cataclyst solves 59/60 benchmarks, while variants of Cataclyst without counterexample generalization or prophylactic pruning solve fewer benchmarks. The only other tool that can handle mixed-quantifier specifications does not support sketching, so a direct comparison is not possible. This prior tool solves 12/60 benchmarks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
