用语法约束精简程序空间，加速程序合成搜索。
Modelling Program Spaces in Program Synthesis with Constraints
- 通过语法约束定义程序空间，筛选潜在有用解。
- 实验显示可消除99%无效程序，大幅减少枚举时间。
- 适合需要高效程序合成的开发者与研究者。
程序合成的核心挑战在于应对庞大的可能程序空间。由于程序合成本质上是组合搜索，学界一直尝试利用强大的组合约束求解器。现有方法通常将约束用于表达程序语义，但未充分挖掘其排除无效程序的潜力。近期归纳逻辑编程方法引入对目标程序语法的约束，使无需执行即可进行约束检查与传播，支持任意算子。本文提出利用语法约束建模程序空间，不仅限定可行解，还聚焦于可能有用的解。为此，我们设计BART求解器，能高效传播与求解这些约束。在程序空间枚举任务上评估发现，约束可消除高达99%的程序空间，且建模程序空间显著降低枚举耗时。
原文摘要 · Abstract (English)
A core challenge in program synthesis is taming the large space of possible programs. Since program synthesis is essentially a combinatorial search, the community has sought to leverage powerful combinatorial constraint solvers. Here, constraints are used to express the program semantics, but not as a potentially potent tool to remove unwanted programs. Recent inductive logic programming approaches introduce constraints on the program's syntax to be synthesized. These syntactic constraints allow for checking and propagating a constraint without executing the program, and thus for arbitrary operators. In this work, we leverage syntactic constraints to model program spaces, defining not just solutions that are feasible, but also ones that are likely useful. To demonstrate this idea, we introduce BART, a solver that efficiently propagates and solves these constraints. We evaluate BART on program space enumeration tasks, finding that the constraints eliminate up to 99 percent of the program space, and that modeling program spaces significantly reduces enumeration time.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。