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