程序不是被写出来的，是被采样出来的

核心思想：把程序生成从”搜索”变成”约束采样”——给定一个谓词 predicate，随机采样所有且仅满足该谓词的值。生成器不是运行时搜索出来的，而是在证明器里被构造出来的。

1. 论文信息

标题：The Search for Constrained Random Generators
作者：Goldstein, Peleg, Torczon, Sainati, Lampropoulos, Pierce（UPenn / Technion / UMD）
发表：PLDI 2026
实现：Palamedes — Lean 定理证明器扩展库

2. 问题：为什么需要”约束生成器”

Property-based testing（PBT）的核心循环是：

随机生成输入 → 检查属性是否满足 → 找反例

以 BST 插入为例，要测试这个属性：

∀x, t . isBST(t) ⟹ isBST(insert(x, t))

PBT 框架会随机生成成对 (x, t)，然后跑一千次检查。

问题在于：大多数随机生成的树都不是合法 BST。标签二叉树中，超过一两个节点的树几乎都不是 BST——如果你随机生成树然后过滤掉不合法的，绝大部分计算都浪费在丢弃的样本上。

这就是 constrained random generation problem：如何只生成满足前置条件的值，而不是生成后再过滤。

传统解法是让 PBT 专家手工写一个”按约束构造”的生成器（比如 genBST），但这需要专家知道如何”按约束构造”，对普通用户门槛很高。

现有方法（约束求解、RL、LLM 辅助等）本质上都是运行时搜索——边生成边剪枝，效率差。Palamedes 的洞察是：如果能在证明器里把生成器”构造”出来，就不需要运行时搜索了。

3. 核心技术：演绎综合 + 递归方案

3.1 思路：把生成器合成变成证明搜索

Palamedes 将受约束生成器综合问题重新定义为：

找一个生成器 g，满足：对于所有值 a，a ∈ [[g]] ⟺ φ(a)

其中 [[g]] 是生成器 g 能生成的值集合，φ 是目标谓词。

换句话说：生成器在语义上等价于目标谓词，且是sound + complete 的。

综合过程用的是演绎综合（deductive synthesis）——类似于 Synquid / SuSLik 的思路：

从目标谓词 φ 开始作为 goal
一组证明规则，每个规则匹配一种语法形式
规则匹配成功后产生子目标，递归综合
完整证明树构造出来后，提取出对应的生成器

3.2 基础规则：pure 和 pick

pure a' : Gen (λa . a = a')           -- 生成唯一值

g1 : Gen P    g2 : Gen Q
─────────────────────────────
pick g1 g2 : Gen (λa . P a ∨ Q a)     -- 在两个生成器间选择

例如，对于谓词 λa . a = 1 ∨ a = 2：

匹配 pick 规则，产生两个子目标
两个子目标分别匹配 pure 规则
最终提取出生成器：pick (pure 1) (pure 2)

3.3 绑定依赖值：bind 规则

BST 生成器中有一个关键依赖：先生成节点值 x，然后用 x 来约束左右子树的取值范围。

g : Gen P    f : (a' : α') → Gen (λa . Q a' a)
─────────────────────────────────────────────
g >>= f : Gen (λa . ∃(a' : α') . P a' ∧ Q a' a)

bind 规则让生成器可以表达这种”先生成一个值，再用它约束后续生成”的依赖关系。

3.4 递归数据类型的递归方案

这是论文最有技术深度的部分。

BST 谓词本质上是一个 catamorphism（折叠）——isBST 是一个递归谓词，它按某种方式折叠树结构。

Palamedes 的关键观察是：如果一个谓词可以表示为 fold（catamorphism），那么对应的生成器就是一个 unfold（anamorphism）。这在范畴论里是对偶关系，在生成器综合里天然成立。

具体来说：

把递归谓词改写为 catamorphism 形式
寻找与之对偶的 anamorphism 作为生成器
用预推导的归纳原理替代循环证明，避免终止性证明的复杂性

这样就可以用已有的归纳原理处理一阶和二阶原始递归谓词，而不需要为每个递归函数单独证明终止性。

3.5 实现：Lean + Aesop

Palamedes 跑在 Lean 定理证明器里，综合算法本身用 Lean 的证明搜索战术 Aesop 实现。

好处：

证明器内建简化/重写，可以自动处理”逻辑等价但语法不同”的谓词变体（比如 true ∧ a = leaf → a = leaf）
综合出来的生成器正确性由 Lean 的核心检查器保证
扩展新 primitive 或 tactics 就是写 lemmas / macros

4. 评估结果

在 32 个基准测试上对比三个系统：

系统	特点
Palamedes	本文，演绎综合，运行快且轻规约负担
Cobb	SOTA 方法，Palamedes 比它快几个数量级（BST 快一个量级）
QuickChick	Rocq 上的自动生成器推导，比 Palamedes 快但规约负担更重

5. 为什么这个工作值得注意

对软件工程的影响：从”写测试”到”写规约”

传统 PBT 的流程是：先写属性（规约），再写生成器（实现）。生成器是额外的工程负担。

Palamedes 把这个关系倒过来了：你只需要写谓词，生成器从谓词自动构造出来。这和”测试即规约”（TbE）的精神一脉相承，但更进一步——规约本身变成了生成器。

对 AI Coding 的暗示：代码是采出来的，不是补出来的

回到开篇的隐喻。如果把”补全”换成”采样”，把”搜索”换成”证明”：

传统补全模型：给定前缀，在概率流形上采样下一个 token → 不保证满足类型/测试
Palamedes 思路：给定类型/谓词，在满足约束的值空间里采样 → 保证满足规约

这解释了一个现象：Vibe Coding 场景下，LLM 生成代码”能跑但不可证”——因为采样落在一个低能量谷，但不一定是可维护的解。

正确的路径可能是：LLM 负责在”规约 → 生成器”这一层工作，而规约本身需要人类来写。规约即能量函数。写好测试和类型，就是在定义代码的能量地形。

当前局限

生成器是非确定性的（只保证 support 正确，不保证分布最优）——后续工作 [Tjoa et al., 2025; Zhuang, 2026] 在处理分布调优
依赖 Lean 的类型系统，使用门槛较高
对非常高阶的递归谓词支持仍在探索

6. 一句话总结

Palamedes 把”满足谓词的随机输入生成”从运行时搜索变成了证明时构造——你写规约，Lean 给你一个保证正确的生成器。这重新定义了测试与代码的关系：不是先有代码再有测试，而是先有规约，生成器自动长出来。

论文：“The Search for Constrained Random Generators”，PLDI 2026，作者 Goldstein et al.