Hypothesis Frontier 把验证器变成搜索状态，却没有学习 DreamCoder 式库 (2026)

在保持模型、任务集和 LLM 轮数上限一致的情况下，Hypothesis Frontier 在 9 组比较中都超过了重复原始 prompt 的生成方式，最终 train-valid 比后者高 6.2 至 25.0 个百分点；其中 7 个配对 bootstrap 区间排除了零。这个结果说明，LLM 不必一次写出正确公式，精确反馈也能让它在后续轮次继续搜索。

但这项工作改变的对象不是 DreamCoder 的 library。论文没有学习跨任务可复用的 DSL，没有训练 neural recognition model，也没有运行 wake-sleep 式的库增长循环。它推进的是一个更窄、但很清楚的变量：验证器不再只是终点检查，而成为当前任务的搜索状态。

先把任务说清楚

这种设置很适合测试「反馈是否真的改变了搜索」。直接 prompting 把每次生成看成独立答案：执行，接受或丢弃。一个公式即使只错几个对象，其中已经包含的量词和关系结构也会被一并丢掉。Hypothesis Frontier 保存这部分进展，再把剩余错误交给下一轮。

验证器如何变成 frontier

论文的循环可以压缩成五步：

提出公式。 LLM 根据完整的训练世界和标签生成一个一阶公式。
逐对象验证。 系统解析公式，并在所有训练对象上执行。不可解析或不可执行的输出直接算失败；可执行但错误的公式会留下误分类对象。
沿着父公式修复。 repair 使用 false positives、false negatives 和它们的身份，选择有界的父派生编辑。结构化 beam 可以做布尔归一化、子树删除、量词体裁剪和约束放宽；selector 则寻找能够排除 false positives 的 restrictor，或覆盖 false negatives 的 expansion。所有候选都必须重新执行。
简化已验证公式。 对 train-valid 公式，系统只接受那些在全部训练对象上保留同一真值向量、同时减少 AST size、量词深度或 equality count 的候选。这个过程保证的是有限训练世界上的行为保持，不是逻辑等价。
携带最强状态。 系统把直接 proposal 和已经保留的符号后代放进累计候选池，按可执行性、可解析性、train validity、错误数和复杂度排序。下一轮 prompt 会收到当前 frontier、它的残余错误和具体误分类对象。整条轨迹最多进行 6 次 LLM 调用。

这个设计的关键限制也在这里：符号模块只能编辑 LLM 公式或其后代，不能独立合成一条全新的整式。LLM 负责引入更大的逻辑结构，符号程序负责在局部邻域中验证、修补和压缩。论文的 2 把两者的边界写得很清楚。

论文给出的一个轨迹很直观。Grok 4.3 在 Benchmark300 上先提出一个带有 7 个 false positives 和 10 个 false negatives 的一阶关系公式。repair 把它改成 0 个 false positives 和 3 个 false negatives 的版本，下一轮 prompt 再根据剩余错误把末端条件从 P 扩展为 P ∨ Q，最终得到训练集上的精确公式。这个例子说明了「不完整但更接近」的公式为什么值得保留；它并不能单独证明 repair 导致了下一轮成功。

结果到底证明了什么

论文 Table 1 同时报告训练有效性、生成 holdout world 上的 H-exact，以及最终精确简化前后的 AST。下面只列出其中两组代表性配置：

配置	HF train-valid	重复生成	HF H-exact	重复生成	HF AST pre → post
Benchmark300 / DeepSeek V4 Pro	67.3%	51.0%	35.7%	33.3%	60.5 → 45.3
Benchmark300 / Gemini 3.5 Flash	65.3%	46.0%	45.3%	41.0%	28.3 → 24.8

这里的 train-valid 要求公式在全部训练标签上无误；H-exact 要求公式在一个任务生成的所有 holdout worlds 上都无误。AST 的下降来自搜索结束后的 exact simplification，它不会改变 prompt、停止条件或 LLM 调用次数。论文报告，Benchmark300 的 3 个 Acc@gold+25 增益都在 7.7 至 9.3 个百分点之间，配对区间均排除了零；但 holdout 的提升比训练有效性的提升更小，不能把它写成普遍的概念恢复。

