---
title: "AND-OR DAG 分层记忆化"
created: 2026-07-03
updated: 2026-07-03
type: concept
tags: ["theorem-proving", "dag", "memory", "planning"]
sources: ["arxiv:2606.03303"]
---

# AND-OR DAG 分层记忆化

> 不只是记录证明进度，还结构化分层记忆——单调精化、引理复用、预期规划。

## 核心定义

**AND-OR DAG 分层记忆化** 是 [[leap-agentic-atp|LEAP]] 证明树的组织方式：
- **OR 节点**：开放目标或引理声明——可用任意有效策略解决
- **AND 节点**：候选分解——其成功取决于所有子目标都被证明

## 三个关键属性

### 1. 单调精化（Monotone Refinement）

一旦目标被分解为子目标，后续搜索可聚焦于扩展和解决这些后代，**无需重构已有依赖结构**。单个证明尝试可被修改、扩展或放弃，而 DAG 保留整体证明计划的稳定依赖结构。

### 2. 引理记忆化（Lemma Memoization）

中间引理声明存储为共享证明节点，在**不同分支中出现相同子问题时复用**。这减少了冗余推导，让独立证明路径收敛于公共依赖。

### 3. 预期引理规划（Anticipatory Lemma Planning）

蓝图生成阶段可提出**当前不立即需要但未来可能有用**的辅助引理。这些预期引理作为非必需依赖（虚线边）保留在图记忆中，不影响当前 AND 节点的解决。

## 与证明透明度的关系

DAG 暴露了：哪些目标仍开放、哪些引理已解决、哪些节点阻塞下游进展。这为 [[verification-guided-proof-search|验证引导搜索]] 提供可解释的蓝图式工作空间，也支持人-AI 协作。

## 参考

- [[leap-agentic-atp|LEAP]]
- [[blueprint-driven-atp|蓝图驱动 ATP]]
- [[interleaved-informal-formal-planning|非正式-形式化交错规划]]