← 研踪 PaperTrailarXiv:2601.04045 · v3
Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties
首次提交 2026-01-08 00:00
版本更新 2026-11-08 08:08
雷达观测 2026-11-10 12:16
摘要
We present a novel approach for the synthesis of recursive programs from relational, 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. No existing tool can directly handle the entire class of synthesis problems that our tool can. A portfolio of existing state-of-the-art tools solves 30/60 of our benchmarks.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v3 · 2026-11-08 08:08 · 最新观测版本
Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties
We present a novel approach for the synthesis of recursive programs from relational, 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. No existing tool can directly handle the entire class of synthesis problems that our tool can. A portfolio of existing state-of-the-art tools solves 30/60 of our benchmarks.
查看此版本解读 →查看此版本原文 ↗