---
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|非正式-形式化交错规划]]