一句话：提出基于演绎程序合成的受限随机生成器合成方法，并在 Lean 中实现 Palamedes。
基于属性的测试（PBT）中，受限随机生成问题要求根据程序值上的谓词，仅从满足该谓词的值集合中随机采样。由于测试前提常使有效输入分布稀疏，高效生成器至关重要。论文提出用演绎程序合成解决该问题：基于生成器的指称语义给出合成规则，形成自动合成正确生成器的过程；对递归谓词，将其改写为 catamorphism，再匹配相应 anamorphism，从而比既有递归函数合成方法更简单但仍极具表达力。作者实现 Palamedes——Lean 定理证明器的可扩展库，合成算法由标准证明搜索策略构建，降低实现负担并受益于 Lean 证明自动化进展。
Among the biggest challenges in property-based testing (PBT) is the constrained random generation problem: given a predicate on program values, randomly sample from the set of all values, and only values, satisfying that predicate. Efficient solutions to this problem are critical, since the executable specifications used by PBT often have preconditions that input values must satisfy in order to be valid test cases, and satisfying values are often sparsely distributed. We propose a novel approach to this problem using deductive program synthesis. We present a set of synthesis rules, based on a denotational semantics of generators, that give rise to an automatic procedure for synthesizing correct generators. Our system handles recursive predicates by rewriting them as catamorphisms and then matching with appropriate anamorphisms; this is theoretically simpler than other approaches to synthesis for recursive functions, yet still extremely expressive. Our implementation, Palamedes, is an extensible library for the Lean theorem prover. The synthesis algorithm itself is built out of standard proof-search tactics, reducing implementation burden and allowing the algorithm to benefit from further advances in Lean proof automation.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2511-12253,
title = {The Search for Constrained Random Generators},
author = {Harrison Goldstein and Hila Peleg and Cassia Torczon and Daniel Sainati and Leonidas Lampropoulos and Benjamin C. Pierce},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808329}
}