论文还把 LLM-free 的 Z3 搜索作为独立参考点。Z3 和 Hypothesis Frontier 覆盖的任务并不相同：前者能解决一些 HF 没有解决的实例，后者也能解决一些 Z3 没覆盖的实例。这个结果支持一个务实结论：固定语言的符号搜索和 LLM 引导的符号搜索各自覆盖不同区域，而不是其中一个已经包含另一个。

它在 DreamCoder 谱系中的位置

系统	跨任务持久对象	神经模块的作用	与 Hypothesis Frontier 的关系
DreamCoder 3	通过 wake-sleep 扩展的符号语言和库	neural recognition model 引导程序搜索	HF 没有库增长，也没有 recognizer 训练
LAPS 4	结合语言标注学习的程序库	联合学习库与 neurally guided search	HF 使用 LLM 提议公式，但不把经验沉淀成 DSL
Stitch 5	从程序语料库压缩出的可复用抽象	重点是 top-down symbolic library synthesis	HF 的 repair 只服务于当前任务，不合并跨任务子程序
LILO 6	LLM 合成、Stitch 压缩和 AutoDoc 形成的可解释库	LLM 生成并使用已学到的抽象	HF 没有持久 library、文档化抽象或下一任务复用

所以，Hypothesis Frontier 更像是谱系旁边的一条搜索路线，而不是 DreamCoder 的下一代库学习实现。它和这些工作共享「神经提议 + 符号操作」这个组合，但它保存的是单个任务的 verified frontier；DreamCoder、LAPS、Stitch 和 LILO 试图保存的是能被后续任务复用的语言、抽象或库。

这个差别会改变实验问题。对 DreamCoder 系统，关键问题是库是否变得更可压缩、更可解释，并且是否让新任务搜索得更快。对 Hypothesis Frontier，关键问题是 residual 是否让下一轮 proposal 的条件分布变得更有用。前者要求跨任务积累，后者首先只要求同一任务内的状态传递。

证据还缺哪一块

论文的 no-symbolic 对照同时关闭了 frontier conditioning、repair 和 simplification。因此，9/9 的整体增益不能说明三者中哪一个真正起了主要作用。论文的 repair 轨迹分析也是观察性的：部分 repair 会先于后续精确解出现，但这不等于 repair 对后续成功构成因果贡献。

其他边界同样重要。Z3 对照使用不同搜索空间，没有做计算量匹配；LLM call savings 排除了自动 API retry 和 Z3 runtime，因此不是总成本或 wall-clock 的结论。holdout 来自同一任务生成器，只能说明超出观测世界的泛化，不能说明面对更大的结构、部分观测、丰富签名或分布外世界时仍然稳健。最后，简化器在有限训练世界上保持行为，并不保证它在逻辑上等价于原公式。

下一步最有信息量的实验不是再增加一个模型，而是固定 LLM proposal budget、符号计算预算和总成本，分别关闭 frontier conditioning、repair、simplification，再比较每个组件带来的 train-valid、H-exact 和调用数变化。这个消融能回答 Hypothesis Frontier 真正改变了什么：是 residual 记忆、局部公式编辑，还是单纯的最终压缩。

结论

Hypothesis Frontier 证明了一个对神经-符号归纳很具体的命题：当验证器能返回对象级 residual 时，LLM 公式就不必在第一轮已经正确，系统仍然可以围绕它继续搜索。论文的实验为这个任务内循环提供了相当清楚的支持。

它暂时没有证明另一个更强的命题：系统已经学会了 DreamCoder 式的可复用程序语言。没有跨任务库增长、没有 neural recognition model，也没有把修复出的结构带到下一个任务。把这项工作放在正确的位置，结论反而更有用：它把「验证反馈如何塑造神经搜索」从直觉推进成了一个可测量的组件，而持久 DSL 学习仍然是另一道尚未解决的问题。

References

1
主论文
arxiv.org
2
论文方法章节
arxiv.org
3
DreamCoder
arxiv.org
4
LAPS
arxiv.org
5
Stitch
arxiv.org
6
LILO
arxiv.org