1.8 KiB
1.8 KiB
title, created, updated, type, tags, sources
| title | created | updated | type | tags | sources | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| 验证引导证明搜索（Verification-Guided Proof Search） | 2026-07-03 | 2026-07-03 | concept |
|
|
验证引导证明搜索
两层验证过滤：Lean 编译器保证形式化正确性，LLM Reviewer 评估分解质量——缺一不可。
核心定义
验证引导证明搜索 是 leap-agentic-atp 中的双层验证机制，用于引导 and-or-dag-memoization 上的 DFS + 回溯搜索。
两层验证
层 1：Lean 编译器（形式验证）
- 检查候选证明的语法和类型正确性
- 对证明草图：仅允许
sorry占位符用于新声明的子目标（保留 AND-OR 语义） - 这是硬约束——不通过就是不正确
层 2：LLM Reviewer（质量评估）
- 评估蓝图分解的质量：
- 子目标是否与父目标相关？
- 是否使问题更简单？
- 是否提供了合理的完成路径？
- 这是软约束/搜索过滤器——防止在弱分解上浪费搜索预算
- 识别无前途的分解 → 触发回溯 → 探索替代策略
为什么 LLM Reviewer 不可省略
消融实验表明：没有 LLM Reviewer 时，草图可能语法正确但引入了 ill-posed（不恰当）或与原始目标同样困难的子目标。Agent 会反复扩展这些弱蓝图，消耗搜索预算而没有任何实质进展。
未来方向
LEAP 目前使用简单 DFS + 回溯。论文指出 LLM 可以进一步作为启发式评估器引导搜索——不只是过滤，而是主动评分和排序候选分支。